Истина и доказательство

Теперь можно объяснить, в чём состоит формальное доказательство предложения. Сначала применяют правила вывода к аксиомам и получают новые предложения, непосредственно выводимые из аксиом. Затем те же правила применяют к новым предложениям (или совместно к новым предложениям и аксиомам) и получают новые предложения и т.д. Если после конечного числа шагов мы приходим к некоторому предложению, то говорим, что оно формально доказано. Данную процедуру более точно можно выразить следующим образом: формальное доказательство предложения S состоит в построении конечной последовательности предложений, такой, что (1) первое предложение есть какая-либо аксиома языка, (2) каждое из последующих предложений есть или некоторая аксиома, или непосредственно выводимо с помощью одного из правил вывода из каких-либо предложений, предшествующих ему в этой последовательности, и (3) последним предложением в этой последовательности является S.

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

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

* * *

Несомненно, что великим достижением современной логики была замена старого психологического понятия доказательства точным, простым понятием чисто формального характера, но именно простота нового понятия оказывается ахиллесовой пятой. Чтобы оценить понятие формального доказательства, мы должны выяснить его отношение к понятию истины. Прежде всего формальное доказательство является процедурой, стремящейся к получению новых истинных предложений. Такая процедура будет адекватной только в том случае, если все предложения, полученные с помощью доказательства, будут истинными, а все истинные высказывания могут быть доказанными. Таким образом, естественно возникает проблема: является ли на самом деле формальное доказательство адекватной процедурой для получения истины? Иными словами, совпадает ли множество всех (формально) доказуемых предложений с множеством всех истинных предложений? Мы рассмотрим эту проблему на материале частной, очень элементарной математической дисциплины, а именно арифметики натуральных чисел (элементарной теории чисел). Мы предполагаем, что эта дисциплина представляет собой формализованную теорию. Словарь теории состоит из переменных, таких, как m, n, p..., представляющих произвольные натуральные числа, из цифр 0, 1, 2..., обозначающих конкретные числа, символов, обозначающих некоторые обычные отношения между числами и операции над числами, например, =, <, >, +, −, и, наконец, некоторых логических терминов ― пропорциональных связок («и»›, «или», «если», «не») и кванторов (выражений типа «для каждого числа», «для некоторого числа n»), синтаксических правил и правил вывода.