Числення висловлень, Детальна інформація

Наприклад, для схеми формул 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):

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

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

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

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

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

- у вигляді MP(A, A(B) = B.

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

A2 = (a((b(a))(((a(((b(a)(a))((a(a))

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

A1 = (a(((b(a)(a))

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

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

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

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

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