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

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

Пусть Н и 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

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

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

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

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

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

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