§5. Понятие вывода.

Определение.

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

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

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

3) он получается по правилу заключения из двух любых предшествующих членов последовательности В₁,В₂,…,В_к.

Как было показано в предыдущем примере_, выводом из совокупности формул Н={А,В} является конечная последовательность формул:

А, В, (А→А)→((А→В)→(А )), (А→В), А→А, (А→В)→(А )), А→В, А , . (см. формулы 1,2,3,7,5,6,8).

Если же здесь воспользоваться правилом сложного заключения , то вывод можно записать так:

А, В, (А→А)→((А→В)→(А )), В→(А→В), А→А, А→В, . (см. формулы 5, 7, 1, 3).

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

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

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

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

4)Если (включено), то всякий вывод из Н является выводом из W.

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

§6. Правила выводимости.

Эти правила непосредственно следуют из свойств вывода с использованием ПП и ПЗ.

Пусть Н и W – две совокупности формул исчисления высказываний. Будем обозначать через Н, W их объединение, т. е. Н,W= .

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

Укажем основные правила выводимости:

1. H ├ A Это правило следует непосредственно из определения вывода

H,w├a из совокупности формул : “Если а выводима из н, то она вы- водима из ”.

2. H,C ├ A,H├C

H├A .

3. H,C ├ A, W├C

H,W├A .

4. H ├ C→A

H,C├A .

5. Теорема дедукции: h, c├ a .

H├C→A

5A. Обобщенная теорема дедукции: {C₁, C₁, …, C_k}├ A

├C₁ →(C₂→(C₃→…(C_k→A)…))

6. Правило введения конъюнкции: H├A,H├B (показано в примере §4).

H├

7. Правило введения дизъюнкции: H,A├C;Н,B├C .

H, ├C

§9.Проблемы аксиоматического исчисления высказываний.

Всякая аксиоматическая теория для ее обоснования требует рассмотрения четырех проблем:

1. проблемы разрешимости,

2. проблемы непротиворечивости,

3. проблемы полноты,

4. проблемы независимости.

Проблема разрешимости исчисления высказываний.

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

Имеет место теорема: проблема разрешимости для исчисления высказываний разрешима.

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

Пусть А – любая формула исчисления высказываний, а х₁,х₂,…,х_n – перечень входящих в нее переменных. Вычислим R_a1,a2,..,an(A) на всех наборах значений а₁, а₂,…,а_n входящих в нее переменных. Если при этом R_a1,a2,..,an(A)=1, на всех наборах а₁, а₂,…,а_n, то формула А – тождественно истинна, и, значит, по теореме о доказуемости тождественно истинной формулы она доказуема.

Если же существует набор значений переменных такой, что , то формула А – не тождественно истинная, и, значит, по теореме 1 §8 она не доказуема.