Реферат: Числення висловлень

а) B_k - аксіома;

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

в) B_k = A ;

г) B_k є вивідною з деяких попередніх формул B_j та B_l за правилом висновку; у цьому випадку формула B_l повинна мати вигляд B_j ®B_k .

У випадках а), б), в) доведення твердження Г |- A ®B_k здійснюється аналогічно доведенню для B ₁ (випадки а) і б) - за допомогою схеми аксіоми A 1; випадок в) - за допомогою результату прикладу 5.2).

У випадку г) за індуктивним припущенням маємо Г |- A ®B_j і Г |- A ®B_l , де B_l - це B_j ®B_k , тобто Г |- A ®(B_j ®B_k ).

Підставимо у схему аксіоми A 2 A замість a , B_j замість b і B_k замість c . Дістанемо (A ®B_j ) ® ((A ®(B_j ®B_k )) ® (A ®B_k )).

Застосовуючи до останньої вивідної формули двічі правило висновку, отримаємо Г |- A ®B_k . Залишилось покласти k =n .

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

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

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

«якщо Г, A |- B і Г,A |- ØB , то Г |- ØA ».

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

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

Г, A |- B і Г, A |- ØB , то Г |- A ®B і Г |- A ®ØB

F 1: A ®B

F 2: A ®ØB

F 3: A 9 = (A ®ØB )®(B ®ØA )

F 4: MP(F 2,F 3)=B ®ØA

F 5: A 2 = (A ®B )®((A ®(B ®C ))®(A ®C ))

F 6: MP(F 1,F 5) = (A ®(B ®C ))®(A ®C )

F 7: F 6 = ((A ®B )®(B ®ØA ))®((A ®B )®ØA ))

F 8: A 1 = (B ®ØA )®((A ®B )®(B ®ØA ))

F 9: MP(F 4,F 8) = (A ®B )®(B ®ØA )

F 10: MP(F 9,F 7) = (A ®B )®ØA

F 11: MP(F 1,F 10) = ØA

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

Г, A | - B ; Г, A | - Ø B

Г |- ØA