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

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

Пусть у нас имеется некоторая совокупность формул

Тогда:

1) всякая формула является формулой, выводимой из Н;

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

3) если формулы С и выводимы из совокупности Н, то формула В также выводима из Н (правило заключения для выводимых формул).

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

Число формул совокупности Н может быть самым различным. Если Н= 0, то предполагается, что совокупность (множество) Н не содержит никаких других формул, кроме аксиом исчисления высказываний. Если указано, что совокупность Н состоит из некоторых формул, например A,B,C, то предполагается (по умолчанию), что в эту совокупность входят и аксиомы. Причем формулы A, B и C не обязательно должны быть доказуемыми.

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

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

Рассмотрим пример. Доказать, что из совокупности формул выводима формула .

Доказательство. Так как и , то по определению выводимой формулы

(1)

(2)

Возьмем аксиомы и I

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

(3)

(4)

Так как формула доказуема (см. подразд. 2.3), то она выводима из Н:

(5)

Из формул (5) и (3) согласно ПЗ получаем

(6)

Из формул (2) и (4) согласно ПЗ получаем

(7)

Из формул (7) и (6) согласно ПЗ получаем

(8)

И, наконец, из формул (1) и (8) по тому же ПЗ получаем

(9)

Если мы запишем последовательность всех выводимых формул с номерами (1)…(9), то получим

Такая последовательность называется выводом формулы из совокупности формул Н.

Теперь распространим понятие вывода на общий случай.