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

a((ba)a).

4) Знову, застосовуючи правило висновку до двох останніх формул, матимемо, що формула aa є вивідною.

Для зручності приймемо таку форму запису виведення формул у ЧВ:

а) послідовність формул виведення писатимемо в стовпчик, нумеруючи їх у порядку слідування F1, F2,....

б) поряд з кожною формулою після двокрапки писатимемо пояснення, що встановлює законність її появи у виведенні.

Правило підстановки записуватимемо у вигляді A = A(B), а правило висновку - у вигляді MP(A, AB) = B.

Тоді останнє виведення набере вигляду:

F1: A2 = (a(ba))((a((ba)a))(aa))

F2: MP(A1,F1) = ((a((ba)a))(aa))

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

F4: MP(F3,F2) = (aa)

Отже, ми довели таку метатеорему числення висловлень:  (aa).

Важливим і зручним у численні висловлень є означене вище правило виведення формули з певної множини заданих формул, яке дозволяє значно скорочувати подальші виведення.

Наведемо приклади виведення деяких формул зі заданих множин формул.

Приклад 5.3. 1). a  (ba)

F1: a

F2: MP(F1,A1) = ba

2). a,b,a(bc)  c

F1: a

F2: b

F3: a(bc)

F4: MP(F1,F3) = bc

F5: MP(F2,F4) = c

3). a,b  (ab)

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