Из первого раздела мы знаем, что, взяв данный язык как язык-объект, мы можем построить соответствующий метаязык и сформулировать в нём материально адекватную дефиницию истины. Это позволяет нам утверждать, что все предложения, определённые с помощью этой дефиниции, составляют множество истинных предложений. В самом деле, дефиниция утверждает, что некоторым условиям, сформулированным в метаязыке, удовлетворяют все элементы этого множества, то есть все истинные предложения, и причём только эти элементы. Еще более легко можно сформулировать в метаязыке множество доказуемых предложений (дефиниция полностью согласуется с объяснением понятия формального доказательства, которое было дано во втором разделе). Строго говоря, дефиниции как истины, так и доказуемости принадлежат к новой теории, сформулированной в метаязыке и специально предназначенной для изучения формализованного арифметического языка. Новая теория называется метатеорией, или, более точно, метаарифметикой. Мы не будем рассматривать здесь в деталях тот путь, следуя по которому строится метатеория, её аксиомы, неопределяемые термины и т.д. Мы только обращаем внимание на то, что в рамках этой метатеории мы формулируем и решаем проблему, совпадает ли множество доказуемых предложений с множеством истинных предложений.
В нашей работе «Понятие истины в формализованных языках» было показано, что решение проблемы является негативным. Мы дадим здесь очень приближённое описание того метода, с помощью которого было получено это доказательство. Главная идея доказательства тесно связана с той идеей, на которую опирался Гёдель в своей знаменитой статье о неполноте формальных теорий.[8]
В разделе первом было отмечено, что метаязык, который позволяет нам определить и обсуждать понятие истины, должен быть достаточно богатым. Он содержит в целом весь язык-объект как свою часть, и поэтому мы можем говорить на нём о натуральных числах, множествах чисел, отношениях между числами и т.д. Но он также содержит и термины, необходимые для обсуждения свойств языка-объекта и его компонент. Следовательно, мы можем говорить на метаязыке о выражениях и, в частности, о предложениях, о множествах предложений, об отношениях между предложениями и т.д. Следовательно, в метатеории мы можем изучать свойства этих различных видов объектов и устанавливать связи между ними. Используя описание предложений, получаемых с помощью синтаксических правил языка-объекта, легко расположить все предложения (от простейших до всё более и более сложных) в бесконечный ряд и последовательно пронумеровать их. Мы соотносим с каждым предложением натуральное число таким образом, что два числа будут соотноситься с двумя различными предложениями. Другими словами, мы устанавливаем взаимнооднозначное соответствие между предложениями и числами. Это, в свою очередь, приводит к подобному же соответствию между множеством предложений и множеством чисел, а также отношений между предложениями и отношений между числами. В частности, мы можем рассматривать номера доказуемых предложений и номера истинных предложений. Для краткости мы назовем их доказуемыми номерами и истинными номерами. Наша главная проблема сведётся тогда к вопросу: являются ли тождественными множество доказуемых номеров и множество истинных номеров?
Ответ на этот вопрос будет отрицательным. Очевидно, достаточно указать только одно свойство, которое принадлежит одному множеству и не принадлежит другому. Это свойство, которое мы обнаружим, может представляться неожиданным, относящимся к виду deus ex machina.
Внутренняя простота формального доказательства и (формальной) доказуемости будет играть здесь основную роль. Мы видели в разделе втором, что значение этих понятий объясняется, по существу, с помощью некоторых простых отношений между предложениями, приписываемых им немногими правилами доказательства. Читатель мог бы вспомнить здесь правило modus ponens. Соответствующие отношения между номерами предложений точно так же просты; оказывается, их можно охарактеризовать с помощью простейших арифметических операций и отношений, таких, как сложение, умножение и равенство, то есть охарактеризовать в терминах, существующих в нашей арифметической теории. Как следствие, множество доказуемых номеров может быть охарактеризовано таким же образом, хотя это множество и было первоначально определено в метаязыке (путем ссылки на соответствующее множество доказуемых предложений). Эта дефиниция может быть заменена некоторым её эквивалентом, сформулированным в языке-объекте. Тем самым дефиниция доказуемости будет переведена с метаязыка на язык-объект.
8
K. Gödel. On Formally Indecidable Propositions in the Principia Mathematica and Related Systems. In «The Indecidable». N.Y. 1965, pp. 5-58.