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

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

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

Тогда:

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

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

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

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

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

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

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