Альфред Тарский - Истина и доказательство

Первый шаг к обеспечению математической теории понятием формального доказательства состоит в формализации языка этой теории, в том смысле, который уже обсуждался в связи с дефиницией истины. В результате формализации получаются формальные синтаксические правила, позволяющие, в частности, просто по виду выражений отделить предложения от таких выражений, которые предложениями не являются. Следующий шаг ― формулирование немногих правил доказательства (или вывода). Число правил доказательства невелико, и их содержание несложно. Интуитивно все эти правила доказательства представляются непогрешимыми в том смысле, что предложение, которое непосредственным образом выводится из истинных предложений с помощью какого-либо из этих правил, должно быть истинным само по себе. В действительности же оказывается, что непогрешимость правил вывода может быть установлена на основе адекватной дефиниции истины. Наиболее известным и важным примером правил доказательства является правило отделения modus ponens. Согласно этому правилу (которое в некоторых теориях является единственным правилом доказательства), предложение q непосредственно выводимо из данных предложений, если одно из них есть условное предложение вида «если p, то q», тогда как другое есть р (здесь p и q являются, как обычно, сокращенными обозначениями любых предложений формализованного языка).

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

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

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

* * *

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