Теорема про дедукцію у вирахуванні висловлювань

Теорема 1(про дедукцію). Нехайφ1,…,φm,φ,ψ– формули ІВ. Тодіφ1,…,φm,φ⊢ψ

φ1,…,φm,⊢φ →ψ.

Рішення.За теоремою про дедукцію

φ→ψ⊢¬ψ→¬φ

φ→ψ, ¬ψ⊢¬φ.

φ→¬ψ(до пп. 2 та 5 застосували правило виведення);

¬φ(до пп. 6 та 4 застосували правило виведення).

Рішення.За теоремою про дедукцію

φ→(ψ→χ)⊢ψ→(φ→χ)

φ→(ψ→χ),ψ⊢(φ→χ)

φ→(ψ→χ),ψ,φ⊢χ.

4)ψ→χ(до пп. 2 та 1 застосували правило виведення);

5)χ(до пп. 3 та 4 застосували правило виведення).

Теорема про заміну в обчисленні висловлювань

Формулиφіψназвемоеквівалентними(позначимоφ≡ψ),якщо

Примітка 2.Для будь-яких формулφіψІВ

φ≡ψ

⊢φ→ψта ⊢ψ→φ.

Твердження 1.Відношення≡є ставленням еквівалентності на безлічі формул ВВ, тобто. для будь-яких формулφ,ψ, χІВ:

b)φ≡ψ

ψ≡φ;

с)φ≡ψ,ψ≡x

φ≡x.

Теорема 2(про заміну). Нехайφ- формула ІВ,ψ- її підформула,φ'виходить зφзаміною деякого входженняψна формулуψ'ІВ іψ≡ψ'.Тодіφ≡φ'.

Властивості виведених та еквівалентних формул обчислення висловлювань

Твердження 3.Нехайφ,ψ, χ –формули ІВ. Тоді

φ,ψ⊢φ

ψ;

Доказ.Пункти 1, 4, 6, 8 доведені в прикладах 13, 14, 16, 17.

Доведемо пункт 7. Покажемо, щоφ→(ψ→χ)⊢φ

ψ→χ.За теоремою про дедукцію

φ→(ψ→χ)⊢φ

ψ→χ

φ→(ψ→χ),φ

ψ⊢χ.

Будуємо висновок формулиχз формулφ→(ψ→χ),φ

ψ:

φ

ψ(гіпотеза);

φ

ψ→φ(схема аксіом 3);

φ(до пп. 2 та 4 застосували правило виведення);

φ

ψ→ψ(схема аксіом 4);

ψ(до пп. 2 та 5 застосували правило виведення);

ψ→χ(до пп. 4 та 1 застосували правило виведення);

χ(до пп. 6 та 7 застосували правило виведення).

Покажемо, щоφ

ψ→χ⊢φ→(ψ→χ).За теоремою про дедукцію

φ

ψ→χ⊢φ→(ψ→χ)

φ

ψ→χ,φ⊢φ →χ

φ

ψ→χ,φ,ψ⊢χ.

Будуємо квазівиведення формулиχз формулφ

ψ→χ,φ,ψ:

φ

ψ→χ(гіпотеза);

φ

ψ(до п.п. 2 і 3 застосували властивість 4);

χ(до пп. 4 та 1 застосували правило виведення).

Основні еквівалентності обчислення висловлювань

Теорема 3.Нехайφ,ψ, χ- формули ІВ. Тоді мають місце такі еквівалентності:

---