Исчисления высказываний

§3. Исчисления высказываний.

Определим исчисление высказываний ИС. Рассмотрим алфавит V = V 1È V 2 È V 3 È V 4, где V 1= {A0,A1,…}, V 2 = { ┐, &,Ú , É }, V 3 = {(, ), ,}, V 4 = { ├ }. Понятие формулы определяется, как в §1. Секвенциями называют выражения вида ( где Á 1,…,Á п, В – любые формулы)

Á 1,…,Á п + В, где п > 0 ( из Á 1,…,Á п следует В)

+ В (В доказуема)

Á 1,…,Á п ├, где п > 0 ( система Á 1,…,Á п противоречива).

Правилом вывода называется выражение вида , где S 1,… , S к, S -- произвольные секвенции. S называется непосредственным следствием S 1,… , S к по данному правилу вывода.

Исчисление ИС определяется следующими схемой аксиом и правилами вывода (где Á , B , Ã -- произвольные формулы, Г, Г1, Г2 , Г3 – конечные последовательности формул, возможно пустые).

Схема аксиом Á + Á .

Правила вывода:

1. Г
1+ Á; Г1+ BÞГ1, Г2 + (Á& B) (введение &)

2. Г├ ( Á & B) Þ Г├ Á (удаление &)

3. Г├ ( Á & B) Þ Г├ B (удаление &)

4. Г├ B Þ Г├ (Á È B) (введение È )

5. Г├ Á Þ Г├ (Á È B) (введение È )

6. Г1 ├ (Á È B); Г2 , Á ├ Ã ;Г3 , B ├ Ã Þ Г 1 ,Г 2 , Г3 + Ã (удаление È )

7. Г , Á ├ B Þ Г ├ (Á É B) ( введение É )

8. Г1 ├ ( Á É B ); Г2 + Á Þ Г1 , Г2 ├ В (удаление É )

9. Г, Á ├ Þ Г├ ù Á (введение ù )

10. Г1 ├ Á ; Г2 ├ ┐Á Þ Г1 , Г2 ├ (сведение к противоречию)

11. Г, ┐Á ├ Þ Г ├ Á (удаление ù )

12. Г ├ Þ Г ├ Á ( утончение )

13. Г├ Á Þ Г, В ├ Á ( расширение)

14. Г1, Á , В, Г2+ Ã Þ Г1, В, Á , Г2+ Ã ( перестановка)

15. Г1, Á , Á , Г2+ Ã Þ Г1, Á , Г2+ Ã ( сокращение).

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

Выводом в ИС называется конечная последовательность секвенций S 1,…, S п такая, что для каждого i ( 1 £ i £ n) S i есть либо аксиома, либо непосредственное следствие предыдущих секвенций по правилам 1—15.

Секвенция S называется выводимой в ИС , если существует вывод в ИС, оканчивающийся S . Правило называется допустимым в ИС, если из выводимости в ИС секвенций S 1,…, S п следует выводимость секвенции S .

Определим исчисление ИВ. Схемами аксиом исчисления ИВ являются следующие выражения:

1. (Á É ( B É Á ))
2. ((Á É B) É ((Á É (B É Ã )) É ( Á É Ã )))
3. ((Á & B) É B)
4. ((Á & B) É Á )
5. ((Á É B) É ((Á É Ã ) É (Á É (B & Ã ))))
6. (Á É (Á È B))
7. (B É (Á È B))
8. ((Á É Ã ) É (( B É Ã ) É ((Á È B) É Ã )))
9. ((Á É ù B) É (B É ù Á ))
10. (ù ù Á É Á )

Исчисление ИВ имеет следующее правило вывода ( modus ponens):

.

Аксиомой (или вариантом схемы аксиом) называется выражение, полученное из данной схемы аксиом подстановкой вместо символов Á , B , Ã конкретных формул. Формула В называется непосредственным следствием формул Á и (Á Ì B ).

Выводом в ИВ называется конечная последовательность формул Á 1,…, Á п такая, что для каждого i ( 1 £ i £ n) Á i есть либо аксиома, либо непосредственное следствие предыдущих формул.

Вывод на множестве формул Г есть последовательность Á 1,…, Á п такая, что для каждого i ( 1 £ i £ n) Ái есть либо аксиома, либо одна из формул Г, либо непосредственное следствие предыдущих формул.

Будем писать ├ Á ( Г├ Á ), если существует вывод (вывод из Г), оканчивающийся формулой Á . Формула Á в этом случае называется выводимой в ИВ (выводимой из Г).

Множество формул Г назовем противоречивым, если существует такая формула Á , что Г├ Á и Г├ ┐Á . В противном случае Г назовем непротиворечивым.

Интуиционистским исчислением высказываний ИИВ называется исчисление, схемами аксиом которого являются схемы аксиом 1—9 исчисления ИВ и формулы вида (┐Á É (Á É В)), правилом вывода – modus ponens. Определение выводимости в ИИВ аналогично соответствующему определению для ИВ. ├И Á(Г├И Á ) означает, что Á выводима в ИИВ (Á выводима в ИИВ из Г).

Логической матрицей называется система Â = á M; D, &, Ú , É , ù ñ , где М – непустое множество, D Í M, &, Ú , É -- двуместные, ù -- одноместная функция на М. Формула Á называется общезначимой в Â , если при любых значениях переменных в множестве М значение формулы Á входит в D.

Говорим, что формула Á зависит от системы формул D , если существует конечная последовательность формул В1,…, Вп, где Вп = Á и для любого i ( 1 £ i £ n) Вi есть непосредственное следствие предыдущих формул по modus ponens. В противном случае Á называется независимой от D . Система формул Dнезависимой, если каждая формула Á из D независима от D \{Á }. называется

Система схем аксиом называется независимой, если для каждой схемы аксиом существует ее вариант, независимый от множества вариантов остальных схем аксиом.