logo
практикум по мат

2.4.2. Эквивалентные формулы исчисления предикатов

Утверждение 2. В ИПΣ выполнимы все эквивалентности ИВ из теоремы 3.

Утверждение 3. Пусть φ, ψ – формулы ИПΣ переменная x не является свободной переменной формулы ψ, переменная у не является свободной переменной формулы φ. Тогда

1) ¬xφ≡x¬φ, 1΄) ¬xφ≡x¬φ,

2) x(φ∧ψ)≡xφ∧ψ, 2΄) x(φ∨ψ)≡xφ∨ψ,

3) x(φ∨ψ)≡xφ∨ψ, 3΄) x(φ∧ψ)≡xφ∧ψ,

4) xφ≡x(φ)4΄)xφ≡x(φ)

Доказательство. Докажем эквивалентность 1). Построим квазивывод формулы ¬xφ→x¬φ из Ø:

  1. φ→xφ (схема аксиом 12);

  2. ¬xφ→¬φ (к п.1 применили свойство контрапозиции);

  3. ¬xφ→x¬φ (к п.2 применили правило вывода 2). Построим квазивывод формулы x¬φ→¬xφ из Ø:

  1. x¬φ→¬φ (схема аксиом 11);

  2. ¬¬φ→¬x¬φ ( к п.1 применили свойство контрапозиции);

  3. φ→¬¬φ (тавтология);

  4. φ→¬x¬φ (к пп.3 и 2 применили свойство транзитивности);

  5. xφ→¬x¬φ (к п. 4 применили правило вывода 3);

  6. ¬¬x¬φ→¬xφ ( к п.5 применили свойство контрапозиции);

  7. x¬φ→¬¬x¬φ (тавтология);

  8. x¬φ→¬xφ (к пп.7 и 6 применили свойство транзитивности).

Докажем эквивалентность 3΄). Построим квазивывод формулы

x(φ∧ψ)→xφ∧ψ из Ø:

  1. x(φ∧ψ)→φ∧ψ (схема аксиом 11);

  2. φ∧ψ→φ (схема аксиом 3);

  3. x(φ∧ψ)→φ (к пп.1 и 2 применили свойство транзитивности);

  4. x(φ∧ψ)→xφ (к п.3 применили правило вывода 2);

  5. φ∧ψ→ψ (схема аксиом 4);

  6. x(φ∧ψ)→ψ (к пп.1 и 5 применили свойство транзитивности);

  7. (x(φ∧ψ)→xφ)→((x(φ∧ψ)→ψ)→(x(φ∧ψ)→xφ∧ψ)) (схема аксиом 5);

  8. (x(φ∧ψ)→ψ)→(x(φ∧ψ)→xφ∧ψ) (к пп. 4 и 7 применили правило вывода 1);

  9. x(φ∧ψ)→xφ∧ψ (к пп. 6 и 8 применили правило вывода 1).

Построим квазивывод формулы xφ∧ψ→x(φ∧ψ) из Ø:

  1. xφ∧ψ→xφ (схема аксиом 3);

  2. xφ→φ (схема аксиом 11);

  3. xφ∧ψ→φ (к пп. 1 и 2 применили свойство транзитивности);

  4. xφ∧ψ→ψ (схема аксиом 4);

  5. (xφ∧ψ→φ)→((xφ∧ψ→ψ)→(xφ∧ψ→φ∧ψ)) (схема аксиом 5);

  6. (xφ∧ψ→ψ)→(xφ∧ψ→φ∧ψ) (к пп. 3 и 5 применили правило вывода 1);

  7. xφ∧ψ→φ∧ψ (к пп. 4 и 5 применили правило вывода 1);

  8. xφ∧ψ→x(φ∧ψ) (к п. 6 применили правило вывода 2).

Теорема 2 (о замене). Пусть φ ‑ формула ИПΣ, ψ ‑ ее подформула, φ' получается из φ заменой некоторого вхождения ψ на формулу ψ' ИПΣ и ψ≡ψ'. Тогда φ≡φ'.

Теорема 3. Для любой формулы φ ИПΣ существует ПНФ ψ, эквивалентная в ИПΣ формуле φ.