Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Ещё раз о теоремах Гёделя

Пусть у нас есть некая теория Т. Она состоит из языка на котором формулируются утверждения и конечного набора правил дедукции, при помощи которых мы выводим одни утверждения из других. (Правила дедукции, которые выводят некие утверждения “из воздуха”, называются аксиомами. Вполне может быть, что конечный набор правил дедукции пораждает бесконечное число аксиом.)

Имеет смысл рассматривать только непротиворечивые теории, т.е. такие, где нельзя доказать одновременно "А" и "не А". Противоречивые теории бессодержательны; там любое высказывание независимо от содержания является доказуемым.

Теория называется полной, если любое для любого высказывания “А” доказуемо либо “А”, либо “не А”.
Полные теории существуют, наприме, арифметика, не содержащая умножения, полна. Язык арифметики, содержащей только сложение-вычитание, настолько беден, что можно алгоритмически выяснить для любого утверждения на этом языке, истинно оно или ложно.

Теорема Гёделя № 1: О неполноте.

Что: Если (непротиворечивая, порождённая конечным набором правил) теория содержит арифметику с умножением, то она неполна.

Почему: Арифметика с умножением имеет бесконечное число “степеней свободы”, их нельзя зафиксировать конечным числом правил.

Почему: Если мир теории (множество натуральных чисел в случае арифметики) содержит более чем конечное число объектов, то существует много разных моделей миров, соответствующих аксиомам теории. Среди них (в случае арифметики) существует минимальная модель, состоящая из 0, 1, 2 и других чисел, которые мы можем записать. Однако существуют и другие нестандартные модели, содержащие "бесконечно далёкие числа", конструктивно (т.е. сложением единичек) недостижимые. Изнутри теории нельзя ввести какую-то аксиому, требующую, чтобы мы работали в минимальной модели. Аксиомы теории живут "внутри мира", а изнутри нет способа увидеть, живём мы в минимальной модели или в матрице^W в другой модели, которая работает как настоящая, но содержит невидимые бесконечно удалённые числа.

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

Теорема Гёделя № 2: О недоказуемости непротиворечивости.

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

Идея 2: В теории, содержащей арифметику с умножением и индукцией, можно написать высказывание Cons(n) = “доказательство n не выводит противоречие”.

Идея 3: Если доказать, что для любого натурального n верно Cons(n), то наша теория непротиворечива.

Примечание: Как будет видно ниже, высказывание “n => Cons(n)” это не просто “данная теория непротиворечива”, а более сильное высказывание. Оно может быть неверно, хотя теория на самом деле непротиворечива.

Утверждение теоремы: Высказывание “n => Cons(n)” недоказуемо.

Почему: Потому что “для всех n” означает в том числе и для тех n, которые к конструктивному сегменту не относятся. И мы действительно всегда можем построить нестандартную модель с бесконечно далёким числом n, для которого Cons(n) не верно. Конечно же, нет доказательства с таким номером, но изнутри модели мы никак не можем отличить настоящие числа от ненастоящих. На самом деле высказывание “данная теория непротиворечива” мы ни в какой теории сформулировать не можем, только вот это более сильное “n => Cons(n)”.

Можно ли это как-то обойти?
Первую теорему нет: либо полная теория, но очень простая, либо богатая, но неполная. Корову можно либо доить, либо употреблять в жареном виде, то и другое одновременно затруднительно.

Вторую — в какой-то степени да:
1) Бывают арифметические системы с настолько слабой дедуктивной системой, что n => Cons(n) верно, несмотря на то, что n может быть бесконечно удалённым. Этой дедуктивной системы не смотря на слабость может хватить, чтобы это самое n => Cons(n) доказать.

2) Но конечно же не может хватать, чтобы доказать n => Cons(n) для более сильных дедуктивных систем: для них n => Cons(n) попросту неверно, если не исключить бесконечно удалённые числа n.

3) Мы можем частично исключить: добавить аксиому, исключающую возможность существования “бесконечно удалённых чисел” порядком ниже определённого ординала W в мире с этой аксиомой. Теперь можем доказать n => Cons(n) для любых теорий с дедуктивной силой ниже W.

4) Только теперь в результате добавления аксиомы про W наша собственная теория стала силы W, и тем самым потеряла способность осозновать свою собственную непротиворечивость.

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

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 5 comments