3.4. Исчисление высказываний

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

1. Алфавит:

• Пропозициональные буквы

Логические операторы (читаются соответственно “не” и “влечет, следует”);

• Скобки

2. Построение формул (или пропозициональных форм):

• Любая пропозициональная буква суть формула.

• Если есть формула, то и также является формулой.

• Если есть формула, то и также является формулой.

• Если являются формулами, то и выражение также является формулой.

3. Аксиомы:

Здесь являются пропозициональными формами или формулами.

4. Одно правило вывода (правило модус поненс, или правило отделения):

Если суть теоремы, то есть следствие выводимо из

Формально это правило записывается следующим образом:

Начиная с момента создания этой формальной системы, использовалась ее интерпретация, моделирующая рассуждения

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

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

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

К этим законам относятся следующие:

— закон тождества, или

— закон исключения третьего, или

— закон противоречия, или

Последний закон гласит, что никакая теорема не может одновременно являться и теоремой, и не-теоремой.

В качестве примера доказательства в исчислении высказываний приведем доказательство приведенного выше закона тождества: “Для всякого выполняется Формула

является аксиомой и, следовательно, теоремой Она соответствует аксиоме где формула представлена цепочкой символов а формула — цепочкой из одного символа Аксиома позволяет представить в качестве теоремы следующую формулу:

где соответствует

Теперь первая формула построена: теорема суть первая часть, заключенная в скобки в Правило модус поненс утверждает, что

Итак, сама формула в соответствии с аксиомой при подстановке вместо представляет собой теорему. Правило модус поненс, примененное еще раз, приводит к теореме

Эта формула уже точно выражает закон тождества.

Другие основные теоремы доказываются аналогично в несколько этапов:

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

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

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

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

формул и в исчислении высказываний. На самом деле будет доказано новое правило вывода

Предположим, что является теоремой, которая уже доказана в исчислении высказываний. Поставим ей в соответствие левую часть аксиомы подставляя Р вместо вместо вместо Тогда по правилу модус поненс получим

Обозначив формулу в аксиоме (А 1) как У, получим теорему где — какая-то формула. Так как является теоремой, еще одно применение правила модус поненс позволяет вывести либо

Теперь, подставив, в аксиоме вместо вместо вместо и применив в третий раз правило модус поненс, находим

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

что доказывает новое правило вывода или метатеорему в исчислении высказываний, т. е. дает новый способ построения теорем типа

где и — формулы исчисления высказываний.

Важные замечания об обычных способах записи формул.

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

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

Много исследований, связанных с исчислением высказываний, было проведено начиная со времен Аристотеля. В 1910 г. Уайтхед и Рассел дали, наконец, строгое формальное представление исчисления высказываний, а также доказали

значительное число теорем, связанных с ним. Интересно отметить, что в их работах исчисление высказываний строилось не на трех, а на четырех аксиомах. Позже Лукасевич показал, что одна из аксиом является лишней, так как может быть выведена из трех остальных. Выше была описана именно эта форма задания исчисления высказываний с уменьшенным числом аксиом. При экономном подходе исчисление высказываний может быть построено таким образом, чтобы в нем использовался один оператор вместо двух, как определено выше. Таким оператором является “штрих Шеффера” (или дизъюнкция отрицаний), который обозначается вертикальной чертой и определяется следующим образом:

Символ интерпретируется как несовместность высказываний. Ж. Нико, основываясь на использовании этого единственного оператора — связки, показал в что исчисление высказываний может быть построено на единственной аксиоме:

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