Числення висловлень, Детальна інформація

Зі схеми аксіоми 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

A9 = (A( (B)((B( (A)

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

A2 = (A(B)(((A((B(C))((A(C))

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

F6 = ((A(B)((B( (A))(((A(B)( (A))

A1 = (B( (A)(((A(B)((B( (A))

F9: M\x2850\x3446\x462C\x2938\x3D20\x2820\x2841\x2942\x2828\x2842\x2820\x2941\x460D\x3031›\x504D\x4628\x2C39\x3746\x2029\x203D\x4128\x4228\x2829\x2820\x0D41\x3146\x3A31\x4D20\x2850\x3146\x462C\x3031\x2029\x203D\x4128

Доведене твердження (метатеорему) часто називають правилом введення заперечення і записують у вигляді

Г, A (( B; Г, A (( (B

Г (( (A

Крім того, неважко переконатись у справедливості для числення висловлень такого твердження або метатеореми, яку можна вважати оберненою до метатеореми дедукції (ОМТД): «якщо Г (( A(B, то Г, A (( B»