Логика и методология математики.

[dmitgu]

Феликс Шмидель в сообщении #955864 писал(а):

Следовательно, если утверждение $A$ истинно в стандартной модели арифметики, то оно доказуемо в арифметике Пеано (первого порядка).

Тут не согласен. Теория Пеано не полна. И где она не полна - там можно расширять или в сторону стандартной арифметики или в другую (тогда это необратимо). И, кстати, это касается и диофантовых уравнений.

[Феликс Шмидель]

А с тем, что если утверждение $A$ истинно в любой модели арифметики, то оно доказуемо в арифметике Пеано (первого порядка) Вы согласны?

[dmitgu]

Феликс Шмидель в сообщении #955866 писал(а):

А с тем, что если утверждение $A$ истинно в любой модели арифметики, то оно доказуемо в арифметике Пеано (первого порядка) Вы согласны?

А что такое "любая модель арифметики"? На всякий случай не согласен )

З.Ы. И вот что я подумал - вот возьмем диофантово уравнение, которое не имеет корней и неразрешимо в теории Пеано (такие есть). Тогда теория не полна ни на $A$ (утверждение о решаемости этого уравнения) ни на $Prov(A)$. Расширяем его утверждением $\neg Prov(A)$ - из него ведь никак не следует $\neg A$, если это как-то пытаться "здравый смысл" включить. Потому что $\neg Prov(Aks, A)$ (оно ведь зависит от акиом) утверждает что в каких-то аксиомах не доказывается $A$. Но это действительно так. То есть, $\neg A$ у нас как не доказывалось, так и не доказывается и мы можем расширить теорию на $A$. И замечательно будет истинным $A \wedge \neg Prov(A)$. Это не доказательство, но близко к тому ). Это же отрицание импликации, которого - если тут нет подводных камней - можно добиться. В определенной непротиворечивой теории.

[Феликс Шмидель]

На вопрос, что такое модель $M$ ответим небольшим отрывком из замечательной статьи Максима Гумина: "Знакомство с математической логикой и теорией алгоритмов: математика и философия теорем Гёделя о неполноте".

Цитирую с небольшими изминениями:

Цитата:

Чтобы можно было говорить об истинности предложений, нужно каким-то образом
интерпретировать входящие в сигнатуру пропозициональные и функциональные символы, а также определить, элементам какого множества соответствуют переменные.
Пусть $S$ произвольная сигнатура языка первого порядка. Для того, чтобы задать интерпретацию $I$ сигнатуры, необходимо:
1. Указать некоторое непустое множество $M$, называемое носителем интерпретации.
2. Каждому предикатному символу валентности $k$ поставить в соответствие $k$-местный предикат, т.е. отображение $M^k \rightarrow \{0, 1\}$.
3. Каждому функциональному символу валентности $k$ поставить в соответствие функцию $k$ переменных, т.е. отображение $M^k \rightarrow M$.

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

[dmitgu]

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

[Феликс Шмидель]

dmitgu в сообщении #955867 писал(а):

Расширяем его утверждением $\neg Prov(A)$ - из него ведь никак не следует $\neg A$, если это как-то пытаться "здравый смысл" включить.

Я не согласен, что никак не следует. Ведь $A$ это не любое утверждение, а утверждение определённого вида. Для такого $A$ может следовать. Это совсем не доказательство.
Подождём, что скажет уважаемый Xaositect.

[dmitgu]

Феликс Шмидель в сообщении #955883 писал(а):

Я не согласен, что никак не следует. Ведь $A$ это не любое утверждение, а утверждение определённого вида. Для такого $A$ может следовать. Это совсем не доказательство.

Гм... Пожалуй, тут я ошибся, действительно. Все же если у нас есть $\neg Prov(Aks, A)$ и $Aks$ - аксиомы Пеано, то наверно как-то можно получить $\neg A$, когда речь идет о диофантовых уравнениях. Потому что при наличии корней доказуемость была бы, а вот ее отсутствие - говорит об охвате бесконечности вариантов. Так что все же похоже $A \wedge \neg Prov(A)$ не доказывается. Но и это тоже не доказательство, строго говоря.

[Феликс Шмидель]

dmitgu в сообщении #955881 писал(а):

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

Модели разные. Стандартная модель содержит только числа $1, 2, 3, ...$, а нестандартные модели содержат эти числа и "нестандартные" числа, которые больше всех чисел $1, 2, 3, ...$. Эти "нестандартные" числа принадлежат сегментам которые в смысле порядка похожи на множество всех целых (включая отрицательные) чисел. Я не углублялся в эти модели и знаю о них понаслышке. Я так понял, не знаю правильно ли, что множество этих "нестандартных" сегментов так же плотно, как множество рациональных чисел.

[dmitgu]

А, понятно. Не на слуху, наверно это что-то для развлечения математических умов.

[Феликс Шмидель]

dmitgu в сообщении #955892 писал(а):

А, понятно. Не на слуху, наверно это что-то для развлечения математических умов.

Если бы. Думаю, что уважаемый epros хорошо понимает, что
утверждение $A \rightarrow Prov(#A)$ истинно в стандартной модели. Но для него этого не достаточно, чтобы считать его истинным (независимо от того является ли это утверждение теоремой арифметики Пеано). Для того, что убедить его в истинности этого утверждения нужно доказать, что и в нестандартных моделях оно истинно. Хотя нестандартные модели совершенно не соответствуют нашему представлению о целых положительных числах.
Для него система аксиом Пеано важнее этого представления.
По-моему это формализм, который не даёт видеть.

[dmitgu]

Феликс Шмидель в сообщении #955925 писал(а):

утверждение $A \rightarrow Prov(#A)$ истинно в стандартной модели.

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

З.Ы. А какая цель у доказательства этой импликации? Может - если даже она и окажется истинной - в дальнейших шагах к цели (какой?) будут очевидные непреодолимые проблемы и лучше сразу это узнать и сэкономить время на долгий путь с отрицательным результатом?

[epros]

Феликс Шмидель в сообщении #955778 писал(а):

Я не считаю преимуществом логики второго порядка замечание уважаемого epros о том, что она знает ответ на вопрос об истинности континуум-гипотезы.

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

Феликс Шмидель в сообщении #955811 писал(а):

Получается, что Вы, как и уважаемый epros, сомневаетесь в истинности совершенно очевидного утверждения $A \rightarrow Prov(#A)$ (где $A$ утверждение вида: $A = \exists x_1, ..., x_k: P(x_1, ..., x_k)=0$ о существовании решений диофантового уравнения $P(x_1, ..., x_k)=0$).
И это после того, как я объяснил: имея целые положительные числа $x_1, ..., x_k$, удовлетворяющие уравнению $P(x_1, ..., x_k)=0$, можно построить доказательство утверждения $A$.

Вы меня не услышали. У нас, вообще говоря, нет никаких чисел $x_1, ..., x_k$. У нас есть только утверждение некой теории, что эти числа существуют.

Знаете, что такое неконструктивное доказательство? Это когда, например, у нас в PA какая-нибудь ВТФ неразрешима, а мы берём теорию с дополнительной аксиомой: PA+A, где A = «Существуют числа, нарушающие ВТФ», и в этой теории доказываем ложность ВТФ. Заметьте, что самих чисел, нарушающих ВТФ, мы в итоге не узнали.

Это я к тому, что дополнительная аксиоматика, позволяющая доказать или опровергнуть ВТФ, не делает доказательство убедительнее. Поэтому доказательство ВТФ в ZFC с моей точки зрения менее убедительно, чем доказательство в PA.

[Феликс Шмидель]

dmitgu в сообщении #955931 писал(а):

З.Ы. А какая цель у доказательства этой импликации? Может - если даже она и окажется истинной - в дальнейших шагах к цели (какой?) будут очевидные непреодолимые проблемы и лучше сразу это узнать и сэкономить время на долгий путь с отрицательным результатом?

Цель простая: обосновать использование всей мощи теории множеств для доказательства арифметических утверждений. Это в любом случае общепринятая математическая практика.
Но уважаемый epros сказал, что от теории множеств нулевая польза, что аксиомы теории множеств это взятые с потолка предположения, и истинность доказанных с использованием теории множеств арифметических утверждений сомнительна.
Если принять истинность утверждения $A \rightarrow Prov(#A)$, то можно строго показать что из доказательства утверждения "не $A$" с использованием теории множеств, если она непротиворечива, следует, что утверждение "не $A$" истинно.
В частности, ВТФ истинна, поскольку Уайлз доказал ВТФ в расширении теории множеств $ZFC$.
Кроме этого, я пытаюсь в этой теме разобраться в основаниях математики, а основания математики включают долю философии.
Я считаю, что истинность арифметических утверждений определяется нашим представлением о числах $1, 2, 3, ...$ и мы вправе принимать новые аксиомы в дополнение к аксиомам Пеано.
А о теории множеств нельзя сказать, чтобы истинность любого утверждения этой теории определялась нашим представлением о множествах. Например, можно считать континуум-гипотезу истинной, а можно ложной.
Это моё понимание в 11-ой версии моего введения в основания математики, которое в 12-ой версии может измениться на противоположное.
Понятно, что мне очень важна критика, которая сильно изменила мои взгляды с 1-ой версии.
Я очень благодарен уважаемому epros и другим участникам за эту критику.
Ещё хотелось бы понять значение истинности импликаций $A \rightarrow Prov(#A)$ в свете теоремы Гёделя о неполноте.

[dmitgu]

Кстати, насчет нестандартных моделей. Все же вернемся к диофантовому уравнению $A$, неразрешимому в Пеано (вместе с $Prov(Aks, A)$, разумеется). Про него ведь можно сказать "Решается!" и расширить этим абсурдом теорию Пеано . Противоречий нет, хоть это уже и не арифметика. Вопрос, станет ли в этой новой теории с аксиомами Aks2 доказано $Prov(Aks, A)$?

Сомневаюсь - хотя новой абсурдной теории и видится то, чего нет (я про корни), но это ещё не значит, что она и доказательство воображает в прошлой теории, которого там нет. То есть, с таким порядком (сначала аксиоматизировать корни, которых нет, а только потом заявить об отсутствии доказательства, которого и правда не было) конъюнкция $A \wedge \neg Prov(Aks, A)$ кажется вполне возможной - после второго расширения на $\neg Prov(Aks, A)$, если $Prov(Aks, A)$ не доказано.

Кстати, и epros передо мной высказался про "воображаемые решения" в том же духе.

Феликс Шмидель в сообщении #955970 писал(а):

что из доказательства утверждения "не $A$" с использованием теории множеств, если она непротиворечива, следует, что утверждение "не $A$" истинно

Дык, если соответствующей аксиомой расширить теорию Пеано, то в случае вывода $Prov(A)$ будет доказано и $A$. Но тут уже точно без всякой импликации. Импликация тут бывает только при истинности $A$ - это теорема Лёба. Она кстати, есть по ссылке на книгу, которую я давал. В той же 16 главе.

[Феликс Шмидель]

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

Знаете, что такое неконструктивное доказательство? Это когда, например, у нас в PA какая-нибудь ВТФ неразрешима, а мы берём теорию с дополнительной аксиомой: PA+A, где A = «Существуют числа, нарушающие ВТФ», и в этой теории доказываем ложность ВТФ. Заметьте, что самих чисел, нарушающих ВТФ, мы в итоге не узнали.

Если утверждение $A$ о существовании решений диофантового уравнения независимо от системы аксиом Пеано, то в стандартной модели арифметики выполняется утверждение "не $A$". Значит теория PA+A не является теорией стандартной арифметики, и то что в ней утверждение $A$ истинно не означает, что оно истинно в стандартной арифметике.
А утверждение $A \rightarrow Prov(#A)$ выполняется в стандартной модели арифметики.
Значит оно истинно в стандартной арифметике.
При этом, утверждение $A$ ложно в стандартной модели, и чисел подтверждающих $A$ действительно нет.
Что заставляет Вас сомневаться в истинности утверждения $A \rightarrow Prov(#A)$? Только то, что это утверждение может не быть теоремой арифметики Пеано?