Понятие вывода

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

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

2) он является доказуемой формулой;

3) он получается по ПЗ (для доказуемых и выводимых формул) из двух любых предшествующих членов последовательности .

Из определения выводимой формулы и вывода из совокупности формул Н следуют свойства вывода:

1) всякий начальный отрезок вывода из совокупности Н есть вывод из Н;

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

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

4) если ( − знак включения, читается: “множество Н включено в множество W “ или “ Н содержится в W “), то всякий вывод из совокупности Н является и выводом из совокупности W.

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

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