Т. А. Сливина математическая логика и теория алгоритмов

§ 2. Определение доказуемой формулы. Правила вывода и заключения

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

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


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

Первая группа аксиом

I₁
I₂

Вторая группа аксиом

II₁
II₂
II₃

Третья группа аксиом

III₁
III₂
III₃

Четвертая группа аксиом

IV₁
IV₂
IV₃
Приведенные аксиомы считаются исходными доказуемыми формулами. Введем правила, с помощью которых можно получать новые доказуемые формулы.


Правила вывода
1. Правило подстановки.
Если формула А доказуема в исчислении высказываний, х переменная, В – произвольная формула исчисления высказываний, то формула, полученная в результате замены в формуле А переменной х всюду, где она входит, формулой В, является также доказуемой формулой.
Операция замены в формуле А переменной х формулой В носит название подстановки и символически записывается так:
.
Уточним сформулированное правило.
а) Если формула А есть переменная х, то подстановка
дает В.
б) Если формула А есть переменная у, отличная от х, то подстановка
дает А.
в) Если А – формула, для которой подстановка уже определена, то подстановка В вместо х в отрицание А есть отрицание подстановки, то есть подстановка дает .
г) Если А₁ и А₂ – формулы, для которых подстановки в уже определены, то подстановка дает .
Если А – доказуемая формула, то будем писать ├ А.
2. Правило заключения.
Если формулы А и АВ доказуемы в исчислении высказываний, то формула В также доказуема.
3. Определение доказуемой формулы.
а) Всякая аксиома является доказуемой формулой.
б) Формула, полученная из доказуемой формулы путем применения подстановки вместо переменной х произвольной формулы В есть доказуемая формула.
в) Формула В, полученная из доказуемых формул А и АВ путем применения правила заключения, есть доказуемая формула.
г) Никакая другая формула исчисления высказываний не считается доказуемой.
Процесс получения доказуемых формул будем называть доказательством.
Приведем пример доказательства.
Доказать, что ├ АА (рефлексивность импликации).
Воспользуемся аксиомой I₂:
├
и выполним подстановку . Тогда получим
├ (1)
Применяя правило заключения к аксиоме I₁ и формуле (1), получим
├ (2)
В формуле (2) осуществим подстановку

В результате получим доказуемую формулу
├ (3)
Применим правило заключения к аксиоме IV₂ и формуле (3). В результате получим доказуемую формулу ├ .