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

F8: A1 = (B A)((AB)(B A))

F9: MP(F4,F8) = (AB)(B A)

F10: MP(F9,F7) = (AB) A

F11: MP(F1,F10) = A

Доведене твердження (метатеорему) часто називають правилом введення заперечення і записують у вигляді

Г, A  B; Г, A  B

Г  A

Крім того, неважко переконатись у справедливості для числення висловлень такого твердження або метатеореми, яку можна вважати оберненою до метатеореми дедукції (ОМТД): «якщо Г  AB, то Г, A  B»

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

F1: A

F2: AB

F3: MP(F1,F2) = B

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

F1: A6 = A(A A)

F2: (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)

Отримуємо