Теорема Гёделя и формальные системы

[AndreUT]

Я из всего вышесказанного делаю такие выводы:

1) Геометрия Евклида не является формальной теорией (а что такое формальная теория, арифметика, и разницу между ними, мне еще надо выяснить )
2) Евклидова геометрия все-таки полна
3) Евклидова геометрия вследствие 1) не подходит под условия теоремы Геделя, что означает, что в ней нельзя сформулировать утверждение, доказуемое и опровержимое одновременно.

Правильные ли выводы? Прошу объяснить, только без очень умных слов, поскольку я не знаю еще многих определений )

[Stan Slapenarski]

arseniiv

Цитата:

Но AndreUT-то имел в виду не абсолютную геометрию, а евклидову!

AndreUT хотел увидеть конкретный пример из обычной геометрии. А, согласно следующему резюме по мотивам Интернета, именно абсолютная геометрия обычна. Пятый постулат резко выделяется среди других, он больше похож на сложную, неочевидную теорему. Евклид, вероятно, сознавал это, и поэтому первые 28 предложений в «Началах» доказываются без его помощи. Громоздкая формулировка пятого постулата закономерно вызывает некоторое чувство протеста и желание отыскать для него доказательство. Математики с давних времён пытались «улучшить Евклида» – либо исключить пятый постулат из числа исходных утверждений, то есть доказать его, опираясь на остальные постулаты и аксиомы, либо заменить его другим, столь же очевидным, как другие постулаты. Надежду на достижимость этого результата поддерживало то, что четвертый постулат Евклида (все прямые углы равны) действительно оказался лишним – он был строго доказан как теорема и исключён из перечня аксиом. История пятого постулата вдохновила известного французского карикатуриста Жана Эффеля на смешной и глубокий сюжет: он нарисовал Господа Бога, который дает урок геометрии юному Адаму. Бог стоит перед доской, на доске изображены два отрезка параллельных прямых, и Бог объясняет: «Вот две параллельные прямые. Они пересекаются только в бесконечности. Доказать этого нельзя, но я сам видел».

[Nemiroff]

AndreUT в сообщении #785009 писал(а):

Геометрия Евклида не является формальной теорией

Является.

Арифметика Пеано (или вот Робинсона) — это название некоторой теории. А еще это некоторый набор штук, которые должна иметь формальная теория, чтобы удовлетворять условию теоремы Гёделя.
А евклидова геометрия — это такая другая формальная теория (ну точнее, есть такая теория, которая представляет собой евклидову геометрию), которая этих самых штук не содержит. Вот так уж вышло.

Stan Slapenarski в сообщении #785010 писал(а):

А, согласно следующему резюме по мотивам Интернета, именно абсолютная геометрия обычна.

Это чудесно, но не имеет отношения к теореме Гёделя.

[AndreUT]

Тогда я буду искать более четкую формулировку теоремы и разбираться с базовыми понятиями.
Спасибо

[Stan Slapenarski]

Nemiroff писал(а):

Это чудесно, но не имеет отношения к теореме Гёделя.

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

AndreUT писал(а):

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

Можете попробовать посмотреть соответствующие статьи в Википедии – у меня сложилось впечатление, что математические статьи из нее достаточно хорошо сочетают строгость и понятность. Кроме того, в начале темы давали ссылки. Успехов!
---

Для интересующихся напишу еще пару слов о том, является ли геометрия Евклида формальной теорией. Сам Евклид в своих «Началах» был далек от формализма, формулируя аксиомы гораздо более туманнее, чем они формулируются сейчас. Например, «Точка есть то, что не имеет частей» (букв, «Точка есть то, часть чего ничто»), «Линия — длина без ширины», «Края же линии — точки», «Прямая линия есть та, которая равно лежит на всех своих точках». Цивилизованную формулировку геометрических аксиом можно найти, например, если мне не изменяет память, в «Высшей геометрии» Ефимова. То есть какая-нибудь гильбертовская аксиоматизация геометрии должна быть формальной (независимой от (семантической) интерпретации), поскольку О. Блюменталь сообщал, что уже в 1891 году Гильберт, обсуждая работу Г. Винера о роли теорем Дезарга и Паппа, о которой тот докладывал на одном из математических собраний, сделал свое знаменитое замечание, в двух словах передающее суть аксиоматического метода: «Следует добиться того, чтобы во всех геометрических утверждениях слова точка, прямая, плоскость можно было заменить словами стол, стул, кружка».

[Xaositect]

AndreUT в сообщении #784922 писал(а):

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

Не в любой, а в рекрсивно-перечислимой, в которой можно определить натуральные числа и арифметические операции над ними.

Цитата:

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

Как ни странно, обычная геометрия (теория первого порядка линейного пространства размерности 2 над действительнозамкнутым полем) разрешима, пока мы не добавляем в нее натуральные числа, например, предикат "данный отрезок имеет натуральную длину" или понятие "$n$-угольник".

[arseniiv]

(О статьях.)

Stan Slapenarski в сообщении #785023 писал(а):

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

Вот как раз на эту тему мне статьи не нравятся. Нормального аккуратного описания ни арифметик, ни исчислений высказываний и предиактов нет. По крайней мере, в русской. В английской что-то немного читать ещё можно.

[Stan Slapenarski]

(О статьях)

arseniiv писал(а):

Вот как раз на эту тему мне статьи не нравятся. Нормального аккуратного описания ни арифметик, ни исчислений высказываний и предиактов нет. По крайней мере, в русской. В английской что-то немного читать ещё можно.

Может быть. Видимо, мы читали разные статьи. Но, с другой стороны, ничего больше по сабжу я, в сущности, порекомендовать не могу, поскольку, с одной стороны, я не специалист по логике, а с другой и с книгами по ней мне не особо везло. У меня сложилось впечатление, что Мендельсон поспешен, Бурбаки запутан, из-за чего в обеих случаях страдают строгость и ясность, Чёрч не пошел у меня вообще, а популярные книги вроде «Гёделя, Эшера, Баха» Дагласа Хофштадтера, как для меня, могут несколько подхалтуривать.

[viknik]

Напомню популярное док-во 1-й теоремы Гёделя (восходящее, по-видимому, к книге Коэна "Теория множеств и континиум-гипотеза", с. 73):
(1) Задаётся нумерация всех арифметических формул с одной свободной переменной $A_1(x),A_2(x),...$
(2) Строится диагональная формула $A_n(n)$
(3) Строится формула ($A_n(n)$ не доказуема).
(4) Пусть номер этой формулы есть $\gamma$; тогда при подстановке $\gamma$ вместо $n$ получаем утверждение: ($A_\gamma(\gamma)$ не доказуема).
(5) СЕМАНТИЧЕСКОЕ доказательство истинности для ($A_\gamma(\gamma)$ не доказуема): допустим, что ($A_\gamma(\gamma)$ не доказуема) ложна. Тогда она ДОКАЗУЕМА и, в предположении "Из доказуемости следует истинность", получаем, что формула ($A_\gamma(\gamma)$ не доказуема) является истинной - ПРОТИВОРЕЧИЕ. Так что формула ( $A_\gamma(\gamma)$ не доказуема) является истинной. Аналогично доказывается истинность утверждения ($\lnot A_\gamma(\gamma)$ не доказуема)
* А вот мой вопрос. Рассмотрим формулу $\lnot A_n(n)$. Вроде бы, в ней нет ничего особенного и она должна встречаться в пересчёте всех формул с одной свободной переменной. Но, с другой стороны, она отличается от всех формул в пересчёте. ЧТО ЗДЕСЬ НЕ ТАК?

[Xaositect]

viknik в сообщении #785232 писал(а):

* А вот мой вопрос. Рассмотрим формулу $\lnot A_n(n)$. Вроде бы, в ней нет ничего особенного и она должна встречаться в пересчёте всех формул с одной свободной переменной. Но, с другой стороны, она отличается от всех формул в пересчёте. ЧТО ЗДЕСЬ НЕ ТАК?

Так у нее же нет свободной переменной.

[viknik]

У формулы $A_n(n)$, как и у формулы $\lnot A_n(n)$, ЕСТЬ свободная переменная. Каждая из этих формул получается применением выразимого в формальной арифметике оператора подстановки: в формулу (с одной свободной переменной), имеющую номер $n$, подставляется вместо свободной переменной номер самой этой формулы, т. е. то же самое число $n$. В общем, эта подстановка даёт формулу, из которой при подстановке чисел $1,2,3,..$ получаются формулы $A_1(1),A_2(2),A_3(3),...$ Так что переменная $n$ является в формуле $A_n(n)$ свободной.

[Xaositect]

Да, извиняюсь, запутался.
Надо конкретно смотреть конструкцию. У меня Коэна под рукой нет, только Колмогоров-Драгалин, а там настолько явной диагонали нет, используется теорема о неподвижной точке (для любой формулы $A(x)$ с 1 свободной переменной найдется формула $B$ с геделевым номером $\gamma$ такая, что $B\equiv A(\gamma)$)
Подозреваю, что строится на самом деле не $B(n) \equiv A_n(n)$, а $B(n)\equiv A_n(n) \textrm{ доказуема}$

[viknik]

Вообще-то, и у Коэна явной диагонали нет - просто я думаю, что только с оператором подстановки и можно строить диагональ (см. Справочная книга по математической логике. Часть IV. Сморинский, Теоремы о неполноте)

[nikvic]

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

Колмогоров-Драгалин, а там настолько явной диагонали нет, используется теорема о неподвижной точке

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

[epros]

viknik в сообщении #785232 писал(а):

допустим, что ($A_\gamma(\gamma)$ не доказуема) ложна. Тогда она ДОКАЗУЕМА

Или я чего-то не понял, или здесь что-то не так. Из указанного допущения следует не то, что "она" доказуема, а то, что $A_\gamma(\gamma)$ доказуемо (а значит и истинно). Недоказуемость $A_\gamma(\gamma)$ отсюда никоим образом не следует.

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