Теорема Лёба

[маткиб]

epros писал(а):

Ну, давайте так. Только в чём тут уточнение?

Тогда постите доказательство (Вы там какие-то замены хотели сделать, не помню какие). Будем указывать на ошибку.

epros писал(а):

Не могу понять, откуда возьмутся мета($\omega$)-аксиомы, не являющиеся мета(n)-аксиомами ни для какого n, если мы определяли в качестве мета($\omega$)-аксиом все мета(n)-аксиомы и только их.

Не знаю, откуда Вы взяли, что мы так определяли.
Для мета($\omega$)-доказуемости мы определяли схему аксиом (для каждой формулы $\Phi$ своя аксиома):
$(\exists n)(\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi$, либо
$(\forall n)((\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi)$,
что одно и то же.
Легко убедиться в том, что среди аксиом мета(n)-доказуемостей таковых нет.

epros писал(а):

Кстати, значит ли это, что Вашу формулировку можно записать так:
$(\forall n)(\mathrm{PA}_n \nvdash (0=S(0)))$?
Т.е. без всяких импликаций?

Можно. Ещё можно записать как
$(\forall n)\mathrm{Con}(\mathrm{PA}_n)$.

epros писал(а):

маткиб писал(а):

Естественно, оно ошибочно. Ошибка выделена красным.

Т.е. Вы утверждаете, что в мета($\omega$)-теории появились некоторые новые аксиомы (которых не было ни на одном из мета(n)-уровней)? И пример такой аксиомы - это Ваше утверждение, приведённое выше?

Именно.

epros писал(а):

Но я не могу понять, откуда эти аксиомы могут взяться. Либо это - доказуемое утверждение (например, по индукции: если арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым). Либо, наверное, придётся обойтись без такой аксиомы.

Оно доказуемое, только не в арифметике Пеано и ни в какой мета(n)-арифметике Пеано. А, например, в арифметике с кванторами по подмножествам множества натуральных чисел оно вполне себе доказуемо.

[epros]

маткиб писал(а):

Тогда постите доказательство (Вы там какие-то замены хотели сделать, не помню какие). Будем указывать на ошибку.

Хм. Помнится, предполагалось заменить алгоритм, результатом которого является формула теории, на алгоритм, результатом которого является её Гёделевский номер. Но я вижу, что в такой постановке моя формулировка не проходит...

маткиб писал(а):

epros писал(а):

Не могу понять, откуда возьмутся мета($\omega$)-аксиомы, не являющиеся мета(n)-аксиомами ни для какого n, если мы определяли в качестве мета($\omega$)-аксиом все мета(n)-аксиомы и только их.

Не знаю, откуда Вы взяли, что мы так определяли.
Для мета($\omega$)-доказуемости мы определяли схему аксиом (для каждой формулы $\Phi$ своя аксиома):
$(\exists n)(\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi$, либо
$(\forall n)((\mathrm{PA}_n\vdash\Phi)\rightarrow\Phi)$,
что одно и то же.
Легко убедиться в том, что среди аксиом мета(n)-доказуемостей таковых нет.

Наверное, схема определялась не только для каждой формулы $\Phi$, но и для каждого мета-уровня $\mathrm{PA}_n$?

Но я кажется понял Вашу идею. Вы в качестве мета($\omega$)-аксиомы рассматриваете формулу с квантором по номерам мета-уровней, а такой аксиомы на каком-либо конкретном мета-уровне действительно нет. Так? Это в чём-то аналогично схеме индукции: Она может быть записана одной формулой на мета(1)-уровне, но такой общей аксиомы в самой теории нет (хотя все аксиомы схемы в теории есть). Так и здесь: одна общая аксиома в мета($\omega$)-теории есть, записать её в виде схемы, каждая из аксиом которой есть на каком-либо из мета-уровней, тоже можно, но самой этой аксиомы ни на каком из мета-уровней нет.

маткиб писал(а):

epros писал(а):

Но я не могу понять, откуда эти аксиомы могут взяться. Либо это - доказуемое утверждение (например, по индукции: если арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым). Либо, наверное, придётся обойтись без такой аксиомы.

Оно доказуемое, только не в арифметике Пеано и ни в какой мета(n)-арифметике Пеано. А, например, в арифметике с кванторами по подмножествам множества натуральных чисел оно вполне себе доказуемо.

А в том, что мы назвали мета($\omega$)-расширением арифметики, оно доказуемо?

[маткиб]

epros писал(а):

Наверное, схема определялась не только для каждой формулы $\Phi$, но и для каждого мета-уровня $\mathrm{PA}_n$?

Нет, по мета-уровням был квантор $\forall$ в формуле.

epros писал(а):

Но я кажется понял Вашу идею. Вы в качестве мета($\omega$)-аксиомы рассматриваете формулу с квантором по номерам мета-уровней, а такой аксиомы на каком-либо конкретном мета-уровне действительно нет. Так?

Именно.

epros писал(а):

маткиб писал(а):

epros писал(а):

Но я не могу понять, откуда эти аксиомы могут взяться. Либо это - доказуемое утверждение (например, по индукции: если арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым). Либо, наверное, придётся обойтись без такой аксиомы.

Оно доказуемое, только не в арифметике Пеано и ни в какой мета(n)-арифметике Пеано. А, например, в арифметике с кванторами по подмножествам множества натуральных чисел оно вполне себе доказуемо.

А в том, что мы назвали мета($\omega$)-расширением арифметики, оно доказуемо?

Да вроде то утверждение, которое рассматривалось было просто по определению доказуемо в мета($\omega$)-расширением арифметики.

Кстати, утверждение о том, что если какая-то арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым, вообще говоря, неверно (даже для мета(1)-расширений).

[nikov]

маткиб писал(а):

Кстати, утверждение о том, что если какая-то арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым, вообще говоря, неверно (даже для мета(1)-расширений).

Например, арифметика Пеано с аксиомой о противоречивости арифметики Пеано будет непротиворечивой, а ее метарасширение - противоречиво. Верно?

[epros]

маткиб писал(а):

epros писал(а):

Наверное, схема определялась не только для каждой формулы $\Phi$, но и для каждого мета-уровня $\mathrm{PA}_n$?

Нет, по мета-уровням был квантор $\forall$ в формуле.

Тогда я чего-то не понимаю. Мы определяли мета(n)-расширение арифметики индуктивно как мета(n-1)-расширение, к которому добавлена схема аксиом:
$PRF_{n-1}(\Phi) \to \Phi$

Соответственно, мета($\omega$)-расширение определялось как теория, включающая схемы аксиом для всех мета(n)-уровней. Т.е. мы строим общую схему для всех аксиом типа $PRF_n(\Phi) \to \Phi$, т.е. общую как для любых n, так и для любых формул $\Phi$. Правильно?

маткиб писал(а):

Да вроде то утверждение, которое рассматривалось было просто по определению доказуемо в мета($\omega$)-расширением арифметики.

Тогда мне очень странно называть это утверждение мета($\omega$)-аксиомой. Скорее уж это мета($\omega$)-теорема.

маткиб писал(а):

Кстати, утверждение о том, что если какая-то арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым, вообще говоря, неверно (даже для мета(1)-расширений).

Интересно. А есть опровергающий пример?

Напомню, что здесь мы говорили только о таких мета-расширениях, которые получаются добавлением схемы $PRF(\Phi) \to \Phi$. Я понимаю, что могут быть и другие расширения, которые будут противоречивыми.

[маткиб]

epros писал(а):

Тогда я чего-то не понимаю. Мы определяли мета(n)-расширение арифметики индуктивно как мета(n-1)-расширение, к которому добавлена схема аксиом:
$PRF_{n-1}(\Phi) \to \Phi$

Соответственно, мета($\omega$)-расширение определялось как теория, включающая схемы аксиом для всех мета(n)-уровней. Т.е. мы строим общую схему для всех аксиом типа $PRF_n(\Phi) \to \Phi$, т.е. общую как для любых n, так и для любых формул $\Phi$. Правильно?

Вообще-то, насколько я помню, мы определяли схему аксиом
$(\forall n)(PRF_n(\Phi) \to \Phi)$,
т.е. по одной аксиоме для каждого $\Phi$ (но не для $n$).

epros писал(а):

Тогда мне очень странно называть это утверждение мета($\omega$)-аксиомой. Скорее уж это мета($\omega$)-теорема.

Рассматривалось, насколько я помню, много разных утверждений, некоторые из которых были мета($\omega$)-аксиомами, а некоторые - теоремами.
Например,
$(\forall n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$ - аксиома,
а
$(\forall n)\mathrm{Con}(\mathrm{PA}_n)$ - теорема.

epros писал(а):

маткиб писал(а):

Кстати, утверждение о том, что если какая-то арифметика непротиворечива, то ни одно из её мета-расширений не будет противоречивым, вообще говоря, неверно (даже для мета(1)-расширений).

Интересно. А есть опровергающий пример?

Пожалуйста, возьмём теорию $T=\mathrm{PA}+\neg\mathrm{Con}(PA)$ (т.е. теория, получающаяся добавлением к арифметике Пеано утверждения о противоречивости арифметики Пеано). Тогда $T$ будет непротиворечива, а мета(1)-расширение $T$ - уже противоречиво.

[nikov]

маткиб писал(а):

Пожалуйста, возьмём теорию $T=\mathrm{PA}+\neg\mathrm{Con}(PA)$ (т.е. теория, получающаяся добавлением к арифметике Пеано утверждения о противоречивости арифметики Пеано). Тогда $T$ будет непротиворечива, а мета(1)-расширение $T$ - уже противоречиво.

Хотя $T$ и непротиворечива, она $\omega$-противоречива (утверждает существование числа, являющегося номером доказательства формулы $1=2$, но такого числа предъявить не может). А можно придумать теорию, которая была бы и непротиворечива и $\omega$-непротиворечива, а какое-то ее метарасширение было бы противоречиво?

[маткиб]

nikov писал(а):

Хотя $T$ и непротиворечива, она $\omega$-противоречива (утверждает существование числа, являющегося номером доказательства формулы $1=2$, но такого числа предъявить не может). А можно придумать теорию, которая была бы и непротиворечива и $\omega$-непротиворечива, а какое-то ее метарасширение было бы противоречиво?

Напомните определение $\omega$-непротиворечивости, тогда отвечу (меня оно как-то стороной обошло).

Добавлено спустя 11 минут 6 секунд:

nikov писал(а):

Хотя $T$ и непротиворечива, она $\omega$-противоречива (утверждает существование числа, являющегося номером доказательства формулы $1=2$, но такого числа предъявить не может). А можно придумать теорию, которая была бы и непротиворечива и $\omega$-непротиворечива, а какое-то ее метарасширение было бы противоречиво?

А, нашёл
http://en.wikipedia.org/wiki/Ω-consistent_theory

Тогда можно доказать, что по крайней мере для ординалов

$$\alpha<\omega+\omega^{\omega}+\omega^{{\omega}^{\omega}}+\ldots$$

если теория $\omega$-непротиворечива, то её мета($\alpha$)-расширение будет непротиворечивым (если мета($\alpha$)-расширение для таких маленьких ординалов определять естественным образом).

Добавлено спустя 4 минуты 34 секунды:

А нет, вру, это только если мета-расширение определять как добавление непротиворечивостию. Вопрос пока открыт

[nikov]

маткиб писал(а):

Тогда можно доказать, что по крайней мере для ординалов

$$\alpha<\omega+\omega^{\omega}+\omega^{{\omega}^{\omega}}+\ldots$$

Кстати, я несколько дней уже думаю, насколько далеко так можно продвинуться. Насколько я знаю, предел этой суммы Кантор обозначал $\epsilon_0$. Мне вроде бы удалось понять, как строится мета$(\epsilon_0)$- и мета$(\epsilon_1)$-расширение арифметики Пеано. Хочу попробовать действительно выписать алгоритм для соответствующей схемы аксиом.

[epros]

маткиб писал(а):

Вообще-то, насколько я помню, мы определяли схему аксиом
$(\forall n)(PRF_n(\Phi) \to \Phi)$,
т.е. по одной аксиоме для каждого $\Phi$ (но не для $n$).

Наверное, так тоже можно, хотя я в этом пока не уверен. Дело в том, что обозначенный мной подход: "определять мета($\omega$)-расширение как теорию, включающую схемы аксиом всех мета(n)-уровней", подразумевает только возможность записать общий алгоритм для генерирования формулы $PRF_n(k)$ по предъявленным в качестве аргументов n (номер уровня мета-доказуемости) и k (порядковый номер формулы арифметики). А обозначенный сейчас Вами подход требует также чтобы $PRF_n(k)$ записывалась в виде общей формулы арифметики со свободными переменными n и k. Возможность последнего мне пока не очевидна.

А что, разве обозначенный мной подход не годится?

маткиб писал(а):

$(\forall n)(\mathrm{PA}_n\vdash(0=S(0)))\rightarrow(0=S(0))$ - аксиома,

Если быть точным, то в обозначенном Вами подходе аксиомой является:
$(\forall n)(PRF_n(k) \rightarrow (0=S(0))$, где в качестве k следует подставить порядковый номер формулы $0=S(0)$.

Символов типа $\vdash$ выбранный Вами синтаксис не допускает.

А в обозначенном мной подходе указанная Вами формула, как я понимаю, будет не аксиомой, а теоремой, доказуемой по индукции по порядковым номерам уровней мета(n)-доказуемости.

маткиб писал(а):

Пожалуйста, возьмём теорию $T=\mathrm{PA}+\neg\mathrm{Con}(PA)$ (т.е. теория, получающаяся добавлением к арифметике Пеано утверждения о противоречивости арифметики Пеано). Тогда $T$ будет непротиворечива, а мета(1)-расширение $T$ - уже противоречиво.

Понятно. Для $\omega$-противоречивой теории мета(1)-расширение противоречиво. Значит даже если мы уверены в том, что арифметика непротиворечива и даже $\omega$-непротиворечива, всё равно можно предположить, что на некоем уровне её мета(n)-расширение окажется противоречивым? А в таком случае и мета($\omega$)-расширение будет противоречивым?

М-да, это ставит под сомнение целесообразность построения цепочки мета(n)-расширений арифметики...

[маткиб]

epros писал(а):

А что, разве обозначенный мной подход не годится?

Ну почему же не годится? Годится. Если определять аксиомы мета($\omega$)-уровня как все аксиомы всех мета(n)-уровней, то на мета($\omega+1$) мы получим как раз то, что сейчас имеем на мета($\omega$)-уровне.

epros писал(а):

А в обозначенном мной подходе указанная Вами формула, как я понимаю, будет не аксиомой, а теоремой, доказуемой по индукции по порядковым номерам уровней мета(n)-доказуемости.

Она не будет теоремой. Такая теорема появится только на мета($\omega+1$) уровне.

epros писал(а):

М-да, это ставит под сомнение целесообразность построения цепочки мета(n)-расширений арифметики...

А вот я не вижу, в чём тут нецелесообразность.

[nikov]

Кстати, нет ли в ZFC доказательства $\omega$-непротиворечивости арифметики Пеано?

[маткиб]

nikov писал(а):

Кстати, нет ли в ZFC доказательства $\omega$-непротиворечивости арифметики Пеано?

есть

[nikov]

маткиб писал(а):

nikov писал(а):

Кстати, нет ли в ZFC доказательства $\omega$-непротиворечивости арифметики Пеано?

есть

Ну что же Вы так односложно отвечаете! Мне очень интересно, как это доказательство построено и где его можно найти.