Формальная логика

ТЕОРЕМА 10. (1) Если AB, то AB.

Следствие. Если A₁( A₂ ... (A_mB) ...), то A₁, ..., A_m  (m1).

(2) Если A₁, ..., A_m  то A₁, ..., A_m-1 A_mB (m1).

Д о к а з а т е л ь с т в о (2):

Формулы данного вывода (I):A₁,..., A_m обозначим списком B₁, ..., B_l. Переделаем вывод (I)в схему :

A_{m } B₁

A_m  B_i

A_m  B_{l ,}

a затем в вывод (11), обосновав выводимость каждой импликации A_m B_i

(i=1,...,l) из списка гипотез A₁,...,A_{m -1} .

1случай: Если B_i есть аксиома или одна из гипотез A_j (j=1,...,m-1) в вы воде (I), то B_i также входит и в вывод (II), так что вхождение импликации A_mB_i в вывод (II) имеет обоснование с помощью аксиомы 1а:

B_i

Bi (A_m B_i) (аксиома 1a)

A_m B_i (modus ponens)

2 случай: Если B_i есть гипотеза A_m в выводе (I), то доказательство импликации A_mA_m приведено в примере 1.

3 случай: B_i получена в выводе (I) из предыдущих формул B_p, B_q=B_pB_i по правилу modus ponens. Обоснование вхождения импликации A_m  B_i в вывод (II) проводится с помощью аксиомы 1б индукцией по построению вывода (11) :

A_mB_p (по индукционному допущению)

A_m(B_pB_i) (по индукционному допущению)

(A_mB_p)((A_m(B_pB_i)) (A_mB_i)) (аксиома 1б)

(A_m(B_pB_i)) (A_mB_i) (modus ponens)

A_m  B_i (modus ponens)

Пример, иллюстрирующий доказательство теоремы о дедукции :

Если AB, CA, C |– B, то A B, CA |– C B.

Вывод (I):

1. A B (гипотеза из списка A₁,...,A_{m -1} )

2. C A (гипотеза из списка A₁,...,A_{m –1} )

3. C (гипотеза A_m )

4. A (modus ponens, 3,2)

5. B (modus ponens, 4,1)

Вывод (II):

AB (гипотеза из списка A₁,...,A_{m –1} )

(A B)(С(AB)) (аксиома 1а)

1^* C(AB) (modus ponens)

СA (гипотеза из списка A₁,...,A_{m –1} )

(СA)(С(CA)) (аксиома 1а)

2^* С(CA) (modus ponens)

С(CC) (аксиома 1а)

(С(CC))((С((СС)С))(СС)) (аксиома 1б)

(С((СС)С))(СС) (modus ponens)

С((СС)С) (аксиома 1а)

3^* CС (modus ponens)

(CC)((C(CA))(CA)) (аксиома 1б)

(C(CA))(CA) (modus ponens)

4^* CA (modus ponens)

(CA)((C(AB))(CB)) (аксиома 1,б)

(C(AB))(CB) (modus ponens)

5^* CB (modus ponens)

Д о к а з а т е л ь с т в о следует из того, что аксиомы выбираются среди тавтологий, а правила вывода сохраняют истинность заключения при истинных посылках.

(AC)((BC)(ABC)) (удаление )

(AB)(AB), (AB)(AB)
(введение )

AA

(AB)((A B) A)

A(AC)

Д о к а з а т е л ь с т в о.

1) : 3)