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

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

Что значит в каком смысле? В прямом: Утверждение $A$ "ВТФ - ложна" не может быть истинной, поскольку Уайлз доказал отрицание этого утверждения. Получается, что утверждение $A$ является утверждением $\Sigma_1^0$, а не $\Pi_1^0$, поскольку $A$ утверждает существование тройки чисел, удовлетворяющих уравнению Ферма.

-- Вт дек 30, 2014 18:31:41 --

А если $A$ является утверждением $\Sigma_1^0$, то что можно сказать об утверждениии $A \rightarrow Bew(#A)$? Оно по-прежнему не является теоремой $PA$? Понимаете, это утверждение настолько очевидно, что если оно не является теоремой $PA$, то надо добавить его в качестве аксиомы.

[Xaositect]

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

А если $A$ является утверждением $\Sigma_1^0$, то что можно сказать об утверждениии $A \rightarrow Bew(#A)$? Оно по-прежнему не является теоремой $PA$?

Является. Я сейчас подумал и понял, что если $\Sigma_1^0$-утверждение $\exists \vec{x} P(\vec{x})$ истинно, то из значений, на которых $P(\vec{x})$ истинно, можно построить доказательство $A$, даже если эти значения нестандартные. Поэтому импликация будет истинна в любой модели, и будет являться теоремой.

Цитата:

Понимаете, это утверждение настолько очевидно, что если оно не является теоремой $PA$, то надо добавить его в качестве аксиомы.

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

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

Xaositect в сообщении #954619 писал(а):

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

Только что Вы сказали, что поняли, что это утверждение является теоремой PA, и после этого говорите, что Гёдель не разрешает??? Обратите внимание, что $A$ - утверждение $\Sigma_1^0$, речь идёт только о таких утверждениях $A\to Bew(#A)$.

[Xaositect]

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

Только что Вы сказали, что поняли, что это утверждение является теоремой PA, и после этого говорите, что Гёдель не разрешает??? Обратите внимание, что $A$ - утверждение $\Sigma_1^0$, речь идёт только о таких утверждениях $A\to Bew(#A)$.

Извините, недопонял. Для таких $A$ утверждение $A\to Bew(\sharp A)$ будет теоремой. Для произвольных не будет.

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

Я немного ошарашен тем, что $A\to Bew(\sharp A)$ является теоремой PA. Вы не ошибаетесь? Получается, что аргумент Миши Вербицкого (он конечно не первый кто это заметил - я знаю об этом много лет) легко формализовать.

Цитата из Вербицкого:

Цитата:

Действительно, предположим, что, исходя из аксиом Пеано, нельзя ни доказать, ни опровергнуть утверждение $Q$ "полиномиальное уравнение $P(t_1, t_2, ..., t_n) = 0$ не имеет целочисленных решений $t_1, ..., t_n$".
В этой ситуации уравнение $P(t_1, t_2, ..., t_n) = 0$ таки не имеет решений, ибо, если бы такое решение было, мы бы могли его подставить в уравнение, и получить теорему "Q ложно".

[Xaositect]

Да, я уверен. Это, оказывается, известная вещь. Если $\Pi_1^0$ утверждение независимо от PA, то оно истинно в стандартной модели.

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

Xaositect в сообщении #954636 писал(а):

Да, я уверен. Это, оказывается, известная вещь. Если $\Pi_1^0$ утверждение независимо от PA, то оно истинно в стандартной модели.

А причём утверждение $\Pi_1^0$, если речь идёт об утверждении $A$, которое $\Sigma_1^0$?

[Xaositect]

Утверждение "Уравнение $P(\vec{x})$ не имеет целочисленных решений" - типа $\Pi_1^0$. Вербицкий говорит в точности то, что я сейчас сформулировал - если мы не можем это ни доказать, ни опровергнуть, то оно решений в стандартной модели действительно нет.
Если рассмотреть отрицание, то есть $\Sigma_1^0$-утверждение "Уравнение имеет корни", то будет обратная теорема - если утверждение истинно, то оно доказуемо.

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

Вам не трудно объяснить, каким образом следует обратная теорема? Кроме того, каким образом можно доказать уважаемому epros, что $A\to Bew(\sharp A)$ является теоремой PA, если модели, основанные на теории множеств для него неубедительны?

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

Новая формулировка начала введения:

Математика занимается определением вводимых понятий, формулировкой утверждений и доказательством их истинности.

Приведём примеры математических понятий: целые положительные числа, cумма двух таких чисел, множество (или совокупность) объектов, понятие принадлежности объекта множеству, прямые линии, понятие параллельности таких линий.

Все эти понятия являются абстракциями реальности и мы понимаем их благодаря нашему опыту с ней.

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

Некоторые из очевидных утверждений берут за основу математической теории и называют аксиомами.
Другие утверждения, очевидные и неочевидные, логически выводятся из аксиом и утверждений, доказанных ранее.
Система аксиом математической теории формально определяет начальные понятия теории.
Если это фундаментальные математические понятия, такие как в приведённом примере, то формальное определение этих понятий должно соответствовать нашему представлению о них.
Но у нас нет полного представления о фундаментальных математических понятиях, поскольку они связаны с бесконечностью.
Лучше всего мы понимаем целые положительные числа $1, 2, 3, ...$.
Как мы увидим в дальнейшем, формальное определение этих чисел не исчерпывает наше представление о них.
Поэтому при необходимости к системе аксиом арифметики добавляют новые очевидные аксиомы.
Что же касается теории множеств или геометрии, то кроме очевидных аксиом принимают и неочевидные.
Обычно к существующей системе аксиом добавляют неочевидное утверждение, которое невозможно ни доказать, ни опровергнуть.
Бесполезно спрашивать истинно ли такое утверждение или нет: можно считать его истинным, а можно ложным.
В результате получаются разные теории с различными системами аксиом, которые формируют наше представление о начальных понятиях теории.
Системы аксиом используются для определения различных математических понятий.
Например, можно определить действительные числа системой аксиом.
Аксиомы в такой системе могут не быть очевидными - они формируют наше представление о начальных понятиях теории.
Продемонстрируем это на примере не математической, а физической теории.
Специальная теория оносительности Эйнштейна основана на двух аксиомах, одной из которых является
неочевидная аксиома о постоянности скорости света в инерциальных системах отчёта.
Следствия из этой теории перевернули наши представления о пространстве и времени.

Начальные понятия теории принято называть "неопределяемыми", а остальные понятия - "определяемыми".
Дело в том, что обычные математические определения определяют понятия, которые не являются начальными.
Аксиоматическое определение начальных понятий теории это особый вид определения.
Определяемые понятия вводятся математическими определениями, которые определяют эти понятия через понятия, введённые ранее.
Любое математическое определение порождает аксиому, которая является утверждением, верным "по определению".
Аксиомы, порождаемые математическими определениями, называются аксиомами определения.

[Xaositect]

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

Вам не трудно объяснить, каким образом следует обратная теорема? Кроме того, каким образом можно доказать уважаемому epros, что $A\to Bew(\sharp A)$ является теоремой PA, если модели, основанные на теории множеств для него неубедительны?

Теорема о полноте для счетных моделей формализуется в той же reverse mathematics в слабой подсистемах арифметики второго порядка $\mathrm{WKL}_0$, которая слабее $\mathrm{PA}$. Так что тот факт, что в любой модели можно из значений $\vec{x}$, для которых выполняется $P(\vec{x})$, построить доказательство утверждения $A = \exists \vec{x} P(\vec{x})$ применением некоторой примитивно-рекурсивной функции, а значит, $A\to Bew(\sharp A)$ истинно в любой модели и, следовательно, является теоремой, тоже формализуется в достаточно слабой метатеории.

[epros]

Xaositect в сообщении #954619 писал(а):

Я сейчас подумал и понял, что если $\Sigma_1^0$-утверждение $\exists \vec{x} P(\vec{x})$ истинно, то из значений, на которых $P(\vec{x})$ истинно, можно построить доказательство $A$, даже если эти значения нестандартные.

Насколько я понимаю, доказательство существования может оказаться неконструктивным. Т. е. «значений, на которых $P(\vec{x})$ истинно» в нашем распоряжении может не оказаться, и нестандартных в том числе.

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

Извините меня, уважаемый Xaositect, но у меня ваше объяснение вызывает много вопросов. Возьмём нестандартную модель арифметики $M$, в которой утверждение $A = \exists \vec{x} P(\vec{x})$ верно. Нам нужно доказать, что в этой модели утверждение $Bew(\sharp A)$ верно. Для этого мы строим доказательство $V$ утверждения $A$. Во-первых что из себя представляет это доказательство? Является ли $V$ доказательством арифметики $PA$ или оно связано с моделью $M$? Как мы находим значения $\vec{x}$ и строим из них доказательство $V$?

[dmitgu]

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

Xaositect в сообщении #953969

писал(а):
$A\to Bew(a)$ будет теоремой тогда и только тогда, когда $A$ доказуема или опровержима в PA, если я не ошибаюсь.

Если найдёте, дайте мне, пожалуйста, какую-нибудь ссылку, чтобы я мог в этом убедиться.

Я правильно понимаю, что Bew(a) - это предикат доказуемости? Если так, то см.
"Вычислимость и логика" Булос, Джеффри. Глава 16.
Дело в том, что в предикате доказуемости уже есть аксиомы, а в $A$ их нет. Если бы была верна импликация, то по правилу контрапозиции $\neg Bew(a) \to \neg A$, но фишка в том, что $\neg Bew(a)$ не может быть доказана в теории 1го порядка с теми же аксиомами, что (неявно) в $Bew(a)$ и не может быть опровергнута - если она не полна на A. А это значит, что можно расширить непротиворечивую теорию на $\neg Bew(a)$ и она останется непротиворечивой. И тогда в случае $\neg Bew(a) \to \neg A$ по правилу вывода MP будет $\neg A$, а это может быть и противоречивое утверждение для данной новой теории. Поэтому и нет $\neg Bew(a) \to \neg A$ а значит нет и $A\to Bew(a)$.

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

Уважаемый dmitgu! Во-первых, спасибо за ссылку.

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

А это значит, что можно расширить непротиворечивую теорию на $\neg Bew(a)$ и она останется непротиворечивой.

Это мне понятно.
Если бы новая теории была противоречивой, то $Bew(#A)$ было бы теоремой прежней теории (т.е. арифметики Пеано). Тогда из пункта (iv) на стр. 244 вашей ссылки следовало бы, что $A$ - теорема прежней теории.
Значит, если $A$ - не зависит от аксиом прежней теории, то $Bew(#A)$ не является её теоремой и новая теория непротиворечива.

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

. И тогда в случае $\neg Bew(a) \to \neg A$ по правилу вывода MP будет $\neg A$, а это может быть и противоречивое утверждение для данной новой теории.

Мы рассматриваем конкретное утверждение $A$ ("ВТФ - ложна"). Каким образом из $\neg A$ следует в новой теории противоречие?