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

F1: A5 = ((aa)((ab)(a(ab))))

F2: (aa) (див.приклад 5.2)

F3: MP(F2,F1) = ((ab)(a(ab)))

F4: b

F5: A1 = (b(ab))

F6: MP(F4,F5) = ab

F7: MP(F6,F3) = (a(ab))

F8: a

F9: MP(F8,F7) = (ab)

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

Лема 1. Якщо  B, то Г  B.

Лема 2. Якщо A1,A2,...,An  B, то A1,A2,...,An,Г  B.

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

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

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

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

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

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

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

Нехай Г,A  B. Тоді існує виведення B1,B2,...,Bn з Г,A таке, що Bn=B. Доведемо за індукцією, що для будь-якого kn Г  ABk.

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