ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ, пропозициональное исчисление

— логическое исчисление (см. Логико-математическое исчисление), определяющее с помощью доказуемых в нем формул логические законы, которым подчиняются логические связки «и», «или», «если..., то», «тогда и только тогда», «не» и др. Высказывания в И. в. рассматриваются только в связи с тем, как они образованы с помощью логич. связок из др. высказываний, взятых целиком, без учета их субъектно-предикатной структуры. И. в. часто входит как часть в более обширные формальные системы. Благодаря своей простоте И. в. служит иллюстрацией для многих общих понятий метаматематики. В кибернетике И. в., как и др. формальные системы, используется в последнее время при доказательстве теорем на ЭВМ.

Классическое И. в. характеризуется тем, что оно имеет двузначную интерпретацию («истинно», «ложно») и в нем доказуема любая тождественно истинная формула алгебры логики. В классическом И. в. доказуемы, в частности, исключенного третьего закон и т. п. «парадоксы материальной импликации», а именно: формулы которые, если отождествить импликацию с логическим следованием, содержательно означают: «если высказывание р истинно, то оно следует из любого высказывания », «если р ложно, то из него следует любое q». В ряде неклассических И. в. ставится цель определить с помощью мн-ва доказуемых в них ф-л другие, возможно, более адекватные человеческой интуиции понятия истины, логич. закона, логич. следования. Различные неклассические И. в. отличаются от классического И. в. ограничением действия закона исключенного третьего (см. Интуиционизм, Логика конструктивная), приписыванием высказываниям заранее (до построения системы аксиом) более двух истинностных значений, устранением возможности доказательства парадоксов материальной импликации путем надлежащего выбора системы аксиом и правил вывода (исчисление импликации строгой), добавлением нетрадиционных логических связок и т. д.

Существует много разновидностей классического И. в., отличающихся друг от друга набором логич. связок, системами аксиом и правилами вывода. Первая формулировка классического И. в. как формальной системы принадлежит нем. математику Г. Фреге (1879). Рассмотрим одну из разновидностей классического И. в. Исходными символами этого И. в. являются: логические связки скобки и бесконечное число переменных Понятие

ф-лы определяется следующим образом. 1. Переменная есть ф-ла. 2. Если - ф-лы, то также являются ф-лами. . Никаких других ф-л, кроме тех, которые получаются согласно 1—2, нет. Напр., является ф-лой, а р ф-лой не является. Поскольку большое к-во скобок часто затрудняет чтение ф-лы, условимся в ф-лах опускать внешние скобки, а также считать, что связывает ф-лы сильнее, чем связывают ф-лы сильнее, чем Тогда, напр., можно записать в виде Следующие ф-лы примем за аксиомы. 1.

Правила вывода следующие. Правило Подстановки. Вместо переменной можно всюду, где она встречается в подставить любую одну и ту же Правило заключения (modus ponens). Из двух можно получить новую Символически это правило занисываетя , так: получаемая из некоторых ф-л с помощью однократного применения одного из правил вывода, наз. непосредственно выводимой из этих Конечная последовательность, состоящая из одной или больше доказательством последней ф-лы этой последовательности, если каждая ф-ла в ней либо является аксиомой, либо непосредственно выводима из предыдущих ф-л последовательности. Ф-ла И. в., для которой существует доказательство, наз. доказуемой или выводимой из аксиом И. в., или теоремой И. в. При построении доказательства в И. в. ф-лы выводятся только с помощью правил вывода, а не каких-либо содержательных соображений. Последние могут только подсказать, к каким посылкам применять правила вывода. Для примера выпишем доказательство теоремы:

1. (подстановка в аксиому 7).

2. (подстановка в аксиому 6).

3. (подстановка в аксиому 8).

4. (по правилу заключения из 1 и 3).

5. , (по правилу заключения из 2 и 4).

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

Ф-ла 33 наз. выводимой из гипотез если можно доказать только с помощью правила заключения, приняв за аксиомы и все теоремы И. в. Теорема дедукции утверждает, что если выводима из гипотез то выводима из гипотез а тем самым есть теорема И. в. Сокращенно: если то Приведем пример доказательства теоремы об И. в. с использованием теоремы дедукции.

Теорема:

Доказательство. 1. (по правилу заключения из (по правилу заключения из В и из выведенной выше теореме дедукции из

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

Для И. в., как и для всякой формальной системы, возникают вопросы о непротиворечивости, полноте и независимости системы его аксиом. Формальная система, имеющая символ для отрицания, наз. непротиворечивой, если ни для какой не являются обе доказуемыми в этой системе. Если бы в И. в. оказались доказуемыми некоторые то в нем была бы доказуема и Поэтому в силу доказуемости в нем ф-л вида в этом исчислении была бы доказуема любая Такое исчисление, конечно, никакой ценности не представляло бы. Рассматриваемое И. в. непротиворечиво. Это следует из того, что всякая теорема И. в. является тождественно истинной ф-лой, а любая ф-ла вида такой не является и, следовательно, она не доказуема в И. в. Формальная система наз. полной по отношению к некоторому свойству, если в ней доказуемы все ф-лы,

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

Если в приведенной системе аксиом отбросить 12-ю аксиому, то получится позитивное И. в., задающее с помощью доказуемых в нем ф-л те законы логики, которые не содержат отрицания. Если заменить 12-ю аксиому 13-й аксиомой , то получится исчисление высказываний минимальное, сильно отличающееся от классического И. в. недоказуемостью в нем многих классических законов, содержащих отрицание. Если заменить 12-ю аксиому двумя аксиомами. а именно: 13-й аксиомой и аксиомой получится интуиционистское исчисление, в котором не доказуем закон исключенного третьего (т. е. ф-ла ). Заменив же 12-ю аксиому аксиомой или же двумя — 13-й и аксиомой , получим снова классическое И. в.

Существуют формулировки классического И. в., основывающиеся только на части обычных логич. связок. При этом система логич. связок выбирается полная (см. Алгебра логики). Напр., непротиворечивой, полной и независимой является система аксиом, состоящая из аксиом 1, 2 и 12-й, а также следующая система аксиом:

Ф-лы, содержащие связки, которые не входят в эти системы аксиом, уже не являются ф-лами этих новых разновидностей И. в. Однако такие ф-лы можно ввести в качестве сокращений ф-л этих новых И. в., считая сокращениями соответственно . Имеются формулировки классического

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

Лит.: Новиков П. С. Элементы математической логики. М., 1973; Чёрч А. Введение в математическую логику. Пер. с англ., т. 1. М., 1960; Карри X. Б. Основания математической логики. Пер. с англ. М., 1969; [библиогр. с. 518—547]; Мендельсон Э. Введение в математическую логику. Пер. с англ. М., 1971 [библиогр. с. 296—309].

В. Ф. Костырко.