49
15 qhą -» ~\p, r/(p - "iq) -> ip, pfp -*q ::
:: (1)=» 3=> 30
Aby jeszcze bardziej skrócić opisy dowodów poszczególnych tez, nic będziemy w dalszym ciągu zaznaczali wszystkich podstawień w pierwszych częściach (przed znakiem ::) informacji dowodowych. Więc np. pierwszą informację dowodową w dowodzie tezy 30, napisalibyśmy tak:
21 :: 28 p/q => 16 p/nq. qf-\p, rfą =* (1)
Informację tę można rozumieć w tym ujęciu następująco: używając prawa 21 można z prawa 28 i prawa 16 przekształconych przez wykonanie zaznaczonych podstawień wyprowadzić (1). Jakie należy przy tym wykonać podstawienia w 21, łatwo się domyślić. Wystarczy tylko przyjrzeć się prawom 28 i 16 i wykonać zaznaczone podstawienia; ewentualnie można jeszcze przyjrzeć się tezie (1). Zupełnie analogicznie można sobie poradzić we wszystkich innych przypadkach tego rodzaju.
§ 4. TEZY ZE ZNAKIEM KONIUNKCJI
31. p -> (q p a </) Prawo koniunkcji
D o w ó d. 16 :: 1 => 8 p/q, q/p, r/ą => (1 j (1) P~* [(4 -* </) (‘i - P A 4)]
17 :: (1)=> 18 p/q => 31
32. [/> -> (q -* r)] -► (p a q -* r) Prawo importacji
D o w ó d. 16 p/p a q :: 7 => (l)
(1) (ą -» r) -»(p a q->r)
15 q/q -»r, rfp a q-* r : : (1) => (2)
(2) [p - {q -* r)j -> [p -> (p a q -» r)]
16 :: (2) => 17 ę/p Ar/=>(3)
(3) [/> ->(q -* r)] -> lp a q -* (/; -> r)]
16 :: (3)=>2 p/p a q, q/p=>(4)
(4) (>-*(</-* r)] - [(/> a q -/>)-(/> a q -> r)]
i