Untitled Scanned 07

(8) (q -* r) -* [p -> (q -> r)]

(9) [/> -* (.v -> r)] -> [(p -> .v) -♦ (p -* r)]

(10) O -> (.v ->f)] -> [(p -> 5) -> (p -f)]

(11) [(</ -> r) -» (.v 0] "> [((<? “* r) -* s) -> ({q -> r) -> f)]

(12) [fr/ -> r) -» [(p -»(</-* r)) -*/]] “*

(/> -*■ fa -> r))'] -> ((f/ -> r) -* 0]

(13) {(q -> r) -> [(p -* (q r)) -* ((p -♦ q) -> (p -♦ r))]} -»

-* {[(t/ -> r) -» (p -> (r/ -> r))] - [(</ -► r) - ((p -> q) - (p -* r))] \

(14) [(r/ -» r) -► (p -► (q -> r))] -* [(// - r) - ((p - r/) ->(p -> r))]

(15) (</ - r) - [(p -> r/) -> (p -> r)]

Na pierwszy rzut oka w ogóle nic widać, czy powyższy ciąg formuł istotnie jest dowodem czegokolwiek. Bliższe zbadanie sprawy rozwiewa jednak wszelkie wątpliwości. Formuła (1) jest lu bowiem aksjomatem l. (2) powstaje z (1) przez podstawienie s za q. (3) powstaje z (2) przez podstawienie całego aksjomatu 2 za p. (4) jest aksjomatem 2. (5) jest wynikiem zastosowania reguły odrywania do (3) i (4). (6) powstaje z (5) przez podstawienie formuły q -* r za s. (7) powstaje z (2) przez podstawienie formuły q -> r za p. (8) powstaje z (7) przez podstawienie p za 5. (9) powstaje z (4) przez podstawienie s za q. (10) powstaje z (9) przez podstawienie t za r. (11) powstaje z (10) przez podstawienie q -* r za p. (12) powstaje z (11) przez podstawienie p -* (r/ -> r) za s. (13) powstaje z (12) przez podstawienie (p -w/) -> (p -» r) za t. (14) uzyskano z (13) i (6) przez odrywanie. (15) otrzymano z (14) i (8) również przez odrywanie. Formuła (15) pokrywa się już z dowodzoną odmianą prawa sylogizmu hipotetycznego.

Dowody zapisywane tak jak w powyższym przykładzie są na ogół długie i mało przejrzyste. Toteż wygodnie jest notować dowody poszczególnych tez w sposób mniej kompletny, w postaci raczej tylko wskazówek, jak dowód powinien być skonstruowany. len skrótowy sposób zilustrujemy przez zastosowanie go do powyższego przykładu. Będzie to wyglądało następująco:

I) o w ó d. 1 p/[p -»(q -» r)] [(p -► q) -> (p -> r)], ąfą -» r :: 2 => (1)

(1) {q -> r) -> [[p - {q - r)] - [(p -> q) - (p -> r)]]

2 p/q -* r, q/p -* (q -* r). r/(p ->q)-*{p->r) :: (1) =o => 1 p/q -* r, q!p => 15