3.3. Интерпретация формальной системы

Формальные системы являются не просто игрой ума, а всегда представляют собой модель какой-то реальности (либо конкретной, либо математической).

Интерпретация представляет собой распространение исходных положений какой-либо формальной системы на реальный мир. Интерпретация придаёт смысл каждому символу формальной системы и устанавливает взаимно однозначное соответствие между символами формальной системы и реальными объектами. Теоремы формальной системы, будучи однажды интерпретированы, становятся после этого утверждениями в обычном смысле слова, и в этом случае уже можно делать выводы об их истинности или ложности.

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

Конкретная формальная система является тем более интересной, чем больше существует для неё различных интерпретаций. В таком случае наличие даже какого-то одного формального доказательства уже обеспечивает получение различных конкретных результатов. В современной математике большой интерес вызывают формальные системы, которые исследуются в теории категорий и теории моделей.

3.4. Доказательство и истинность

Из приведённых выше определений существует уже по построению глубокое различие между концепциями доказательства и истинности. Эти понятия относятся к двум различным областям. Априорно ничто не гарантирует, что всякое утверждение, истинное в обычном смысле слова, соответствует какой-то доказуемой формуле. Ведь не только то истинно, для чего у нас есть доказательство!

На самом деле имеются четыре варианта взаимоотношений между доказательством и значением истинности, поскольку формула, с одной стороны, может быть теоремой либо не-теоремой, а с другой стороны, её интерпретация может быть истинной либо ложной.

Первый вариант, когда интерпретация истинна, не представляет проблемы. Если формула доказуема и соответствует определённой интерпретации, значение которой ложно, то такая интерпретация просто не представляет интереса. Вариант теорема «ложь» исключается из рассмотрения и может использоваться для определённой корректировки рассматриваемой формальной системы таким образом, чтобы с ней остались связанными только те интерпретации, которые истинны для всех теорем системы. Теперь рассмотрим варианты: не-теорема «истина», не-теорема «ложь». Что касается последнего, то весьма желательно, чтобы значение «ложь» было бы присвоено всем не-теоремам; однако это не всегда возможно. Тем не менее наиболее часто используемые формальные системы относятся именно к этому случаю, как, например, логика высказываний (которую называют также пропозициональной логикой или исчислением высказываний).

Наиболее сложным является вариант не-теорема «истина», когда не всегда можно избежать трудностей, заключающихся в том, что могут существовать не-теоремы данной формальной системы, которые в определённых интерпретациях являются истинными, причём такие интерпретации часто оставляются для рассмотрения. В качестве примера назовём знаменитое утверждение Ферма: «Для всякого целого n  , уравнение в целых числах xⁿ+yⁿ=zⁿ не имеет решения ». Вполне возможно, что оно является истинным в обычной интерпретации, где используемые имеют обычный арифметический характер. Это утверждение проверено с помощью ЭВМ, на которой оно просчитано до значений n=10000. Однако остаётся возможность того, что оно не доказуемо в существующей арифметической аксиоматике. Ещё более неприятным является тот факт, что существуют формальные системы, в которых класс формул не-теорема «истина» не является пустым ни при какой интерпретации!

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

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

Другим подробным примером является следующий: если никакое правило вывода данной системы не порождает формулы, более длинной (т.е. содержащей большее число символов), чем теорема, к которой оно применяется, то всякая теорема большего размера, чем аксиома, может быть удалена из рассмотрения. В этом случае всегда можно получить результат за конечное число шагов, так как дерево поиска уменьшено в этом случае до конечной величины ≤Lⁿ , где L – число символов в алфавите, а n – длина доказываемой формулы.

Именно такой подход позволил трём великим математикам Черчу, Геделю и Тарскому получить к 1930 г. весьма общие результаты, относящиеся к формальным системам и называемые теоремами ограничения.

Возможны формальные системы, в которых

• существуют формулы m, такие, что ни m ни  m не являются доказуемыми (теорема Геделя);

• во всякой их интерпретации найдутся выражения, истинные, но недоказуемые (теорема Тарского);

• не существует алгоритма, чтобы отличать теоремы от не-теорем (теорема Черча).