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

Послідовно маємо

F1: A

F2: A(B

F3: MP(F1,F2) = B

2. Доведемо тепер закон виключення третього:  (( A ( (A.

A6 = A((A( (A)

(a(a) = (((A( (A))((((A( (A)) (див.приклад 2)

З формул F1 і F2 маємо (за ОМТД)

F3: ((A( (A),A  ((  A( (A

F4: ((A( (A), A  ((  ((A( (A)

За доведеним правилом введення заперечення у формула з F3 і F4 отримаємо:

F5: ((A( (A)  ((  (A.

Аналогічно використовуємо аксіому A7, в якій замість b підставляємо (A.

A7 = (A((A( (A)

((A( (A), (A  ((  A( (A

((A( (A), (A  ((  ((A( (A)

Отримуємо

F6: ((A( (A)  ((  ((A.

За правилом введення заперечення з F5 і F6 дістанемо:

F7:  ((  (( (A( (A)

A10 = (((A( (A)((A( (A)

F9: MP(F7,F8) = A( (A, тобто  (( A( (A.

Iснують й інші числення висловлень, тобто числення з іншими системами аксіом і правилами виведення.

Наприклад, розглянемо числення висловлень ЧВ1, яке використовує тільки логічні операції ( і ( і має таку систему аксіом:

S1. a((b(a)

S2. (a((b(c))(((a(b)((a(c))

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

Правилами виведення в новому численні є ті самі правила, що і в старому, тобто правило підстановки і правило висновку.

Якщо в системі аксіом першого числення замінити підформули (a(b) на ((a(b), а підформули (a(b) - на ((a( (b), то справедливою є така теорема.

Теорема 4. Обидва наведені числення висловлень ЧВ і ЧВ1 є рівносильними в тому смислі, що множини формул вивідних у кожному з цих числень (множини теорем цих числень) співпадають між собою.