Составители:
Рубрика:
∃x[P(x) \/ Q(x)] ↔ [∃x P(x) \/ ∃x Q(x)],
(2.5)
∃x[P(x) & P] ↔ [∃x P(x) & P].
(2.6)
Законы пронесения кванторов через импликацию:
∀x[P(x) → Q(x)] → [∀x P(x) → ∀x Q(x)],
(2.7)
∀x[P(x) → Q(x)] → [∃x P(x) → ∃x Q(x)],
(2.8)
∀x[P(x) → Q] ↔ [∃x P(x) → Q].
(2.9)
Законы удаления квантора общности и введения квантора
существования:
∀x P(x) → P(x),
(2.10)
P(x) → ∃x P(x).
(2.11)
Законы преобразования категорических высказываний:
∀x[P(x) → Q(x)] ↔ ⎤∃x[P(x) &⎤Q(x)],
(2.12)
∀x[P(x) → ⎤Q(x)] ↔ ⎤∃x[P(x) & Q(x)].
(2.13)
Все формулы исчисления предикатов можно разделить на три
типа:
• истинные при любой интерпретации, т.е. общезначимые;
• ложные при любой интерпретации, т.е. противоречивые;
• формулы, истинность которых зависит от интерпретации.
Чтобы определить тип формулы, то сначала следует попытаться
установить общезначимость или противоречивость заданной
формулы (тем более, что для одноместных предикатов это
алгоритмически разрешимая задача) и, если это не удается сделать,
то перейти к установлению значения истинности формулы для
заданной интерпретации, например так, как было показано выше в
примере 2.11.
Пример 2.12. Требуется установит тип формулы
∀x(⎤P(x) → ⎤Q(x)) ↔ ⎤∃x(⎤P(x) & Q(x)).
Попытаемся установить общезначимость или противоречивость данной
формулы. Для этого левую часть заданной эквивалентности заменим
равносильной формулой ∀x(P(x) \/ ⎤Q(x) на основе (1.38), а правую часть -
формулой ∀x⎤(⎤P(x) & Q(x)) на основе (2.2). Далее, с учетом (1.14), правая часть
примет вид ∀x(P(x) \/ ⎤Q(x)), т.е. исходная формула преобразована к виду
110
Страницы
- « первая
- ‹ предыдущая
- …
- 24
- 25
- 26
- 27
- 28
- …
- следующая ›
- последняя »