3.3. Разрешимость и интерпретация формальных систем

3.3.1. Разрешимость

Первым вопросом, который возникает при задании формальной системы, является вопрос об инверсии, т. е. о том, возможно ли, рассматривая какую-либо формулу формальной системы; определить, является ли она доказуемой или нет. Другими словами, речь идет о том, чтобы определить, является ли данная формула теоремой или не-теоремой и как это доказать. В математике предполагается, что при задании формальной системы существует хорошо определенный способ действий, который за конечное число шагов позволит получить ответ на данный вопрос. Такой способ, если он существует, называется процедурой решения, а соответствующую формальную систему называют разрешимой. Однако основная трудность заключается в том, что такие процедуры существуют далеко не всегда, даже для таких простых и фундаментальных теорий, как исчисление предиктов первого порядка (разд. Д5). Причина этого состоит в следующем. Даже если применить правила словообразования (т. е. правила построения формул, правила вывода) последовательно ко всем возможным объектам формальной системы и формальная система такова, что Имеется принципиальная возможность полного перечисления ее теорем (даже при бесконечном числе), то все же не существует никакого подходящего способа в общем случае, чтобы перечислить все нетеоремы.

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

3.3.2. Интерпретация

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

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

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

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

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

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

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

символом Г на схеме, изображенной на рис. 3.1) либо не-теоремой а с другой стороны, ее интерпретация может быть истинйой либо ложной

Первый вариант , когда интерпретация истинна, не представляет проблемы. Если формула доказуема и соответствует определенной интерпретации, значение которой ложно, то такая интерпретация просто не представляет интереса.

Рис. 3.1. Четыре класса сочетания теорем и не-теорем и значений истинности ИСТИНА (V) и ЛОЖЬ (F).

Вариант исключается из рассмотрения и может использоваться для определенной корректировки рассматриваемой формальной системы таким образом, чтобы с ней остались связанными только те интерпретации, значения которых истинны для всех теорем системы. Теперь рассмотрим варианты и ( соответствующие не-теоремам. Что касается варианта 4, то весьма желательно, чтобы значение “ложь” было бы присвоено всем не-теоремам; однако это не всегда возможно (разд. 3.4.1). Тем не менее наиболее часто используемые формальные системы относятся именно к этому случаю, как, например, логика высказываний (которую называют также пропозициональной логикой или исчислением высказываний). Логика высказываний рассмотрена в разд. 3.4.

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

символы имеют обычный арифметический характер. Это утверждение проверено с помощью ЭВМ, на которой оно просчитано до значений Однако остается возможность того, что оно недоказуемо в существующей арифметической аксиоматике. Еще более неприятным является тот факт, что (как показано в разд. 3.6) существуют формальные системы, в которых класс формул не является пустым ни при какой интерпретации!

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

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

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

3.3.4. Примеры формальных доказательств

Пример 1. Формальная система

Эта система определена в разд. В ней в качестве аксиомы и правила вывода определены

Теоремы в этой системе получаются следующим образом:

Очевидно, что теоремы здесь совпадают с формулами вида

где символ повторяется по раз до и после символа . В сокращенном виде это может быть записано

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

Отметим, что при рассмотрении этой формальной системы необходимо использовать систему более высокого уровня — формальную арифметику.

Замечание. Необходимость различать язык и метаязык возникает в ситуациях, когда естественный язык выполняет одновременно две различные функции:

• указание соответствующего фрагмента в произведении;

• определение на языке грамматики этого же языка.

Это различие является фундаментальным для информатики, где специальные программы (компиляторы) предназначены для преобразования на язык другого уровня исходных программ.

Определение какого-либо языка программирования в форме Бэкуса — Наура задает формальную систему, которая определяет допустимые выражения этого языка:

Эта запись означает, что программа представляет собой команду или программу с последующей командой:

Таким образом, все символы между угловыми скобками последовательно определены.

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

Теперь введем две интерпретации системы

Первая интерпретация. Условимся, что символ а представляет нуль, символ обозначает последующее целое числа за числом, стоящим справа от него на множестве целых чисел, и символ обозначает знак равенства. Тогда аксиома интерпретируется как и является истинной. Последовательность теорем отображается последователыиитью равенств которые все истинны. В противоположность этому формула которая не вытекает из интерпретации какой-либо теоремы, является для нас очевидно ложной. (Эта формула следует из не-теоремы Таким образом, имеется корректная интерпретация системы в обычной арифметике с полным соответствием При этом клетки 2 и 3 на рис. 3.1 являются пустыми.

Вторая интерпретация. Теперь пусть а обозначает предложение: “Сократ смертен”, знак — идентичность двух предложений, и символ означает отрицание. Тогда аксиома формулируется следующим образом:

“Сократ смертен” идентично “Сократ смертен”, что рассматривается нами как истинное выражение.

Первая теорема приобретает следующую форму: “Сократ бессмертен” идентично “Сократ бессмертен”, что истинно. (Отметим, что на самом деле здесь не имеет значения то, был ли Сократ смертен или нет, так как оба предыдущих выражения утверждают только, что ложь идентична лжи, а истина — истине.)

Рис. 3.2. Дерево ветвлений для

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

Пример 2. Формальная система

Формальная система (рис. 3.2) имеет следующие правила вывода:

С учетом поставленной выше задачи вопрос заключается в том, является ли формула теоремой в системе выводима ли она из аксиомы Проведем формальное исследование системы на метауровне.

Прежде всего очевидно, что в системе могут порождаться только формулы, начинающиеся с символа М. Действительно, оба правила — продукции 1) и изменяют начало слов. С этой точки зрения может являться теоремой. Впрочем, для достижения цели необходимо устранить по крайней мере один символ , уже имеющийся в аксиоме. Для этого можно использовать только правила 2 и/или 3, так как правила 1 и 4 оставляют неизменным число символов в формуле.

Правило 3 уменьшает общее число символов на 3 единицы, а правило 2 напротив, каждый раз удвцивает это число. Следовательно, правило 2 создает только четные числа символов тогда как правило 3 уменьшает их только на 3 единицы. Таким образом, чтобы получить число символов I, равное нулю, нужно применить правило 3 к формуле, содержащей число символов кратное трем, причем их должно быть только 3 до последнего применения правила 3. А так как правило 2 порождает только четные числа символов то оно не сможет породить такие формулы.

Рис. 3.3. Схема возможных переходов системе при использовании правил

Следовательно, не является теоремой формальной системы

Отметим, что для получения этого результата снова был использован результат из другой формальной системы — формальной арифметики (и это не случайно), состоящий в следующем; для того чтобы число делилось на 3, необходимо, чтобы на 3 делилось и число так как числа 2 и 3 не имеют общих делителей. А так как правила 2 и 3 не могут порождать число символов кратное трем, и в аксиоме не содержится число кратное трем, то невозможно и получение таких формул.

Приведенные выше рассуждения можно более кратко и просто представить с помощью новой формальной системы, моделирующей правила 2 и 3 системы

Аксиома: (число символов в аксиоме Правило (результат действия правила 2);

Правило (результат действия правила 3). Необходимо определить, можно ли в этой системе получить Нельзя получить формулы с числом символов кратным трем. Формулы типа не могут быть теоремами в На рис. 3.3 показаны возможные переходы между формулами в системе при использовании правил 2 и 3.

Полученную формальную систему над можно упростить с помощью схемы, показанной на рис. 3.2, где возможными возвратными шагами являются только шаги с уменьшением на 3 единицы за шаг имеющегося числа единиц 1. Действия по модулю 3 отражают этот существенный факт. При по

модулю 3 (второе изменение первоначального представления), так как правило 3 оставляет неизменным и так как по модулю 3 равно по модулю 3 и равно то получаем новую формальною систему над

Аксиома:

Правило

Необходимо определить, можно ли в этой формальной системе получить

Очевидно, что получение в системе не может быть осуществлено, поскольку не могут попеременно принимать значения