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

[Padawan]

помогите разобраться
1) Существует ли алгоритм, позволяющий любую формулу (без свободных переменных) формальной арифметики переводить в формулу формальной теории множеств, причем так, что если полученная формула выводима в формальной теории множеств, то исходная формула истинна (в естественной интерпретации)?

2) можно ли дополнительно к 1) обеспечить условие, чтобы формула теории множеств, полученная из истинной арифметической формулы, была бы выводима в теории множеств?

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

[Someone]

Padawan писал(а):

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

Вряд ли.

[luitzen]

Padawan писал(а):

помогите разобраться
1) Существует ли алгоритм, позволяющий любую формулу (без свободных переменных) формальной арифметики переводить в формулу формальной теории множеств, причем так, что если полученная формула выводима в формальной теории множеств, то исходная формула истинна (в естественной интерпретации)?
2) можно ли дополнительно к 1) обеспечить условие, чтобы формула теории множеств, полученная из истинной арифметической формулы, была бы выводима в теории множеств?

1) Да.
2) Вряд ли.

[Padawan]

Дело в том, что я прочитал в В.А. Успенский Теорема Геделя о неполноте - М.: Наука 1982, что множество истинных формул арифметики не является рекурсивно перечислимым. Отсюда следует, что на 2) следует дать отрицательный ответ. Более того, ни в какой формальной системе нельзя вывести все истинные формулы арифметики (при естественном условии, что те, которые выводимы, истинны). Мне это показалось очень странным! Потому что про арифметику-то все можно доказать в принципе!

Неужели, есть теоремы (допустим наподобие теоремы Ферма) которые истинны, но которые нельзя доказать...вообще никак. Помогите разобраться.

to luitzen Не могли бы Вы в общих чертах пояснить, почему на 1) ответ да. Как примерно такой алгоритм построить? Или это слишком сложно?

P.S. А еще я прочитал в какой-то книжке, недостаточно ,впрочем, респектабельной, что опыт показывает, что все реальные математические рассуждения могут быть формализованы в аксиоматике теории множеств ZFC ( c аскиомой выбора). Правда ли это, или наврала книжка?

[Amigo]

Padawan писал(а):

Неужели, есть теоремы (допустим наподобие теоремы Ферма) которые истинны, но которые нельзя доказать...вообще никак. Помогите разобраться.

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

[PAV]

Посмотрите этот пост и последующие.

Добавлено спустя 10 минут 16 секунд:

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

[tolstopuz]

Padawan писал(а):

Неужели, есть теоремы (допустим наподобие теоремы Ферма) которые истинны, но которые нельзя доказать...вообще никак. Помогите разобраться.

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

Наверное, в ZFC тоже есть такие утверждения.

[luitzen]

Padawan писал(а):

Как примерно такой алгоритм построить? Или это слишком сложно?

Слишком просто. Пусть, например, переводом всякой арифметической формулы будет $\forall x (x \in x)$.

[Amigo]

Интересно, а можно ли приблизится к доказательству теоремы Гёделя рассуждая по следующей схеме:
1. Мы доказаваем, что существует по крайней мере одно утверждение, которое не проверяемое. То есть не имеет доказательства. Причём нам заранее не известно истинно оно или ложно.
2. Обозначая за М множество всех не проверяемых утверждений,
мы вводим (а может это и не нужно) некоторые дополнительные
условия, которые гарантируют нам существования в множестве
М хотя бы одного истинного утверждения. Отсюда и получится доказательство теоремы Гёделя.

Только у меня проблемма: я не могу придумать не одного принципиально не проверяемого утверждения. Такие вообще есть?

[PAV]

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

[Amigo]

PAV писал(а):

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

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

[PAV]

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

[Amigo]

PAV писал(а):

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

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

Добавлено спустя 1 час 25 минут 15 секунд:

Верно ли вообще, что если я доказал, что некоторое утверждение
истинно, то тем самым я доказал, что противоположное ему утверждение - ложно? Мне кажется, что "да". А разве нет?

[Amigo]

Спасибо PAV за ссылку на тему, а Brukvalub за ссылку на книгу. Очень интересная и более менее понятная для меня книга оказалась. Но есть всё-таки есть в ней вещи которые мне непонятны. В конце книги приводится следующий парадокс:

Цитата:

Это предложение недоказуемо.


Парадокс состоит в следующем. Если это предложение ложно, то не верно, что оно недоказуемо. Следовательно, оно доказуемо, а это означает, что оно истинно. Итак, предположив, что это предложение ложно, мы пришли к противоречию. Значит, оно должно быть истинно.

А теперь будьте внимательны! Я доказал, что предложение, набранное курсивом, истинно. Но в истинном предложении говорится о том, что есть на самом деле. Значит, оно недоказуемо. Как же мне удалось доказать его?

Где ошибка в приведенных мною рассуждениях? Ошибка в том, что понятие доказуемого предложения не вполне определенно. Одна из основных задач важного раздела современной математики, известного под названием "математической логики", состоит в придании точного значения понятию доказательства. Вполне строгого универсального определения доказательства, применимого к любым математическим системам, пока не существует. В современной математической логике принято говорить о доказуемости в рамках
данной системы. Предположим, что у нас имеется система (назовем ее системой S), в которой строго определено, что такое доказуемость в рамках системы S. Предположим также, что система S непротиворечива, то есть что всякое доказуемое в S предложение действительно истинно. Рассмотрим следующее предложение:


Это предложение недоказуемо в системе S.


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

Вот я ни как не могу понять, почему относительно второго утверждения, автор говорит,
что оно парадокса уже не представляет?
Я рассуждаю так:
Предположим это утверждение ложно, следовательно не верно, что оно не доказуемо в системе S. Следовательно оно доказуемо в системе S. Но поскольку система S не противоречива, то данное утверждение должно быть истинным. Противоречие.
Поскольку это предложение истинно, и мы это доказали средствами системы(или как мы это доказали? именно эта деталь мне более всего не понятна) S,
то не верно, что это предложение не доказуемо в системе S. Опять противоречие. С чего это парадокс снимается? Не пойму...

[PAV]

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

При этом остается две возможности - либо S не противоречива и тогда данное утверждение оказывается недоказуемым. Либо S противоречива - тогда утверждение, конечно, доказуемо, так как в противоречивой теории доказуемо любое утверждение.

Такое доказательство истинности действительно не может являться выводом в системе S, потому что иначе S оказывается противоречивой.

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

Добавлено спустя 51 минуту 20 секунд:

Собственно, подозреваю, что именно так теорема Геделя о непротиворечивости и доказывается.

Тему переношу из "Помогите решить" в дискуссионный раздел