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

A(B)

2) правило висновку (modus ponens). Якщо A і AB - вивідні формули, то вивідною є й формула B; записується

A, AB

B

У поданому описі числення висловлень аксіоми є формулами числення (відповідними до означення формули); формули, що використовують у правилах виведення (A, AB тощо), є метаформулами, або так званими схемами формул.

Схема формул - це вираз метамови для позначення нескінченної множини всіх тих формул числення, які отримують після заміни змінних метамови (метазмінних) цієї схеми певними формулами числення.

Наприклад, для схеми формул AB, якщо замінити A на p, а B - на pq, то з даної схеми отримаємо формулу числення p(pq); якщо ж метазмінну A замінити на pq, а B - на (pq)p, то дістанемо формулу (pq)((pq)p) тощо.

Використання схем формул можна поширити і на всі аксіоми. Наприклад, якщо в системі аксіом пропозиційні змінні a,b,c замінити метазмінними A,B,C, то отримаємо десять схем аксіом, що задають десять нескінченних множин аксіом. Таким чином приходимо до іншого способу побудови числення висловлень: з нескінченною множиною аксіом (що задається скінченним числом схем аксіом), але без правила підстановки, оскільки воно неявно міститься у поясненні (інтерпретації) схем аксіом.

Перший спосіб є більш послідовно конструктивним: всі його засоби явно зафіксовані і скінченні; при введенні числення в ЕОМ (наприклад, для автоматизації доведень теорем та побудови виведень для заданих формул) він виглядає природнішим.

З іншого боку, другий спосіб більш відповідає математичній традиції тлумачення (інтерпретації) формул: наприклад, алгебраїчна тотожність (a+b)2=a2+2ab+b2 або відомі логарифмічні чи тригонометричні тотожності тлумачаться саме як схеми тотожностей, а не конкретні тотожності, справедливі лише для конкретних літер. Правило підстановки при цьому мається на увазі і присутнє неявно. Втім, досить очевидно, що перехід від одного способу побудови числення до іншого є нескладним.

Аксіоми числення висловлень разом з правилами виведення повністю визначають поняття довідної (вивідної) формули у ЧВ, або теореми ЧВ.

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

Розглянемо приклади виведення теорем ЧВ.

Приклад 5.2. Доведемо, що формула aa є теоремою ЧВ.

1) Підставляючи в аксіому A2 змінну a замість змінної c і ba замість b, матимемо вивідну формулу

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

2) Підформула a(ba) є аксіомою A1. Тоді з вивідних формул

a(ba) і (a(ba))((a((ba)a))(aa))

за правилом висновку виводимо формулу(a((ba)a))(aa)).

3) Замінимо в аксіомі A1 b на (ba):