Предикатов

Утверждение 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. Для любой формулы φ ИП^Σ существует ПНФ ψ, эквивалентная в ИП^Σ формуле φ;.