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

2.4.3. Теорема Геделя о полноте. Непротиворечивость исчисления предикатов

Теорема 4. Все доказуемые в ИП^Σ формулы являются тождественно истинными.

Доказательство проводим индукцией по длине вывода формулы. Очевидно, что аксиомы ИП^Σ являются тождественно истинными. Проверку того, что правила вывода 1-3 сохраняют тождественную истинность, мы оставляем читателю в качестве упражнения.

Следствие 3. ИП^Σ непротиворечиво, т.е. не все формулы ИП^Σ доказуемы в ИП^Σ.

В ИП^Σ справедлив аналог теоремы о полноте в исчислении высказываний.

Теорема 5 (Геделя о полноте). Формула φ исчисления ИП^Σ доказуема тогда и только тогда, когда φ тождественно истинна.

Таким образом, проверка доказуемости формулы φ сводится к проверке ее тождественной истинности. Однако в отличие от ИВ, в общем случае не существует алгоритма распознавания доказуемости формул ИП^Σ, т. е. ИП^Σ неразрешимо. Тем не менее, если в формуле φ "записать", что каждая переменная может принимать конечное число значений, то перебором всех возможных систем можно установить, является ли формула тождественно истинной или нет.