ВУЗ:
Составители:
Рубрика:
Применяя правило введения противоречия, важно правильно по-
добрать формулу A.
Часто значительное упрощение доказательства дают допустимые
правила вывода (см. следующий пункт).
Чтобы не пойти по тупиковому пути при построении доказатель-
ства, следует постоянно проверять, можно ли вообще вывести те се-
квенции, к которым мы пришли. Если речь идет о секвенции вида
Γ ` A, то в силу полноты исчисления секвенций (см. п. 4) для этого
достаточно проверить, имеет ли место логическое следование Γ |= A.
3. Эквивалентность и допустимые правила
вывода
Говорят, что формулы F и G эквивалентны в смысле исчисления
секвенций, если доказуемы секвенции F ` G и G ` F . Будем записы-
вать в таком случае F ≡ G.
Пример 4. Докажем эквивалентность A ≡ ¬¬A .
¬A ` ¬A
¬¬A, ¬A ` ¬A
¬¬A ` ¬¬A
¬¬A, ¬A ` ¬¬A
¬¬A, ¬A `
¬¬A ` A
(уд.¤)
(вв.¤).
Из построенного доказательства секвенции ¬¬A ` A ясно, что и се-
квенция ¬¬¬A ` ¬A является доказуемой. Используем это:
A ` A
A, ¬¬¬A ` A
¬¬¬A ` ¬A
A, ¬¬¬A ` ¬A
A, ¬¬¬A `
A ` ¬¬A
(уд.¤)
(вв.¤).
Чтобы не иметь дело с длинными цепочками отрицаний, можно
ввести правила введения отрицания и удаления двойного отрицания:
Γ, A `
Γ ` ¬A
Γ ` ¬¬A
Γ ` A
(вв. ¬ и уд. ¬¬).
Правило называется допустимым, если его добавление к списку
правил вывода не расширяет множество доказуемых секвенций.
Теорема 1. Следующие правила являются допустимыми:
53
Страницы
- « первая
- ‹ предыдущая
- …
- 52
- 53
- 54
- 55
- 56
- …
- следующая ›
- последняя »
