§2. Исчисление высказываний
Предварительное обсуждение
Простой алгоритм проверки принадлежности формулы пропозициональной теории, приведённый в §1, хорош не во всех отношениях. Если вспомнить основную цель исследования – изучение человеческого мышления, то недостаток алгоритма становится понятен: люди думают не так. Они используют умозаключения, а не полный перебор различных вариантов (он «несолиден» и обычно нереален из-за высокой трудоёмкости). Формальный аналог умозаключения называется правилом вывода, а система, позволяющая производить последовательные выводы – исчислением. При этом любое умозаключение должно начинаться с какой-то посылки, значит, должны быть некоторые исходные посылки, принимаемые на веру, некритически, с которых всё начинается – аксиомы.
Итак, для задания
исчисления необходимо и достаточно
задать его аксиомы и правила вывода.
При этом важно, чтобы относительно любой
формулы можно было бы за конечное время
определённо выяснить, является ли она
аксиомой; другими словами – теория А,
состоящая из аксиом (аксиоматика),
должна быть разрешимой.
Для задания необходимой аксиоматики
не то, чтобы потребуется, но – окажется
очень удобна – ещё одна логическая
связка – импликация. Она, конечно,
выражается через уже имеющиеся:
.
Соответственно, полезно модифицировать
рассматриваемый алфавит, добавив к нему
новый символ J,
заменяющий буквосочетание DN:
.
2. Аксиоматика
Определение 2.1. Аксиомой исчисления высказываний называется любая формула, имеющая один из тринадцати видов:
(А1)
,
(А2)
,
(А3)
,
(А4)
,
(А5)
,
(А6)
,
(А7)
,
(А8)
,
(А9)
,
(А10)
,
(А11)
,
(А12)
,
(А13)
,
где а, b, с – произвольные формулы.
Замечания. (1) Почему приведённая аксиоматика разрешима? Потому что существует алгоритм (обычно именуемый синтаксическим анализом) который позволяет проверить, имеет ли некоторое выражение один из тринадцати приведённых выше видов (для начала посмотрим, начинается ли слово с буквы J или D, затем выделим фрагменты, соответствующие аргументам этой булевой функции и т.д.).
(2) Выражения (А1) – (А13) обычно называют схемами аксиом. Их конечное число. Конкретные аксиомы получаются из схем заменой переменных а, b, с на конкретные формулы, поэтому множество всех аксиом бесконечно. Соответственно, и количество аксиом бесконечно. Важно также отметить, что а, b, с – не пропозициональные переменные, они принимают значения не из множества высказываний, а из множества формул. Такие переменные можно назвать формульными.
(3) От вхождения
«лишнего» символа J
можно избавиться, заменив все его
вхождения «обратно» на DN.
Например, аксиома (А8) превратится при
этом в «настоящую» формулу
.
(4) С другой стороны,
использование символа J
упрощает аксиомы, но ещё не делает их
интуитивно понятными (что было бы крайне
желательным)
.
В этом смысле определение 2.1. представляет
собой самый настоящий «персидский
компромисс». Для того чтобы радикально
повысить их интуитивную очевидность,
можно использовать любой естественный
символ импликации:
,
или
.
Все они, так или иначе, используются в
метаязыке, так что его использование
нарушит одно из используемых соглашений.
Кроме того, это исключит возможность
использования свойств «польской записи»,
так что для установления порядка
выполнения логических операций придётся
использовать скобки (обычным образом).
Тем не менее, сделаем это, используя
символ
и привычные символы для дизъюнкции,
конъюнкции и отрицания. Это превратит
список схем аксиом (А1) – (А13) в следующий
список:
(А1)
,
(А2)
,
(А3)
,
(А4)
,
(А5)
,
(А6)
,
(А7)
,
(А8)
,
(А9)
,
(А10)
,
(А11)
,
(А12)
,
(А13)
.
В таком виде аксиомы действительно являются интуитивно очевидными .
(5) Список схем аксиом из определения 2.1. не является единственно возможным для построения исчисления высказываний. Он даже не является минимальным! В действительности можно, основываясь на полном наборе булевых функций, состоящем из импликации и тождественного нуля, построить аксиоматику, основанную всего на трёх схемах аксиом.
Определение 2.1'. Аксиомой исчисления высказываний называется любая формула, имеющая один из трёх видов:
(В1) ,
(В2) ,
(В3)
.
При этом аксиомы вида (А3) – (А13) станут теоремами (что бы ни означало это слово).