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

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

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

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

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

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

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

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

(a ®(b ®a ))®((a ®((b ®a )®a ))®(a ®a ))

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

a ®(b ®a ) і (a ®(b ®a ))®((a ®((b ®a )®a ))®(a ®a ))

за правилом висновку виводимо формулу

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

3) Замінимо в аксіомі A 1 b на (b ®a ):

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

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

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

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

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

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

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

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

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

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

F 4: MP(F 3,F 2) = (a ®a )

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

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

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

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

F 1: a