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

2). a ,b ,a ®(b ®c ) |-c

F 1: a

F 2: b

F 3: a ®(b ®c )

F 4: MP(F 1,F 3) = b ®c

F 5: MP(F 2,F 4) = c

3). a ,b |- (a Ùb )

F 1: A 5 = ((a ®a )®((a ®b )®(a ®(a Ùb ))))

F 2: (a ®a ) (див.приклад 5.2)

F 3: MP(F 2,F 1) = ((a ®b )®(a ®(a Ùb )))

F 4: b

F 5: A 1 = (b ®(a ®b ))

F 6: MP(F 4,F 5) = a ®b

F 7: MP(F 6,F 3) = (a ®(a Ùb ))

F 8: a

F 9: MP(F 8,F 7) = (a Ùb )

Безпосередньо з означення поняття вивідності випливають такі очевидні твердження для довільної множини формул Г.

Лема 1. Якщо |-B , то Г |-B .

Лема 2. Якщо A ₁ ,A ₂ ,...,A_n |-B , то A ₁ ,A ₂ ,...,A_n ,Г |-B .

Лема 3. Якщо Г |-A і A |-B , то Г |-B (транзитивність відношення вивідності).

Будь-яку доведену у численні вивідність вигляду Г |- A , де Г - множина формул, A - довільна формула, можна розглядати як правило виведення , яке можна додати до заданої множини правил.

Наприклад, доведену у прикладі 3(1) вивідність a |-b ®a разом з правилом підстановки можна розглядати як правило , що може бути інтерпретовано так: «якщо формула A є вивідною, то вивідною є і формула B ®A , де B - довільна формула». Це правило надалі можна використовувати для побудови нових виведень. Такі правила називатимемо похідними правилами . За допомогою додаткових похідних правил дістаємо можливість скоротити виведення формул, не виконуючи повного виведення. Маючи скорочене виведення, завжди можна побудувати повне виведення, замінюючи кожну формулу, яка є результатом застосування похідного правила виведення, на повне її виведення. Такою формулою є, наприклад, формула F 2 у прикладі 3(3). Iнакше кажучи, похідні правила - це будівельні блоки при побудові виведень формул ЧВ, кожен з яких замінює кілька кроків звичайного виведення.

Могутнім засобом одержання ряду важливих і корисних похідних правил виведення є так звана метатеорема дедукції (МТД ); зокрема, сама МТД може розглядатись як таке похідне правило.

Теорема 3 (метатеорема дедукції ). Якщо Г,A |- B , то Г |- A ®B , де Г - множина формул (можливо, порожня), A і B - формули.

Доведення . Зауважимо, що доведення метатеорем на відміну від теорем числення проводиться змістовно як звичайне математичне доведення.

Будемо виходити з того, що задані аксіоми є схемами аксіом, тобто не будемо користуватись правилом підстановки.

Нехай Г,A |- B . Тоді існує виведення B ₁ ,B ₂ ,...,B_n з Г,A таке, що B_n =B . Доведемо за індукцією, що для будь-якого k £n Г |- A ®B_k .

Розглянемо спочатку випадок k =1, тобто формулу B ₁ . B ₁ , як перша формула виведення, повинна або бути аксіомою, або міститися в Г, або співпадати з A .

Зі схеми аксіоми A 1 випливає, що B ₁ ®(A ®B ₁ ) є аксіомою. Якщо B ₁ - аксіома або міститься в Г, то за правилом висновку A ®B ₁ є вивідною з Г. Якщо ж B ₁ =A , то з прикладу 2 маємо, що A ®A , тобто A ®B ₁ є вивідною формулою. Отже, у будь-якому випадку отримаємо Г |- A ®B ₁ .