что следует из теоремы Геделя

[Alexey Romanov]

Ваша метатеория в логике первого порядка:

1) содержит арифметику;
2) рекурсивно аксиоматизируема;

3) следовательно, по теореме Гёделя о неполноте, её арифметическая часть неполна.

Если она описывает только стандартные натуральные числа, то по теореме Гёделя о полноте, её арифметическая часть полна.

Или о теореме о полноте Вы тоже не желаете слышать?

-- Пн июн 22, 2009 14:55:11 --

Меня легко опровергнуть, если Вы правы: Вам достаточно просто явно выписать все аксиомы метатеории и предъявить доказательство. Без всяких "очевидно, что" -- просто доказательство в логике первого порядка. Его можно будет механически проверить и выписать Вам премию за опровержение одной из теорем Гёделя (уж какой из них, придётся разбираться отдельно).

[epros]

Alexey Romanov в сообщении #223950 писал(а):

Ваша метатеория в логике первого порядка:
1) содержит арифметику;

Разумеется. Я даже предлагаю включить в неё "аксиому рефлексивности" (как Вы выражаетесь, я предпочитаю называть это утверждением о верности арифметики):
$(\forall p)((A \vdash p) \rightarrow p)$

Так что эта теория может смело использовать в своих выводах любую теорему арифметики.

Alexey Romanov в сообщении #223950 писал(а):

2) рекурсивно аксиоматизируема;

Конечно, куда ж мы без этого. Иное и "теорией"-то было бы стыдно назвать...

Alexey Romanov в сообщении #223950 писал(а):

3) следовательно, по теореме Гёделя о неполноте, её арифметическая часть неполна.

Разумеется. В ней, конечно же, тоже есть недоказуемое истинное утверждение. Но это уже не теорема Гудстейна.

Alexey Romanov в сообщении #223950 писал(а):

Если она описывает только стандартные натуральные числа, то по теореме Гёделя о полноте, её арифметическая часть полна.

Или о теореме о полноте Вы тоже не желаете слышать?

Очевидно, она описывает не только "стандартные натуральные числа". Но это всё, что нас интересует при доказательстве теоремы Гудстейна.

Alexey Romanov в сообщении #223950 писал(а):

Меня легко опровергнуть, если Вы правы: Вам достаточно просто явно выписать все аксиомы метатеории и предъявить доказательство.

Ну Вы скажете тоже. Предлагаете на формальном языке мне расписать все определения стандартного синтаксиса арифметики и т. д., только для того, чтобы продемонстрировать, что ничего другого при выводе не использовалось?

Alexey Romanov в сообщении #223950 писал(а):

Без всяких "очевидно, что" -- просто доказательство в логике первого порядка.

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

Alexey Romanov в сообщении #223950 писал(а):

Его можно будет механически проверить и выписать Вам премию за опровержение одной из теорем Гёделя (уж какой из них, придётся разбираться отдельно).

Пока что я никаких теорем Гёделя не опровергал.

[Alexey Romanov]

epros в сообщении #223957 писал(а):

Ну Вы скажете тоже. Предлагаете на формальном языке мне расписать все определения стандартного синтаксиса арифметики и т. д., только для того, чтобы продемонстрировать, что ничего другого при выводе не использовалось?

Я предлагаю Вам вспомнить, что любая аксиоматизация стандартного синтаксиса арифметики и т. д. в логике первого порядка будет неполна.

epros в сообщении #223957 писал(а):

Пока что я никаких теорем Гёделя не опровергал.

Из Вашего утверждения и теорем Гёделя выводится противоречие (с помощью тех рассуждений, которые Вы не желаете слушать, но они от этого никуда не деваются).

epros в сообщении #223957 писал(а):

Что касается того, есть ли для этой функции в арифметике общая формула

Не в арифметике, а в Вашей метатеории.

[epros]

Alexey Romanov в сообщении #223966 писал(а):

Я предлагаю Вам вспомнить, что любая аксиоматизация стандартного синтаксиса арифметики и т. д. в логике первого порядка будет неполна.

Что Вы имеете в виду? Первую теорему Гёделя о неполноте? Так я её не отрицаю. Давайте лучше по существу: В чём претензии к моему доказательству?

Alexey Romanov в сообщении #223966 писал(а):

epros в сообщении #223957 писал(а):

Пока что я никаких теорем Гёделя не опровергал.

Из Вашего утверждения и теорем Гёделя выводится противоречие (с помощью тех рассуждений, которые Вы не желаете слушать, но они от этого никуда не деваются).

Я не желаю слушать выводы на основе теории моделей, ибо ни в формулироке теоремы Гудстейна, ни в моём доказательстве, ни даже в доказательстве первой теоремы Гёделя о неполноте теория моделей не используется. Если Вы даже продемонстрируете какое-то противоречие вполне коррекными рассуждениями (в чём я лично сомневаюсь), это может заставить меня усомниться в используемой Вами теории моделей, но уж никак не в корректности доказательства, полученного без её использования.

Давайте лучше по существу - о претензиях к приведённому доказательству.

Alexey Romanov в сообщении #223966 писал(а):

epros в сообщении #223957 писал(а):

Что касается того, есть ли для этой функции в арифметике общая формула

Не в арифметике, а в Вашей метатеории.

В моей метатеории она определена ровно таким образом, как записано (т.е. рекурсивно, двумя утверждениями). Синтаксически, конечно же, это не арифметические формулы, но синтаксис вполне однозначный. Какие проблемы?

Опять же, хотите, чтобы я на Си написал процедуру, которая по этому определению построит арифметическую формулу для любого заданного $k$? Можно даже продемонстрировать, как для какого-нибудь $k=15$ будет напечатана формула из 15-ти этажей возведения в степень.

Вот Вам пример для $k=3$:
$\Lambda_{3}(n, m_1, m_2, m_3) = m_3 + n^{m_2 + n^{m_1}}$

Что тут может не устраивать?

[Alexey Romanov]

epros в сообщении #224002 писал(а):

Первую теорему Гёделя о неполноте? Так я её не отрицаю.

А теорему о полноте?

epros в сообщении #224002 писал(а):

Давайте лучше по существу: В чём претензии к моему доказательству?

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

Кстати, как выглядит доказательство того, что теорема Гудстейна недоказуема в арифметике Пеано без применения теории моделей?

-- Пн июн 22, 2009 18:02:36 --

Сформулирую этот вопрос более общим. Пусть у нас есть теория $T$ и предложение на том же языке $p$. Что Вы готовы принять в качестве доказательства, что $p$ не является теоремой $T$?

[epros]

Alexey Romanov в сообщении #224013 писал(а):

А теорему о полноте?

О полноте классического исчисления предикатов? А причём тут это?

Alexey Romanov в сообщении #224013 писал(а):

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

Давайте конкретнее: какие "факты" я использую, которые не доказаны? Пока что Вы только придрались к определению функции $\Lambda$, которая на самом деле деле есть просто общая форма записи для некой последовательности арифметических функций.

Alexey Romanov в сообщении #224013 писал(а):

Кстати, как выглядит доказательство того, что теорема Гудстейна недоказуема в арифметике Пеано без применения теории моделей?

Не интересуюсь. Я не возражаю против доказательства в теории моделей. В конце концов, если даже оно неверно, для моих выводов это ничего не изменит.

Alexey Romanov в сообщении #224013 писал(а):

Сформулирую этот вопрос более общим. Пусть у нас есть теория $T$ и предложение на том же языке $p$. Что Вы готовы принять в качестве доказательства, что $p$ не является теоремой $T$?

Я ожидал более конкретных вопросов, а не более общих.

Да что угодно, лишь бы без сомнительных аксиом и строго. Пример: Гёделевское доказательство несуществования доказательства предложения $G$. Доказывается равносильность $G$ утверждению о собственной недоказуемости, и далее из утверждения об истинности теории выводится его недоказуемость в теории. И никаких теорий моделей, кстати.

[Alexey Romanov]

epros в сообщении #224044 писал(а):

Давайте конкретнее: какие "факты" я использую, которые не доказаны? Пока что Вы только придрались к определению функции $\Lambda$, которая на самом деле деле есть просто общая форма записи для некой последовательности арифметических функций.

На языке метатеории мы можем определить предикат $F(\sigma, n)\equiv \sigma$ -- -- формула c $n$ свободными переменными.

Для формализации статьи Вам понадобится утверждение, что для любого $k$ функция $\Lambda_k$ записывается некоторой формулой в арифметике, то есть, на языке метатеории,

$\forall k ~ \exists \sigma ~ F(\sigma, k + 2) \wedge A \vdash ???$

Что Вы предлагаете написать на месте ??? В доказательстве в логике первого порядка участвуют только формулы логики первого порядка, так что этому шагу соответствует конкретная формула.

epros в сообщении #224044 писал(а):

Гёделевское доказательство несуществования доказательства предложения $G$.

Ошибаетесь. Гёдель доказал, что если $A$ непротиворечива, то $G$ недоказуемо в $A$. Но непротиворечивость $A$ означает только то, что $A \nvdash 0 = S(0)$; а как доказать это?

То, что в мета-теории мы принимаем истинность $A$, нам не поможет: если $A$ противоречива, то и наша метатеория, которая её включает -- тоже.

[epros]

Alexey Romanov в сообщении #224059 писал(а):

На языке метатеории мы можем определить предикат $F(\sigma, n)\equiv \sigma$ -- -- формула c $n$ свободными переменными.

Для формализации статьи Вам понадобится утверждение, что для любого $k$ функция $\Lambda_k$ записывается некоторой формулой в арифметике, то есть, на языке метатеории,

$\forall k ~ \exists \sigma ~ F(\sigma, k + 2) \wedge A \vdash ???$

Что Вы предлагаете написать на месте ??? В доказательстве в логике первого порядка участвуют только формулы логики первого порядка, так что этому шагу соответствует конкретная формула.

Никаких $\ldots \wedge A \vdash ???$. Причём тут вообще это? Выражение $A \vdash ???$ читается как: "??? является теоремой арифметики".

Ваше $F(\sigma, k + 2)$ уже является утверждением о том, что $\sigma$ - формула арифметики с $k+2$ свободными переменными. Поэтому высказывание:
$\forall k \in \mathbb{N} ~ \exists \sigma ~ F(\sigma, k + 2)$
читается как: "Для любого $k$ существует формула арифметики с $k+2$ свободными переменными". Как я понимаю, Вы хотите ещё что-то сказать об этой формуле (продолжить фразу: ", которая ..."). Чем же именно продолжить?

Alexey Romanov в сообщении #224059 писал(а):

Гёдель доказал, что если $A$ непротиворечива, то $G$ недоказуемо в $A$. Но непротиворечивость $A$ означает только то, что $A \nvdash 0 = S(0)$; а как доказать это?

Ничего больше доказывать не надо, речь была именно об этом: "Если арифметика непротиворечива ..."

Alexey Romanov в сообщении #224059 писал(а):

То, что в мета-теории мы принимаем истинность $A$, нам не поможет: если $A$ противоречива, то и наша метатеория, которая её включает -- тоже.

Разумеется. Тем не менее, вывод метатеории о недоказуемости $G$ в арифметике останется выводом метатеории.

Скажу даже более того: Если арифметика омега-противоречива, но непротиворечива, то метатеория, принимающая истинность арифметики, будет уже противоречивой.

[Alexey Romanov]

epros в сообщении #224159 писал(а):

Как я понимаю, Вы хотите ещё что-то сказать об этой формуле (продолжить фразу: ", которая ..."). Чем же именно продолжить?

...Которая записывает функцию $\Lambda_k$.

epros в сообщении #224159 писал(а):

Скажу даже более того: Если арифметика омега-противоречива, но непротиворечива, то метатеория, принимающая истинность арифметики, будет уже противоречивой.

Ошибаетесь. Покажите вывод противоречия из этой метатеории.

[epros]

Alexey Romanov в сообщении #224171 писал(а):

epros в сообщении #224159 писал(а):

Как я понимаю, Вы хотите ещё что-то сказать об этой формуле (продолжить фразу: ", которая ..."). Чем же именно продолжить?

...Которая записывает функцию $\Lambda_k$.

Вот так:
$\forall k \in \mathbb{N} ~ \exists \sigma ~ F(\sigma, k + 2) \wedge \sigma = \Lambda_k$

В конце дописано равенство между значением строковой переменной и значением строковой функции от натурального аргумента.

Цитата:

epros в сообщении #224159 писал(а):

Скажу даже более того: Если арифметика омега-противоречива, но непротиворечива, то метатеория, принимающая истинность арифметики, будет уже противоречивой.

Ошибаетесь. Покажите вывод противоречия из этой метатеории.

Арифметика $A$ омега-противоречива, если в ней есть такая формула $P(n)$, что $\forall n ~ A \vdash P(n)$ (1), но $A \vdash \exists n ~ \neg P(n)$ (2). (Опровержения этого факта нет, точно так же как не опровергнуто $A \vdash 0 = S(0)$).

Если в метатеории принята аксиома истинности арифметики, то из (1) выводится $\forall n ~ P(n)$, а из (2) выводится $\exists n ~ \neg P(n)$. Противоречие.

[Alexey Romanov]

epros в сообщении #224197 писал(а):

в ней есть такая формула $P(n)$, что $\forall n ~ A \vdash P(n)$...

Нет. Правильное определение можете посмотреть в Википедии или в любом хорошем учебнике:
Действительно должно быть $A \vdash \exists n ~ \neg P(n)$, но первое условие нужно заменить на $A \vdash P(0)$, $A \vdash P(1)$, ...

Для метатеории первого порядка эти утверждения далеко не эквивалентны, поскольку она сама может быть $\omega$-противоречивой!

Разумеется, в обычной математике метатеориями первого порядка не ограничиваются.

[epros]

Alexey Romanov в сообщении #224201 писал(а):

epros в сообщении #224197 писал(а):

в ней есть такая формула $P(n)$, что $\forall n ~ A \vdash P(n)$...

Нет. Правильное определение можете посмотреть в Википедии или в любом хорошем учебнике:
Действительно должно быть $A \vdash \exists n ~ \neg P(n)$, но первое условие нужно заменить на $A \vdash P(0)$, $A \vdash P(1)$, ...

Опять "инфинитарная логика"? Не может быть в нормальной теории утверждения бесконечной длины. А если хотим получить утверждение конечной длины, то почему бы не квантифицировать?

Alexey Romanov в сообщении #224201 писал(а):

Для метатеории первого порядка эти утверждения далеко не эквивалентны, поскольку она сама может быть $\omega$-противоречивой!

Я понимаю, что метатеория сама может быть омега-противоречивой, так что выводимость в ней $A \vdash P(n)$ для любого $n$ не эквивалентна выводимости $\forall n ~ A \vdash P(n)$.

Тем не менее, если последнее выводимо в метатеории наряду с $A \vdash \exists n ~ \neg P(n)$ (независимо от омега-противоречивости или омега-непротиворечивости метатеории), разве это не означает омега-противоречивость $A$ с точки зрения этой метатеории?

[Alexey Romanov]

epros в сообщении #224207 писал(а):

Не может быть в нормальной теории утверждения бесконечной длины.

Конечно, не может. Это не одно утверждение, а бесконечный список утверждений.

Заметьте, что метатеорию обычно никто не формализует как теорию в логике первого порядка и это не потому, что лень, а для использования выразительных средств, выходящих за её пределы.

epros в сообщении #224207 писал(а):

разве это не означает омега-противоречивость $A$ с точки зрения этой метатеории?

Да, означает.

Ещё один вопрос: используются ли где-нибудь в Вашем доказательстве частные случаи "аксиомы истинности" для тех $p$, которые недоказуемы в $A$? Насколько я вижу, нет.

[epros]

Alexey Romanov в сообщении #224217 писал(а):

Ещё один вопрос: используются ли где-нибудь в Вашем доказательстве частные случаи "аксиомы истинности" для тех $p$, которые недоказуемы в $A$? Насколько я вижу, нет.

Во-первых, в приведённой статье аксиома истинности арифметики вообще не используется, ибо моей задачей было доказать $\forall n \in \mathbb{N} ~ A \vdash G(n)$, а не $\forall n \in \mathbb{N} ~ G(n)$.

Во-вторых, я не понял про "частный случай": Если высказывание $p$ недоказуемо в арифметике, т.е. $A \nvdash p$, то для него высказывание $(A \vdash p) \rightarrow p$ будет истинным, независимо от наличия или отсутствия в метатеории аксиомы истинности арифметики.

Alexey Romanov в сообщении #224217 писал(а):

epros в сообщении #224207 писал(а):

Не может быть в нормальной теории утверждения бесконечной длины.

Конечно, не может. Это не одно утверждение, а бесконечный список утверждений.

Тогда встаёт вопрос о том, в какой теории сформулировано утверждение о существовании этого "бесконечного списка утверждений".

Alexey Romanov в сообщении #224217 писал(а):

Заметьте, что метатеорию обычно никто не формализует как теорию в логике первого порядка и это не потому, что лень, а для использования выразительных средств, выходящих за её пределы.

С этим надо быть очень осторожным. В логиках более высоких порядков (и в инфинитарной тоже) могут оказаться выводимыми очень странные вещи, если и не прямо абсурдные, то по крайней мере не поддающиеся разумной интерпретации. С моей точки зрения это где-то близко к "путанию уровней рефлексии", о котором говорил Свободный Художник: как в том парадоксе заключённого, которому говорят, что его казнят на следующей неделе, но день казни останется для него неожиданностью до последнего момента.

P.S. Заметьте, в приведённой статье я тоже не формализую метатеорию в логике первого порядка. Это Вы меня сейчас заставляете это делать (и я полагаю, что при необходимости это сделать можно).

[Alexey Romanov]

epros в сообщении #224232 писал(а):

Если высказывание $p$ недоказуемо в арифметике, т.е. $A \nvdash p$, то для него высказывание $(A \vdash p) \rightarrow p$ будет истинным, независимо от наличия или отсутствия в метатеории аксиомы истинности арифметики.

Если $A \nvdash p$, это совсем не значит, что это можно доказать в метатеории (опять-таки, в любой фиксированной метатеории первого порядка). Более того, классическим методом доказательства в метатеории $A \nvdash p$ является предъявление модели $A$, в которой ложно $p$. У Вас этого ресурса нет.
Напомню, что первая теорема Гёделя имеет вид не $A \nvdash G$, а $A \nvdash 0 = 1 \rightarrow A \nvdash G$.

epros в сообщении #224232 писал(а):

в какой теории сформулировано утверждение о существовании этого "бесконечного списка утверждений".

В неформальной метатеории.

epros в сообщении #224232 писал(а):

Заметьте, в приведённой статье я тоже не формализую метатеорию в логике первого порядка. Это Вы меня сейчас заставляете это делать (и я полагаю, что при необходимости это сделать можно).

Мои возражения начались вот с этого:

epros в сообщении #223333 писал(а):

Для доказательства $(\forall n \in \mathbb{N})(A \vdash G(n))$ нужно стандартное исчисление предикатов первого порядка + индукция по натуральным числам.