Просмотр

{| width="100%"  
 | width="40%"|[[Формулы арифметики их номера]] << 
 ! width="20%"|[[Истинность и доказуемость|Оглавление]] 
 | width="40%" align="right"| >> [[Что такое истина?]]
|}
----
Как ни странно, но существование формул, которые невозможно ни доказать ни опровергнуть, на самом деле, достаточно естественно. В математике нет ограничения на длину доказательства. Мы можем записать сколь угодно длинную формулу. Её формальное доказательство также является формулой, которая будет ещё длиннее. Более того, весь опыт математики говорит о том, что минимально возможная длина доказательства данной формулы напрямую не связана с её длиной. Многие очень простые формулы имеют очень сложные (=длинные) доказательства (теорема Ферма, задача о 4-х красках, и т.п.).

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

Гёдель в 1931 г. предложил формальную демонстрацию этого факта. Введем логическую функцию "<math>\textstyle \mathbf{Proof}(A)</math>", обозначающую то, что существует доказательство формулы "<math>\textstyle A</math>". Если доказательство "<math>\textstyle A</math>" существует, то "<math>\textstyle \mathbf{Proof}(A)=И=истина</math>", а если нет то "<math>\textstyle \mathbf{Proof}(A)=Л=ложь</math>". Теперь рассмотрим высказывание <math>\textstyle \mathbf{G}</math>, определяемое как утверждение о том, что оно недоказуемо: <blockquote> <math>\textstyle \mathbf{G} : \neg \mathbf{Proof}(\mathbf{G})</math>. </blockquote> Сформулируем теорему Гёделя: <blockquote>  "Если теория непротиворечива, то формула <math>\textstyle \mathbf{G}</math> истинна, но ее нельзя доказать: <math>\textstyle \mathbf{Proof}(\mathbf{G})=Л</math>". </blockquote> Непротиворечивость означает, что ложную формулу нельзя доказать <math>\textstyle \mathbf{Proof}(Л)=Л</math>, а если формула доказуема <math>\textstyle \mathbf{Proof}(\mathcal F)=И</math>, то она истинна: <math>\textstyle \mathcal F=И</math>. Поэтому строится такое доказательство от противного: <math>\textstyle \lozenge_1</math>: пусть <math>\textstyle \mathbf{Proof}(\mathbf{G})=И \;\;=>\;\; \mathbf{G}=И,\;но\;\mathbf{G}=\neg \mathbf{Proof}(\mathbf{G})=\neg И=Л</math>. Мы получили противоречие, значит исходная посылка "<math>\textstyle \mathbf{Proof}(\mathbf{G})=И</math>" не верна, следовательно, доказательства утверждения '''G''' не существует. Но об этом и ''утверждает'' '''G''', поэтому мы построили высказывание, которое не доказуемо, но при этом истинно ''по своему смыслу''.

Конечно можно было построить и прямое доказательство теоремы: <math>\textstyle \lozenge_2</math>: пусть <math>\textstyle \mathbf{Proof}(\mathbf{G})=Л \;\;=>\;\; \mathbf{G}=Л,\;но\;\mathbf{G}=\neg \mathbf{Proof}(\mathbf{G})=\neg Л=И</math> и опять получить противоречие. Однако, так не делают. Почему? Потому, что в первом случае вывод из "<math>\textstyle \mathbf{Proof}(\mathbf{G})=И</math>" того, что "<math>\textstyle \mathbf{G}=И</math>" основывается на определении истинности (раз доказательство утверждения существует, то утверждение истинно). Во втором же случае, учитывая общие соображения, приведенные в начале этого раздела, можно усомниться в том, что из отсутствия доказательства утверждения <math>\textstyle \mathbf{G}</math>, т.е. "<math>\textstyle \mathbf{Proof}(\mathbf{G})=Л</math>" следует его ложность "<math>\textstyle \mathbf{G}=Л</math>" (как в прочем, и истинность). Поэтому, рассуждения <math>\textstyle \lozenge_2</math> считаются неправомерными.

Формулировки и доказательство, приведенные выше, очень ''психологичны''. Они используют никак не определённое понятие <math>\textstyle \mathbf{Proof}</math> ("существует доказательство"), а также объект '''G''', который, подобно парадоксу лжеца, вводится со ссылкой на самого себя. Поэтому, в такой форме теорема о неполноте убедительна только при изрядной харизме доказывающего. Заслуга Гёделя состоит в том, что он придал и <math>\textstyle \mathbf{Proof}</math> и <math>\textstyle \mathbf{G}</math> видимость конструктивных объектов в рамках арифметики натуральных чисел.

Введём предикат <math>\textstyle {D}(p, f)</math>, обозначающий, что формула под номером <math>\textstyle f</math> имеет доказательство под номером <math>\textstyle p</math>, т.е. <math>\textstyle \mathcal P</math> доказывает <math>\textstyle \mathcal F</math>. Понятно, что когда доказательство <math>\textstyle \mathcal P</math> ''уже построено'', в силу его формальности, мы всегда можем проверить, что оно соответствует принятыми правилам, и в его конце находится доказываемая формула <math>\textstyle \mathcal F</math>. Подобный алгоритм вполне реализуем, поэтому предикат <math>\textstyle { D}(p, f)</math> можно также рассматривать как всюду определённую вычислимую на компьютере функцию, возвращающую 1, если <math>\textstyle \mathcal P</math> доказывает <math>\textstyle \mathcal F</math> или 0, если нет.

При помощи <math>\textstyle { D}(p, f)</math> мы можем определить утверждение, которое себя не может доказать. Рассмотрим сначала следующий простой вариант:

:<center><math>\mathbf{G} : \neg \exists p \,D(p, g),\;\;\;\;\;\;\;где\;\;\;\;\;g=\gamma(\mathbf{G})=\gamma(''\neg \exists p \,D(p, g)'').</math></center>

В этом определении, символ <math>\textstyle g</math> &mdash; это ''конкретное'' число (гёделевский номер формулы), получаемое из решения уравнения: <math>\textstyle g=\gamma(''\neg \exists p \,D(p, g)'')</math>.

Теперь можно "смело" проводить доказательство теоремы о не полноте. Например, пусть <math>\textstyle \mathbf{G}</math> доказуемо, тогда существует некоторый номер доказательства <math>\textstyle p_0</math>, при котором <math>\textstyle D(p_0, g)</math> истинно. Следовательно, можно ввести квантор всеобщности и записать <math>\textstyle \exists p\, D(p, g)</math>, а это не что иное, как <math>\textstyle \neg \mathbf{G}</math>. Мы приходим к противоречию, следовательно <math>\textstyle \mathbf{G}</math> не доказуемо. Аналогично проверяется недоказуемость <math>\textstyle \neg \mathbf{G}</math>.

<math>\textstyle \bullet</math> Вернёмся к уравнению <math>\textstyle g=\gamma(''\neg \exists p \,D(p, g)'')</math>. Как оно должно решаться? В предикате <math>\textstyle D(p,x)</math> (или в соответствующем алгоритме для компьютера) кодируются все символы, и в тех местах, где встречается <math>\textstyle x</math>, ставится сначала "<math>\textstyle 0</math>", вычисляется гёделевский номер формулы, и проверяется не равен ли он 0. Если нет, подставляется <math>\textstyle \,0'\,</math> (т.е. 1) и сравнивается результат с единицей, затем <math>\textstyle 0''</math>, и т.д, пока решение найдено не будет. Увы, но, по крайней мере в гёделевской нумерации, это уравнение ''не имеет решения''! Действительно, если код штриха равен числу <math>\textstyle m>0</math>, то <math>\textstyle g</math> штрихов в <math>\textstyle 0'''''</math> вместо <math>\textstyle x</math> на <math>\textstyle k</math>-той позиции приведут в <math>\textstyle \gamma</math> к произведению простых чисел в степени <math>\textstyle m</math>: <math>\textstyle p_{k+1}^m\cdot...\cdot p_{k+1+g}^m</math>, что существенно больше чем число <math>\textstyle g</math> (которому должно равняться <math>\textstyle \gamma</math>). Взять для штриха код <math>\textstyle m=0</math> нельзя, так как тогда формулы <math>\textstyle \gamma(''0=0'')</math> и <math>\textstyle \gamma(''\,0=0'''\,'')</math> будут неотличимы. Таким образом, такой прямолинейный вариант построения <math>\textstyle \mathbf{G}</math> не проходит, и необходимы дополнительные хитрости.

<math>\textstyle \bullet</math> Предикат <math>\textstyle D(p,f)</math> получает номер любой формулы <math>\textstyle f</math>. Однако, её доказательство <math>\textstyle p</math> может существовать только если <math>\textstyle f</math> замкнута (без свободных переменных). Так, "<math>\textstyle x>2</math>" не доказуема и не опровергаема. Рассмотрим, тем не менее, класс формул, которые содержат одну свободную переменную вида <math>\textstyle F(x)</math> и будем их доказывать при ''данном'' <math>\textstyle x</math>:

:<center><math>Q(x):\;\; x>2,\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;F(x):\;\; \exists a\,\exists b\,\exists c\, (a^x+b^x=c^x),\;\;\;\;\;\;\;\;....</math></center>

При любом конкретном <math>\textstyle x</math>, первая формула имеет простое доказательство, и <math>\textstyle Q(3)</math>, например, будет истинной. Вторая формула, для <math>\textstyle F(3)</math> потребует уже достаточно нетривиальных рассуждений и будет ложной, и т.д. Все такие формулы имеют номер <math>\textstyle f=\gamma(''x>0'')</math>. Если же на место <math>\textstyle x</math> подставлено конкретное число, номер будет ''другой'', так как это другая строка <math>\textstyle f_1=\gamma(''0'''>0'')</math>.

Для подстановки "данного числа" введём функцию:

:<center><math>s(f) = \gamma\left(\,\{x/f\}\;\Gamma(f)\,\right).</math></center>

Она вычисляется по следующему алгоритму. Берётся формула с произвольным номером <math>\textstyle f</math>. По этому номеру "раскручивается" её строковое представление <math>\textstyle \Gamma(f)</math>. В нём вместо всех свободных вхождений <math>\textstyle x</math> подставляется число <math>\textstyle f</math> [в форме <math>\textstyle 0''''''</math>], и снова вычисляется гёделевский номер. В принципе, может возникнуть несколько свободных переменных, поэтому будем считать, что <math>\textstyle \{x/f\}</math> означает, что все они замещаются на <math>\textstyle f</math>. Чтобы <math>\textstyle s(f)</math> была всюду определена, необходимо модифицировать алгоритм нумерации так, чтобы для всех <math>\textstyle f=0,1,2,...</math> при применении <math>\textstyle \Gamma(f)</math> получались ''правильно построенные'' формулы, иначе нельзя будет идентифицировать свободна переменная или нет. ''Пусть'' это сделано.

Определим теперь высказывание (формулу):

:<center><math>G(x) :\;\;\neg\exists p\, D(p, s(x)).</math></center>

Здесь содержится утверждение о том, что не существует доказательства некоторой формулы под номером <math>\textstyle x</math>, в которую вместо всех свободных переменных подставлен номер этой формулы, т.е. конкретное число <math>\textstyle x</math>. Пусть гёделевский номер <math>\textstyle G(x)</math> (формула зависящая от одной свободной переменной) равен <math>\textstyle g</math>. Тогда определим:

:<center><math>\mathbf{G} :\;\;\neg \exists p\, D(p, s(g)),\;\;\;\;\;\;\;\;\;где\;g=\gamma(''\neg \exists p\, D(p, s(x))'').</math></center>

Подчеркнём, что <math>\textstyle g</math> &mdash; это ''конкретное число'', вычисленное при помощи гёделевской нумерологии по строке <math>\textstyle \gamma(''\neg\exists p\, D(p, s(x))'')</math>, где <math>\textstyle x</math> ''свободная переменная''.

Не сложно видеть, что формула <math>\textstyle \mathbf{G}</math> имеет номер равный <math>\textstyle s(g)</math>:

:<center><math>\gamma(\mathbf{G}) = \gamma(''\neg \exists p\, D(p, s(g))'') = s(g).</math></center>

Действительно, функция <math>\textstyle s(g)</math> восстанавливает формулу <math>\textstyle G(x)</math> и подставляет в неё число <math>\textstyle g</math>. Таким образом, <math>\textstyle \mathbf{G}</math> утверждает свою недоказуемость.

<math>\textstyle \bullet</math> Подобное построение уже не содержит явных просчётов, но тем не менее предполагает доказанными ряд "очевидных" посылок. Так, мы считаем, что можно вычислять номер формул, содержащих "мета"- арифметическую функцию <math>\textstyle s(x)</math>, которую не просто записать в рамках только арифметических операций, так как она использует поиск и замену свободных переменных. Поэтому, лучше <math>\textstyle D(p,f)</math> и <math>\textstyle s(x)</math> воспринимать как программы для идеального компьютера, например, на языке BASE. Правда, переходя к программированию, прийдётся выразить символы существования и единственности в виде бесконечных циклов, а не использовать их как самостоятельные математические объекты. Тем не менее, будем считать, что объект <math>\textstyle \mathbf{G}</math> "сконструирован".

Получая противоречие при доказательстве <math>\textstyle \lozenge_1</math> теоремы Гёделя, необходимо помнить, что возможны два варианта: (1) теорема верна; (2) объекты, участвующие в её доказательстве, не существуют, так как некорректно определены. Не всегда существование противоречия доказывает то, что мы хотим доказать!

Даже если при построении <math>\textstyle \mathbf{G}</math> удаётся формально устранить все сомнения, есть ещё один вопрос, связанный с квантором существования <math>\textstyle \exists</math>, и определением предиката <math>\textstyle \mathbf{Proof}(f)=\exists p\, D(p, f)</math>. Вспомним, что при доказательстве теоремы Тьюринга, противоречие свидетельствовало об отсутствии универсальной функции контроля остановки <math>\textstyle T(p,i)</math>. Не возникает ли той же проблемы с функцией <math>\textstyle \mathbf{Proof}(f)</math>?

----
{| width="100%"  
 | width="40%"|[[Формулы арифметики их номера]] << 
 ! width="20%"|[[Истинность и доказуемость|Оглавление]] 
 | width="40%" align="right"| >> [[Что такое истина?]]
|}
----
[[Истинность и доказуемость]] - о конструктивной математике, Канторе и Гёделе