Вопрос по основаниям математики

[epros]

Someone писал(а):

Padawan писал(а):

можно ли доказать любую истинную формулу арифметики при помощи аксиом теории множеств.

Вряд ли.

А разве нельзя? Вроде бы можно доказать, что теория множеств (в аксиоматике ZF) содержит в себе аксиоматику Пеано (т.е. формальную арифметику). Стало быть доказуемое в арифметике должно автоматически являться доказуемым в теории множеств.

PAV писал(а):

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

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

Итак, 1-ую теорему Гёделя формально можно записать так:
$\overline{(T | G)} \leftrightarrow G$
Здесь $T | G$ означает утверждение о доказуемости $G$ в теории $T$ (не нашёл значка для более адекватной замены вертикальной черты). Соответственно, горизонтальная черта над этим утверждением означает его отрицание. Т.е. формула читается так: "Высказывание $G$ равносильно его недоказуемости в теории $T$".

В понимании Гёделя "непротиворечивость" теории - это когда любое доказуемое в ней высказывание является истинным. Т.е.:
$(T | X) \to X$ для любого высказывания $X$.

Я-то сам с таким пониманием непротиворечивости не согласен. По-моему, это есть просто утверждение о том, что метатеория включает как минимум всю аксиоматику теории $T$. В моём понимании непротиворечивость - это вот что:
$(T | \overline{X}) \to \overline{(T | X)}$ - если высказывание опровержимо в теории, то оно не должно быть в ней доказуемо.
Но давайте пока примем "непротиворечивость" в первом смысле.

Тогда из предположения $T | G$ выводится $G$, а следовательно - $\overline{(T | G)}$, что является противоречием с исходным предположением. Надо заметить, что конструктивная логика (без законов исключённого третьего и снятия двойного отрицания) не отвергает способ опровержения высказывания путём сведения его к противоречию. Т.е. из $A \to \overline{A}$ следует $\overline{A}$. Другое дело, что таким образом нельзя доказать позитивное утверждение, т.е. из $\overline{A} \to A$ будет следовать $\overline{\overline{A}}$, но не $A$.

Таким образом, доказано отрицание исходного предположения - $\overline{(T | G)}$, а значит и $G$.

[Amigo]

Уважаемый PAV , можно ли резюмировать Ваш ответ так:
Предположив ложность исходного утверждения мы приходим к выводу,что данное
утверждение должно быть доказуемым в S. Следовательно мы в системе S можем построить доказательство, которое доказывает ложное утверждение. Но в силу того, что данная система
не противоречива,этого быть не может. Приведённое только, что доказательство обладает таким свойством, что его нельзя формализовать в самой системе S. Потому как если бы это было возможно, мы бы получили, что система S противоречива, что противоречит предположению о не противоречивости системы S?

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

Re: Вопрос по основаниям математики

epros писал(а):

В понимании Гёделя "непротиворечивость" теории - это когда любое доказуемое в ней высказывание является истинным. Т.е.:
$(T | X) \to X$ для любого высказывания $X$.

Я-то сам с таким пониманием непротиворечивости не согласен. По-моему, это есть просто утверждение о том, что метатеория включает как минимум всю аксиоматику теории $T$. В моём понимании непротиворечивость - это вот что:
$(T | \overline{X}) \to \overline{(T | X)}$ - если высказывание опровержимо в теории, то оно не должно быть в ней доказуемо.

Когда произносится слово "опровержимо" сразу же представляется некоторый процес,
который даёт этот результат. Но что предсавляет собой этот процес размышления?
Не представляет ли он собой замаскированную процедуру доказательства ложного утверждения? Если так, то Ваше понимание приводит к абсурду. Если же под словом
"опровержимо" понимается просто "ложное утверждение" - то Ваше понимание совпадает
с Гёделевским.

[epros]

Amigo писал(а):

Когда произносится слово "опровержимо" сразу же представляется некоторый процес,
который даёт этот результат. Но что предсавляет собой этот процес размышления?

Этот процесс называется "формальный вывод". См. здесь, в разделе "Формальное доказательство". Цитирую:
"Формальным выводом называется конечное упорядоченное множество строк, написанных на формальном языке, таких, что каждая из них либо является аксиомой, либо получена из предыдущих строк применением одного из правил вывода".

Вот когда мы получили формальный вывод, последней строкой которого является высказывание $\overline{X}$, это и значит что мы получили опровержение $X$ в этой теории.

Amigo писал(а):

Не представляет ли он собой замаскированную процедуру доказательства ложного утверждения? Если так, то Ваше понимание приводит к абсурду. Если же под словом
"опровержимо" понимается просто "ложное утверждение" - то Ваше понимание совпадает
с Гёделевским.

Не понимаю. Что такое "ложное утверждение"? $0=1$ - это ложное утверждение? Как в этом убедиться? Вроде бы, в арифметике доказывается противоположное утверждение, но является ли это подтверждением того, что данное утверждение - ложно? Очевидно, это было бы так, если бы мы знали, что арифметика непротиворечива. Но это опять возвращает нас к вопросу о том, что такое противоречивость теории.

Я предложил выше определение непротиворечивости. Если ему следовать, то противоречивая теория - это такая теория, в которой есть такое высказывание, которое и опровержимо и доказуемо одновременно.

[STilda]

epros писал(а):

Не понимаю. Что такое "ложное утверждение"?

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

[PAV]

Да, разумеется, зависимость от системы также есть.

А утверждение $0=1$ в стандартной арифметике ложно по определению.

[bot]

quote="STilda"]Насколько я понимаю, ложность и истинность утверждения также зависит от системы, в которой мы его рассматриваем.[/quote]
Угу, по сути все теоремы в математике - это импликации. Вот только посылки в них замучаешься выписывать, чтобы всё честно было.
А что касается равенства $0=1$, почему ему бы не быть, если рассматриваемая теория допускает одноэлементную модель и в то же время требует существование спецэлементов 0 и 1? Примером может быть теория колец с нейтральным элементом по умножению. Поле в качестве примера тут брать нельзя - в этой теории нет одноэлементных моделей, впрочем если захочется, то опять можно - надо только убрать аксиому $0\ne 1$ и возникнет слегка другая теория.

P.S. Яркину это не читать!

[epros]

PAV писал(а):

Да, разумеется, зависимость от системы также есть.

А утверждение $0=1$ в стандартной арифметике ложно по определению.

Гёдель различает "истинность" и "доказуемость в теории". В частности, построенное им выражение $G$ "истинно", но "недоказуемо в теории". Соответственно, он должен различать "ложность" и "опровержимость в теории".

Я-то с Вами согласен: ложность "в теории" - это ни что иное, как доказанность противоположного утверждения (отрицания). Но если мы предполагаем противоречивость теории, то ни о какой "ложности в теории" говорить не приходится, ибо доказать в такой теории можно абсолютно любое утверждение: т.е. и $0=1$, и $0 \ne 1$ одновременно.

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

Указанное мной условие непротиворечивости теории не нуждается в понятиях истинности или ложности "вообще" (т.е. вне теории). Оно оперирует только понятиями доказуемости и опровержимости в теории. Проблема в том, что с использованием этого условия, похоже, никак не удастся доказать истинность Гёделевского высказывания $G$ (а значит и вторая теорема о неполноте оказывается под вопросом).

[Someone]

Стандартно противоречивость теории означает, что в ней выводимы (доказуемы) все формулы. Если язык теории содержит знак отрицания, то это равносильно тому, что в теории доказуемы некоторое утверждение и его отрицание.

[luitzen]

Someone писал(а):

…это равносильно тому, что в теории доказуемы некоторое утверждение и его отрицание.

Ну, не совсем так.

Есть всякие паранепротиворечивые системы, в которых, гм, из противоречия не следует всё, что угодно. Иными словами, там может быть так, что некоторое высказывание выводимо вместе с его отрицанием, но не обязательно выводима произвольная формула.

[Someone]

luitzen писал(а):

Есть всякие паранепротиворечивые системы, в которых, гм, из противоречия не следует всё, что угодно. Иными словами, там может быть так, что некоторое высказывание выводимо вместе с его отрицанием, но не обязательно выводима произвольная формула.

Я о них ничего не говорю.

[Yarkin]

bot писал(а):

P.S. Яркину это не читать!

Зачем зря тратить время. Если Ваши рассуждение не связаны с законами природы, они всегда могут быть и доказуемыми и не доказуемыми. Попробуйте опровергнуть неравенство треугольника или теорему косинусов. Или выведите все это из теории множеств. Почти четыре века математики не могли разобраться на каком же множестве задана ВТФ, пока это не показал Яркин. Желаю успехов.

[нг]

Yarkin писал(а):

Почти четыре века математики не могли разобраться на каком же множестве задана ВТФ

Почти четыре века назад Пьер Ферма (совпадение?!) написал, что в $\mathbb N$.

[epros]

Someone писал(а):

Стандартно противоречивость теории означает, что в ней выводимы (доказуемы) все формулы. Если язык теории содержит знак отрицания, то это равносильно тому, что в теории доказуемы некоторое утверждение и его отрицание.

Загадка состоит в том, как из такой непротиворечивости вывести истинность Гёделевского выражения $G$. Ведь на этом (что из непротиворечивости теории следует недоказуемая в ней формула) основана вторая теорема Гёделя о неполноте - что в теории недоказуема её собственная непротиворечивость. То, что $G$ следует из $\forall X (T | X \to X)$ - это понятно. Но причём тут непротиворечивость - непонятно.