Классическое исчисление высказываний. Исчислением высказываний называют исчисление, в котором в качестве алфавита взят алфавит логики высказываний

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

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

1. α ® (b ® α),
2. (α ® (b ® γ)) ® ((α ® b) ® (α ® γ)),
3. (α Ù b) ® α,
4. (α Ù b) ® b,
5. α ® (α Ú b),
6. b ® (α Ú b),
7. (α ® b) ® ((α ® γ) ® (α ® (b Ù γ)),
8. (α ® γ) ® ((b ® γ) ® ((α Ú b) ® γ)),
9. (α ® b) ® (Øb ® Øα),
10. α ® ØØα,
11. ØØα ® α.

Классическое исчисление высказываний использует два правила вывода:

• Modus ponens. Из истинности условия импликации и истинности самой импликации следует истинность следствия импликации: α, α®b├ b.
• Правило одновременной подстановки. Из формулы α(р), где р – переменная, выводима формула α(R), где R – формула, получаемая заменой в α(р) каждого вхождения переменной р на формулу R: α (р) ├ α (R). В общем случае будем обозначать подстановку (x₁,…, x_n ò α ₁,…, α _n).

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

Натуральное исчисление высказываний

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

• Исключение конъюнкта. Из истинности конъюнкции следует истинность любого ее конъюнкта:

α₁ Ù α₂ Ù … Ù α_n ├ α_i.

• Введение конъюнкции. Из списка истинных формул следует истинность их конъюнкции:

α₁, α₂, …, α_n ├ α₁ Ù α₂ Ù … Ù α_n.

• Введение дизъюнкции. Из истинности формулы следует истинность ее дизъюнкции с любыми другими формулами:

α₁ ├ α₁ Ú α₂ Ú … Ú α_n.

• Исключение двойного отрицания. Из истинности двойного отрицания формулы следует истинность ее самой:

ØØα ├ α.

• Простая резолюция (удаление дизъюнкта). Из истинности дизъюнкции и отрицания одного из ее дизъюнктов следует истинность формулы после удаления этого дизъюнкта:

α Ú b, Øb ├ α.

• Резолюция. Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая его отрицание следует формула, являющаяся дизъюнкцией исходных формул после удаления этого дизъюнкта:

α Ú b, Øb Ú γ ├ α Ú γ.