Истина и доказательство
Шрифт:
Первый шаг к обеспечению математической теории понятием формального доказательства состоит в формализации языка этой теории, в том смысле, который уже обсуждался в связи с дефиницией истины. В результате формализации получаются формальные синтаксические правила, позволяющие, в частности, просто по виду выражений отделить предложения от таких выражений, которые предложениями не являются. Следующий шаг - формулирование немногих правил доказательства (или вывода). Число правил доказательства невелико, и их содержание несложно. Интуитивно все эти правила доказательства представляются непогрешимыми в том смысле, что предложение, которое непосредственным образом выводится из истинных предложений с помощью какого-либо из этих правил, должно быть истинным само по себе. В действительности же оказывается, что непогрешимость правил вывода может быть установлена на основе адекватной дефиниции истины. Наиболее известным и важным примером правил доказательства является правило отделения modus ponens. Согласно этому правилу (которое в некоторых теориях является единственным правилом доказательства), предложение q непосредственно выводимо из данных предложений, если одно из них есть условное предложение вида «если p, то q», тогда
Теперь можно объяснить, в чём состоит формальное доказательство предложения. Сначала применяют правила вывода к аксиомам и получают новые предложения, непосредственно выводимые из аксиом. Затем те же правила применяют к новым предложениям (или совместно к новым предложениям и аксиомам) и получают новые предложения и т.д. Если после конечного числа шагов мы приходим к некоторому предложению, то говорим, что оно формально доказано. Данную процедуру более точно можно выразить следующим образом: формальное доказательство предложения Ѕ состоит в построении конечной последовательности предложений, такой, что (1) первое предложение есть какая-либо аксиома языка, (2) каждое из последующих предложений есть или некоторая аксиома, или непосредственно выводимо с помощью одного из правил вывода из каких-либо предложений, предшествующих ему в этой последовательности, и (3) последним предложением в этой последовательности является Ѕ.
Любая аксиоматическая теория, язык которой формализован и для которой имеет силу понятие формального доказательства, называется формализованной теорией. Мы оговариваем в качестве особого условия, что единственным доказательством, которым можно пользоваться в формализованной теории, является формальное доказательство. Ни одно предложение не может рассматриваться как теорема, если оно не появляется в списке аксиом или для него не может быть найдено формальное доказательство. Метод изложения формализованной теории на каждой стадии её развития является в принципе очень элементарным: мы сначала перечисляем аксиомы, а затем все известные теоремы в таком порядке, что каждое предложение из списка, не являющееся некоторой аксиомой, может быть непосредственно установлено как теорема просто путём сравнения его вида с видом предложений, которые предшествуют ему в списке, без привлечения для этого сложных видов рассуждения и убеждения. (Мы здесь не говорим о психологическом процессе, посредством которого теоремы открывались на самом деле). В результате обращение к интуитивной очевидности существенно ограничивается; сомнение относительно истинности теорем хотя целиком и не элиминируется, однако сводится к возможным сомнениям относительно истинности немногих предложений, перечисленных в качестве аксиом, и к сомнениям в непогрешимости немногих простых правил доказательства. Мы можем добавить, что процесс введения новых терминов в язык теории также может быть формализован с помощью специальных формальных правил образования дефиниции.
Известно, что все существующие математические дисциплины могут быть представлены как формализованные теории. Формальные доказательства в них могут быть приведены для самых глубоких и самых сложных математических теорем, которые первоначально были установлены с помощью интуитивных аргументов.
* * *
Несомненно, что великим достижением современной логики была замена старого психологического понятия доказательства точным, простым понятием чисто формального характера, но именно простота нового понятия оказывается ахиллесовой пятой. Чтобы оценить понятие формального доказательства, мы должны выяснить его отношение к понятию истины. Прежде всего формальное доказательство является процедурой, стремящейся к получению новых истинных предложений. Такая процедура будет адекватной только в том случае, если все предложения, полученные с помошью доказательства, будут истннными, а все истинные высказывания могут быть доказанными. Таким образом, естественно возникает проблема: является ли на самом деле формальное доказательство адекватной процедурой для получения истины? Иными словами, совпадает ли множество всех (формально) доказуемых предложений с множеством всех истинных предложений? Мы рассмотрим эту проблему на материале частной, очень элементарной математической дисциплины, а именно арифметики натуральных чисел (элементарной теории чисел). Мы предполагаем, что эта дисциплина представляет собой формализованную теорию. Словарь теории состоит из переменных, таких, как m, n, p..., представляющих произвольные натуральные числа, из цифр 0, 1, 2..., обозначающих конкретные числа, символов, обозначаюших некоторые обычные отношения между числами и операции над числами, например, =, <, >, +, -, и, наконец, некоторых логических терминов - пропорциональных связок («и»›, «или», «если», «не») и кванторов (выражений типа «для каждого числа», «для некоторого числа n»), синтаксических правил и правил вывода.
Из первого раздела мы знаем, что, взяв данный язык как язык-объект, мы можем построить соответствующий метаязык и сформулировать в нём материально адекватную дефиницию истины. Это позволяет нам утверждать, что все предложения, определённые с помощью этой дефиниции, составляют множество истинных предложений. В самом деле, дефиниция утверждает, что некоторым условиям, сформулированным в метаязыке, удовлетворяют все элементы этого множества, то есть все истинные предложения, и причём только эти элементы. Еще более легко можно сформулировать в метаязыке множество доказуемых предложений (дефиниция полностью согласуется с объяснением понятия формального доказательства, которое было дано во втором разделе). Строго говоря, дефиниции как истины, так и доказуемости принадлежат к новой теории, сформулированной в метаязыке и специально предназначенной для изучения формализованного арифметического языка. Новая теория называется метатеорией, или, более точно, метаарифметикой. Мы не будем рассматривать здесь в деталях тот путь, следуя по которому строится метатеория, её аксиомы, неопределяемые термины и т.д. Мы только обращаем внимание на то, что в рамках этой метатеории мы формулируем и решаем проблему, совпадает ли множество доказуемых предложений с множеством истинных предложений.
В нашей работе «Понятие истины
В разделе первом было отмечено, что метаязык, который позволяет нам определить и обсуждать понятие истины, должен быть достаточно богатым. Он содержит в целом весь язык-объект как свою часть, и поэтому мы можем говорить на нём о натуральных числах, множествах чисел, отношениях между числами и т.д. Но он также содержит и термины, необходимые для обсуждения свойств языка-объекта и его компонент. Следовательно, мы можем говорить на метаязыке о выражениях и, в частности, о предложениях, о множествах предложений, об отношениях между предложениями и т.д. Следовательно, в метатеории мы можем изучать свойства этих различных видов объектов и устанавливать связи между ними. Используя описание предложений, получаемых с помощью синтаксических правил языка-объекта, легко расположить все предложения (от простейших до всё более и более сложных) в бесконечный ряд и последовательно пронумеровать их. Мы соотносим с каждым предложением натуральное число таким образом, что два числа будут соотноситься с двумя различными предложениями. Другими словами, мы устанавливаем взаимнооднозначное соответствие между предложениями и числами. Это, в свою очередь, приводит к подобному же соответствию между множеством предложений и множеством чисел, а также отношений между предложениями и отношений между числами. В частности, мы можем рассматривать номера доказуемых предложений и номера истинных предложений. Для краткости мы назовем их доказуемыми номерами и истинными номерами. Наша главная проблема сведётся тогда к вопросу: являются ли тождественными множество доказуемых номеров и множество истинных номеров?
8
K. G"odel. On Formally Indecidable Propositions in the Principia Mathematica and Related Systems. In «The Indecidable». N.Y. 1965, pp. 5-58.
Ответ на этот вопрос будет отрицательным. Очевидно, достаточно указать только одно свойство, которое принадлежит одному множеству и не принадлежит другому. Это свойство, которое мы обнаружим, может представляться неожиданным, относящимся к виду deus ex machina.
Внутренняя простота формального доказательства и (формальной) доказуемости будет играть здесь основную роль. Мы видели в разделе втором, что значение этих понятий объясняется, по существу, с помощью некоторых простых отношений между предложениями, приписываемых им немногими правилами доказательства. Читатель мог бы вспомнить здесь правило modus ponens. Соответствующие отношения между номерами предложений точно так же просты; оказывается, их можно охарактеризовать с помощью простейших арифметических операций и отношений, таких, как сложение, умножение и равенство, то есть охарактеризовать в терминах, существующих в нашей арифметической теории. Как следствие, множество доказуемых номеров может быть охарактеризовано таким же образом, хотя это множество и было первоначально определено в метаязыке (путем ссылки на соответствующее множество доказуемых предложений). Эта дефиниция может быть заменена некоторым её эквивалентом, сформулированным в языке-объекте. Тем самым дефиниция доказуемости будет переведена с метаязыка на язык-объект.
С другой стороны, обсуждение понятия истины в обыденных языках решительно наводит на предположение о том, что никакого подобного перевода для дефиниции истины получить нельзя, ибо в противном случае было бы доказано, что язык-объект является в некотором смысле семантически универсальным, и это грозило бы вновь появлением антиномии лжеца. Мы подтверждаем это предположение, доказывая, что если бы множество истинных номеров могло быть переведено на язык арифметики, то в таком случае антиномия лжеца появилась бы и в этом языке. Однако, поскольку мы сейчас имеем дело с ограниченным формальным языком, антиномия приобрела бы здесь более утончённую форму (по сравнению с обычными формулировками антиномии лжеца).
Таким образом, множество доказуемых номеров не совпадает с множеством истинных номеров, поскольку первое определимо на языке арифметики, тогда как последнее не определимо. Следовательно, множества доказуемых предложений и истинных предложений не совпадают друг с другом. С другой стороны, используя дефиницию истины, мы легко доказываем, что все аксиомы арифметики являются истинными и все правила доказательства являются непогрешимыми. Следовательно, все доказуемые предложения являются иститиными, тогда как обратное высказывание не имеет силы.
В результате мы приходим к выводу, что существуют предложения, сформулированные на языке арифметики, которые являются истинными, но не могут быть доказаны формально на основе аксиом и правил доказательства, принятых в арифметике. Можно подумать, что данное заключение существенным образом зависит от специфических аксиом и правил вывода, выбранных для арифметической теории, и что окончательный исход дискуссии мог бы быть иным, если бы мы соответственным образом обогатили теорию, введя в неё новые аксиомы или новые правила вывода. Однако более тщательный анализ показывает, что вывод очень мало зависит от специфических свойств обсуждаемой теории и что он распространяется и на большинство других формализованных теорий. Предполагая, что некоторая теория включает в себя арифметику натуральных чисел (или что по крайней мере арифметика может быть реконструирована в ней), мы можем повторить существенную часть аргументации в практически неизменном виде. Таким образом, мы вновь придём к выводу, что множество доказуемых предложений данной теории отличается от множества истинных предложений. Более того, если мы можем показать (как это часто бывает), что все аксиомы теории являются истинными и все правила вывода непогрешимыми, то мы далее заключаем, что в данной теории существуют истинные предложения, которые недоказуемы. За исключением некоторых элементарных теорий вывод о несовпадении понятий истинности и доказуемости справедлив по отношению ко всем другим формализованным теориям и, следовательно, имеет почти универсальный характер.