Правила вывода

1. Правило подстановки. Если формула А доказуема в исчислении высказываний, х переменная, В – произвольная формула исчисления высказываний, то формула, полученная в результате замены в формуле А переменной х всюду, где она входит, формулой В, является также доказуемой формулой.

Операция замены в формуле А переменной х формулой В носит название подстановки и символически записывается так:

.

Если А – доказуемая формула, то будем писать ├А. Тогда правило подстановки можно записать схематически следующим образом:

И читается эта запись так: «Если формула А доказуема, то доказуема формула .

2. Правило заключения. Если формулы А и АВ доказуемы в исчислении высказываний, то формула В также доказуема. Схематическая запись этого правила имеет вид:

Определение 3.4. Определение доказуемой формулы.

а) Всякая аксиома является доказуемой формулой.

б) Формула, полученная из доказуемой формулы путем применения подстановки вместо переменной х произвольной формулы В есть доказуемая формула.

в) Формула В, полученная из доказуемых формул А и А  В путем применения правила заключения, есть доказуемая формула.

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

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

Производные правила вывода

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

1. Правило одновременной подстановки.

Пусть А – доказуемая формула; x₁, х₂, ..., х_п – переменные, a B₁, B₂, ..., В_п – любые формулы исчисления высказываний. Тогда результат одновременной подстановки в А вместо x₁, х₂, ..., х_п соответственно формул B₁, B₂, ..., В_п является доказуемой формулой.

Схематично операция одновременной подстановки записывается в виде:

2. Правило сложного заключения.

Второе производное правило применяется к формулам вида

(А₁ (А₂ (…(А_пL)…))

Если формулы А₁, А₂, ..., А_п и (А₁ (А₂ (…(А_пL)…)) доказуемы, то и формула L доказуема.

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

3. Правило силлогизма.

Если доказуемы формулы АВ и ВС, то доказуема формула АС, то есть

4. Правило контрпозиции.

Если доказуема формула АВ, то доказуема формула , то есть

5. Правило снятия двойного отрицания.

а) Если доказуема формула , то доказуема формулаАВ.

б) Если доказуема формула , то доказуема формулаАВ.

То есть

Понятие выводимости формулы из совокупности формул

Будем рассматривать конечную совокупность формул Н={А₁, А₂,..., А_п}.

Определение 3.5. Определение формулы, выводимой из совокупности формул.

1. Всякая формула А_iН является формулой, выводимой из Н.

2. Всякая доказуемая формула выводима из Н.

3. Если формулы С и СВ выводимы из совокупности Н, то формула В также выводима из Н.

Если некоторая формула В выводима из совокупности Н, то записывают Н├В.

Класс формул, выводимых из совокупности Н, совпадает с классом доказуемых формул в случае, когда совокупность Н содержит только доказуемые формулы, и в случае, когда Н пуста.

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