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

[epros]

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

Вы спорите не только со мной, но и с приведённой мной цитатой из Миши Вербицкого. Что Вы скажите насчёт программы генерирующей доказательство в $ZFC$?

Что именно цитата?

И какая разница чем генерируется доказательство?

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

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

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

Цитата:

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

Формальная теория, в которой доказывается, что все люди - негры неадекватна описываемой ей реальности.
Допустим $ZFC$ неадекватна реальности натуральных чисел. Но арифметика Пеано адекватна? Найдя решение уравнения Ферма, мы можем доказать а арифметике Пеано, что решение существует. Согласны ли Вы с тем что любое утверждение, доказанное в арифметике Пеано, можно доказать в $ZFC$?

Неплохо бы услышать мнение других специалистов по этому вопросу.

[grizzly]

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

Неплохо бы услышать мнение других специалистов по этому вопросу.

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

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

Понимаете grizzly, предмет нашего спора не филосовский, а математический. Здесь либо я прав, либо epros.
Дано, что в $ZFC$ cуществует доказательство, что некоторое диофантово уравнение не имеет решений. Я утверждаю, что если это уравнение имеет решение, то $ZFC$ противоречива. Утверждение о противоречивости $ZFC$ можно перевести на язык арифметики. Если сделать это, то моё утверждение является арифметическим утверждением, которое можно доказать.
А уважаемый epros считает, что доказать это нельзя.

[Xaositect]

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

Я же только что доказал, что если $ZFC$ непротиворечива и из неё следует ВТФ, то ВТФ справедлива.

Если углубляться в тонкости, то формулировка будет "Если $\mathrm{ZFC}$ непротиворечива и из нее следует ВТФ в стандартной модели арифметики, то ВТФ истинна в стандартной модели". Из этого не следует доказуемость ВТФ в $\mathrm{PA}$.

epros, я так понимаю, не видит смысла рассматривать можели арифметики в $\mathrm{ZFC}$, потому что $\mathrm{ZFC}$ представляется ему более сомнительной, чем сама арифметика.

[epros]

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

Согласны ли Вы с тем что любое утверждение, доказанное в арифметике Пеано, можно доказать в $ZFC$?

Да, согласен. Но это не значит, что всякое утверждение о натуральных числах, доказанное в ZFC, доказуемо в арифметике.

Xaositect хорошо об этом сказал. И да, это верно: Я считаю ZFC более сомнительной, чем арифметика. Просто потому что чем больше взятых с потолка предположений аксиом, тем сомнительнее теория.

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

Уважаемый Xaositect, я не имел ввиду утверждение, которое Вы озвучили.
Пусть $A$ - формула "ВТФ - ложна" и $a$ - число Гёделя этой формулы.
Тогда $A \rightarrow Bew(a)$ является теоремой арифметики $PA$ (по моему скромному мнению).

.

[elektrybalt]

arseniiv в сообщении #953235 писал(а):

Да, полугруппа явно списана с чего-то реального.

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

[Xaositect]

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

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

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

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

Если найдёте, дайте мне, пожалуйста, какую-нибудь ссылку, чтобы я мог в этом убедиться.
Если это так, то уважаемый epros частично прав, хотя по большому счёту он всё равно не прав.
Не думаю, что надо сильно расширять PA, чтобы получить теорему $A \rightarrow Bew(a)$.
$ZFC$ здесь ни при чём.
Все эти нестандартные модели с числами после сегмента $1, 2, 3, ...$ не имеют ничего общего с нашим представлением о натуральных числах.

[Xaositect]

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

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

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

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

Это неверно, извиняюсь. Например, $A\to Bew(a)$ доказуемо для любой формули $A$ вида $Bew(n)$, но ясно, что не все такие формулы опровержимы или доказуемы.

Однако, существуют недоказуемые формулы, для которых это утверждение не является теоремой, например, утверждения истинные в стандартной модели, но недоказуемые. ВТФ, если она независима от $PA$, к таким относится, как и любое независимое $\Pi_1^0$-утверждение.

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

Все эти нестандартные модели с числами после сегмента $1, 2, 3, ...$ не имеют ничего общего с нашим представлением о натуральных числах.

Зато имеют непосредственное отношение к теории PA.

[epros]

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

хотя по большому счёту он всё равно не прав.

А в чём этот большой счёт?

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

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

А в чём этот большой счёт?

Это не имеет значения, поскольку это моё личное мнение. Считайте, что я ничего не сказал.

(Оффтоп)

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

Уважаемый epros, если я так начну, будет хорошо по вашему мнению:

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

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

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

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

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

Система аксиом математической теории формально определяет основные понятия теории.
Если это фундаментальные математические понятия, такие как в приведённом примере, то формальное определение этих понятий должно соответствовать нашему представлению о них.
Как мы увидим в дальнейшем, формальное определение фундамантальных математических понятий не исчерпывает наше представление о них.
Поэтому при необходимости к системе аксиом теории добавляют новые очевидные аксиомы.

В других теориях формальное определение основных понятий формирует наше представление о них.
В таких теориях система аксиом может содержать неочевидные аксиомы.
Речь идёт не только о математических, но и о физических теориях.
Например, специальная теория оносительности Эйнштейна основана на двух аксиомах, одной из которых является неочевидная аксиома о постоянности скорости света в инерциальных системах отчёта.
Следствия из этой теории перевернули наши представления о пространстве и времени.

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

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

Однако, существуют недоказуемые формулы, для которых это утверждение не является теоремой, например, утверждения истинные в стандартной модели, но недоказуемые. ВТФ, если она независима от $PA$, к таким относится, как и любое независимое $\Pi_1^0$-утверждение.

Утверждение $A$ "ВТФ - ложна" не является истинной в стандартной модели. Это что-нибудь меняет?
Является ли $A$ $\Pi_1^0$-утверждением?
Извините, может я когда-то это и знал, но сейчас не помню, что такое $\Pi_1^0$-утверждение.

[Xaositect]

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

Утверждение $A$ "ВТФ - ложна" не является истинной в стандартной модели. Это что-нибудь меняет?

В каком смысле? Я лично ничего против ZFC и представления натуральных чисел как стандартной модели PA в ZFC не имею, для меня доказательство, которое, по общему мнению, формализуемо в ZFC, вполне убедительно, хотя, конечно, чем меньше используется неприятных вещей, тем лучше. Я просто против того, что классическая логика и ZFC - это единственная система оснований, на которую надо обращать внимание.

$\Pi_1^0$-утверждения - это утверждения вида $\forall x_1 \forall x_2 \dots \forall x_n P(x_1,x_2,\dots,x_n)$. ВТФ таким является. Отрицание ее, наоборот, является $\Sigma_1^0$-утверждением, с кванторами существования.