Числення висловлень

Зі схеми аксіоми A1 випливає, що B1(AB1) є аксіомою. Якщо B1 - аксіома або міститься в Г, то за правилом висновку AB1 є вивідною з Г. Якщо ж B1=A, то з прикладу 2 маємо, що AA, тобто AB1 є вивідною формулою. Отже, у будь-якому випадку отримаємо Г  AB1.

Відтак, припустімо, що Г  ABі для довільного i
а) Bk - аксіома;

б) Bk міститься у Г;

в) Bk = A;

г) Bk є вивідною з деяких попередніх формул Bj та Bl за правилом висновку; у цьому випадку формула Bl повинна мати вигляд BjBk.У випадках а), б), в) доведення твердження Г  ABk здійснюється аналогічно доведенню для B1 (випадки а) і б) - за допомогою схеми аксіоми A1; випадок в) - за допомогою результату прикладу 5.2).

У випадку г) за індуктивним припущенням маємо Г  ABj і Г  ABl, де Bl - це Bj Bk, тобто Г  A(Bj Bk).

Підставимо у схему аксіоми A2 A замість a, Bj замість b і Bk замість c. Дістанемо (ABj)  ((A(Bj  Bk))  (ABk)).

Застосовуючи до останньої вивідної формули двічі правило висновку, отримаємо Г  ABk. Залишилось покласти k=n.

Розглянемо декілька застосувань метатеореми дедукції.

1. Дуже поширеним методом математичних доведень є метод доведення від супротивного: припускаємо, що A є вірним (істинним твердженням), і доводимо, що, по-перше, з A виводиться B, а по-друге, що з A виводиться B, що неможливо; отже, A невірно, тобто вірно A.

У термінах числення висловлень цей метод формулюється так:

«якщо Г, A  B і Г,A  B, то Г  A».

Доведемо справедливість цього правила у численні висловлень.

Справді, за теоремою дедукції, якщо

Г, A  B і Г, A  B, то Г  AB і Г  A B

F1: AB

F2: A B

F3: A9 = (A B)(B A)

F4: MP(F2,F3)=B A

F5: A2 = (AB)((A(BC))(AC))

F6: MP(F1,F5) = (A(BC))(AC)

F7: F6 = ((AB)(B A))((AB) A))