ВУЗ:
Составители:
Рубрика:
§7. Исчисление секвенций
1. Аксиомы и правила вывода
Познакомимся с другой теорией, формализующей логику выска-
зываний, — исчислением секвенций. Основной конструкцией здесь яв-
ляется секвенция — выражение вида Γ ` F , где Γ — список формул,
возможно, пустой; F — формула или символ ¤
1
. Таким образом, допу-
стимы секвенции ` F (такие секвенции мы уже рассматривали; они ис-
пользуются для выражения того факта, что F есть теорема) и Γ ` (что
означает противоречивость посылок Γ). Смысл секвенции Γ ` F состо-
ит в том, что формула F выводится из гипотез Γ. Список Γ называется
антецедентом секвенции, F — консеквентом, или заключением.
Определение формулы практически не отличается от принято-
го в логике высказываний. Однако мы воспользуемся возможностью
сужения набора основных логических связок, о которой говорили в
замечании II § 5, и исключим эквиваленцию из числа основных свя-
зок. Выражение A ⇔ B определим как сокращение для формулы
(A ⇒ B) ∧ (B ⇒ A).
Множество аксиом задается с помощью одной-единственной схе-
мы. Правил вывода значительно больше — к ним относятся 10 правил
введения и удаления логических связок и одно структурное правило —
правило утончения.
Схема аксиом: F ` F .
Правила вывода:
Правила введения Правила удаления
Γ ` A; Γ ` B
Γ ` A ∧ B
Γ ` A ∧ B
Γ ` A
Γ ` A ∧ B
Γ ` B
(вв. и уд. ∧).
Γ ` A
Γ ` A ∨ B
Γ ` B
Γ ` A ∨ B
Γ, A ` C; Γ, B ` C; Γ ` A ∨ B
Γ ` C
(вв. и уд. ∨).
Γ, A ` B
Γ ` A ⇒ B
Γ ` A; Γ ` A ⇒ B
Γ ` B
(вв. и уд. ⇒).
1
Впрочем, в секвенции Γ ` ¤ символ противоречия ¤ часто опускают: Γ ` .
50
Страницы
- « первая
- ‹ предыдущая
- …
- 49
- 50
- 51
- 52
- 53
- …
- следующая ›
- последняя »
