Числення висловлень (стр. 2 из 2)
Нехай Г,A |- B. Тоді існує виведення B1,B2,...,Bn з Г,A таке, що Bn=B. Доведемо за індукцією, що для будь-якого k£n Г |- A®Bk.
Розглянемо спочатку випадок k=1, тобто формулу B1. B1, як перша формула виведення, повинна або бути аксіомою, або міститися в Г, або співпадати з A.
Зі схеми аксіоми A1 випливає, що B1®(A®B1) є аксіомою. Якщо B1 - аксіома або міститься в Г, то за правилом висновку A®B1 є вивідною з Г. Якщо ж B1=A, то з прикладу 2 маємо, що A®A, тобто A®B1 є вивідною формулою. Отже, у будь-якому випадку отримаємо Г |- A®B1.
Відтак, припустімо, що Г |- A®Bі для довільного i<k і розглянемо формулу Bk. Можливі чотири ситуації:
а) 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))F8:
A1 = (B®ØA)®((A®B)®(B®ØA))F9: MP(F4,F8) = (A®B)®(B®ØA)
F10: MP(F9,F7) = (A®B)®ØA
F11: MP(F1,F10) = ØA
Доведене твердження (метатеорему) часто називають правилом введення заперечення і записують у вигляді
Г, A |- B; Г, A |-ØB
Г |- ØA
Крім того, неважко переконатись у справедливості для числення висловлень такого твердження або метатеореми, яку можна вважати оберненою до метатеореми дедукції (ОМТД): «якщо Г |- A®B, то Г, A |- B»
Послідовно маємо
F1: A
F2: A®B
F3: MP(F1,F2) = B
2. Доведемо тепер закон виключення третього: |- AÚØA.
F1:
A6 = A®(AÚØA)F2:
(a®a) = (Ø(AÚØA))®(Ø(AÚØA)) (див.приклад 2)З формул F1 і F2 маємо (за ОМТД)
F3: Ø(AÚØA),A |- AÚØA
F4: Ø(AÚØA), A |- Ø(AÚØA)
За доведеним правилом введення заперечення у формула з F3 і F4 отримаємо:
F5: Ø(AÚØA) |- ØA.
Аналогічно використовуємо аксіому A7, в якій замість b підставляємо ØA.
A7 = ØA®(AÚØA)Ø(AÚØA), ØA |- AÚØA
Ø(AÚØA), ØA |- Ø(AÚØA)
Отримуємо
F6: Ø(AÚØA) |- ØØA.
За правилом введення заперечення з F5 і F6 дістанемо:
F7: |- ØØ (AÚØA)
F8:
A10 = ØØ(AÚØA)®(AÚØA)F9: MP(F7,F8) = AÚØA, тобто |- AÚØA.
Iснують й інші числення висловлень, тобто числення з іншими системами аксіом і правилами виведення.
Наприклад, розглянемо числення висловлень ЧВ1, яке використовує тільки логічні операції Ø і ® і має таку систему аксіом:
S1. a®(b®a)
S2. (a®(b®c))®((a®b)®(a®c))
S3. (Øa®Øb)®((Øa®b)®a)
Правилами виведення в новому численні є ті самі правила, що і в старому, тобто правило підстановки і правило висновку.
Якщо в системі аксіом першого числення замінити підформули (aÚb) на (Øa®b), а підформули (aÙb) - на Ø(a®Øb), то справедливою є така теорема.
Теорема 4. Обидва наведені числення висловлень ЧВ і ЧВ1 є рівносильними в тому смислі, що множини формул вивідних у кожному з цих числень (множини теорем цих числень) співпадають між собою.
Доведення теореми полягає в тому, що доводиться вивідність усіх аксіом першого числення з аксіом другого, і навпаки (з урахуванням зауважень відносно Ú і Ù).
Яке з двох числень краще? Однозначної відповіді на це питання немає. Друге числення є більш компактним і наочним; відповідно більш компактними є доведення різних його властивостей. У той же час, у багатшому першому численні виведення різноманітних формул є, взагалі кажучи, коротшими.
Можливі й інші числення, що рівносильні двом наведеним.