Hilbert II Subject: Deduction of propositional logic due to Hilbert and Ackermann [1928] Date: 2003-12-17 Version: $Revision: 1.1 $ Author(s): Michael Meyling, Franz Fritsche Def -> a -> b =df -a v b HA1 a v a -> a HA2 a -> a v b HA3 a v b -> b v a HA4 (a -> b) -> (c v a -> c v b) Th. 1 // Form zum Hypothetischen Syllogismus (a -> b) -> ((c -> a) -> (c -> b)) Bew: (a -> b) -> (-c v a -> -c v b) (nach HA4) (a -> b) -> ((c -> a) -> (c -> b)) (Def ->) Regel HS // Hypothetischer Syllogismus a -> b, b -> c -------------- a -> c Bew: a -> b (Vor) b -> c (Vor) (a -> b) -> ((c -> a) -> (c -> b)) (Th. 1) (b -> c) -> ((a -> b) -> (a -> c)) (Subst) (a -> b) -> (a -> c) (MP) a -> c (MP) Th. 2 a -> a Bew: a -> a v a (nach HA2) a v a -> a (HA1) a -> a (HS) Th. 3 -a v a Bew: a -> a (Th. 2) -a v a (Def ->) Th. 4 a v -a Bew: -a v a (Th. 3) a v -a (nach HA3) Th. 5 a -> --a Bew: a v -a (Th. 4) -a v --a (Subst) a -> --a (Def ->) Th. 6 --a -> a Bew: -a -> ---a (nach Th. 5) a v -a -> a v ---a (nach HA4) a v -a (Th. 4) a v ---a (MP) ---a v a (nach HA3) --a -> a (Def ->) Th. 7 (a -> b) -> (-b -> -a) Bew: b -> --b (Th. 5) -a v b -> -a v --b (nach HA4) -a v --b -> --b v -a (nach HA3) -a v b -> --b v -a (HS) (a -> b) -> (-b -> -a) (Def ->) Regel ORK a -> b ---------------- a v c -> b v c Bew: a -> b (Vor) c v a -> c v b (HA4) c v b -> b v c (HA3) c v a -> b v c (HS) a v c -> c v a (HA3) a v c -> b v c (HS) Regel EQUI a -> b b -> a ------------ A(a) -> A(b) A(b) -> A(a) Bew: a -> b (Vor) (a -> b) -> (-b -> -a) (Th. 7) -b -> -a (MP) (a -> b) -> (c v a -> c v b) (HA4) c v a -> c v b (MP) a v c -> b v c (ORK) analog für b -> a rekursiver Aufbau von A(a) -> A(b) (u.a. mit Def ->) Th. 8 (a -> b) -> (a v c -> b v c) Bew (a): (a -> b) -> (c v a -> c v b) (HA4) (a -> b) -> (a v c -> b v c) (EQUI HA3, 2-mal) Bew (b): (a -> b) -> (c v a -> c v b) (HA4) c v b -> b v c (HA3) (-(c v a) v (c v b)) -> (-(c v a) v (b v c)) (nach HA4) (c v a -> c v b) -> (c v a -> b v c) (Def ->) * (a -> b) -> (c v a -> b v c) (HS) a v c -> c v a (HA3) -(c v a) -> -(a v c) (nach Th. 7) ((b v c) v -(c v a)) -> ((b v c) v -(a v c)) (HA4) ((b v c) v -(a v c)) -> (-(a v c) v (b v c)) (nach HA3) ((b v c) v -(c v a)) -> (-(a v c) v (b v c)) (HS) (-(c v a) v (b v c)) -> ((b v c) v -(c v a)) (nach HA3) (-(c v a) v (b v c)) -> (-(a v c) v (b v c)) (HS) (c v a -> b v c) -> (a v c -> b v c) (Def ->) (a -> b) -> (a v c -> b v c) (HS *) Th. 9 a -> b v a Bew: a -> a v b (HA2) a v b -> b v a (HA3) a -> b v a (HS) Th. 10 a v (b v c) -> b v (a v c) Bew: c -> a v c (nach Th. 9) b v c -> b v (a v c) (nach HA4) a v (b v c) -> a v (b v (a v c)) (nach HA4) * a v (b v c) -> (b v (a v c)) v a (EQUI HA3) a -> b v a (Th. 9) a v c -> b v (a v c) (Subst) a -> a v c (nach HA2) a -> b v (a v c) (HS) (b v (a v c)) v a -> (b v (a v c)) v (b v (a v c)) (nach HA4) (b v (a v c)) v a -> b v (a v c) (EQUI a v a -> a, a -> a v a) a v (b v c) -> b v (a v c) (HS *) Th. 11 a v (b v c) -> (a v b) v c Bew: a v (b v c) -> a v (c v b) (EQUI HA3) a v (c v b) -> c v (a v b) (nach Th. 10) a v (b v c) -> c v (a v b) (HS) a v (b v c) -> (a v b) v c (EQUI HA3) Th. 12 (a v b) v c -> a v (b v c) Bew: c v (b v a) -> (c v b) v a (nach Th. 11) (a v b) v c -> a v (b v c) (EQUI HA3, mehrmals) Th. 13 (a -> (b -> c)) -> (b -> (a -> c)) Bew: -a v (-b v c) -> -b v (-a v c) (nach Th. 10) (a -> (b -> c)) -> (b -> (a -> c)) (Def ->) Def & a & b =df -(-a v -b) Th. 14 -(a & b) -> -a v -b Bew: --(-a v -b) -> -a v -b (nach Th. 6) -(a & b) -> -a v -b (Def &) Th. 15 -a v -b -> -(a & b) Bew: -a v -b -> --(-a v -b) (nach Th. 5) -a v -b -> -(a & b) (Def &) Th. 16 -(a v b) -> -a & -b Bew: -(a v b) -> -(a v b) (nach Th. 2) -(a v b) -> -(--a v --b) (EQUI Th. 5, Th. 6, 2-mal) -(a v b) -> -a & -b (Def &) Th. 17 -a & -b -> -(a v b) Bew: -(a v b) -> -(a v b) (nach Th. 2) -(--a v --b) -> -(a v b) (EQUI Th. 5, Th. 6, 2-mal) -a & -b -> -(a v b) (Def &) Th. 18 a & b -> b & a Bew: a & b -> a & b (nach Th. 2) a & b -> -(-a v -b) (Def &) a & b -> -(-b v -a) (EQUI HA3) a & b -> b & a (Def &) Th. 19 a & b -> a Bew: -a -> (-a v -b) (nach HA2) -(-a v -b) -> --a (nach Th. 7) a & b -> --a (Def &) a & b -> a (EQUI Th. 5, Th. 6) Th. 20 a & (b & c) -> (a & b) & c Bew: (a v b) v c -> a v (b v c) (Th. 12) -(a v (b v c)) -> -((a v b) v c) (nach Th. 7) -(a v --(b v c)) -> -(--(a v b) v c) (EQUI Th. 5, Th. 6, 2-mal) -(-a v --(-b v -c)) -> -(--(-a v -b) v -c) (Subst) a & -(-b v -c) -> -(-a v -b) & a (Def &) a & (b & c) -> (a & b) & a (Def &) Th. 21 (a & b) & c -> a & (b & c) Bew: a v (b v c) -> (a v b) v c (Th. 11) -((a v b) v c) -> -(a v (b v c)) (nach Th. 7) -(--(a v b) v c) -> -(a v --(b v c)) (EQUI Th. 5, Th. 6, 2-mal) -(--(-a v -b) v -c) -> -(-a v --(-b v -c)) (Subst) -(-a v -b) & a -> a & -(-b v -c) (Def &) (a & b) & a -> a & (b & c) (Def &) Th. 22 a -> (b -> a & b) Bew: a v -a (Th. 4) (-a v -b) v -(-a v -b) (Subst) -a v (-b v -(-a v -b)) (Th. 12) a -> (b -> -(-a v -b)) (Def ->) a -> (b -> a & b) (Def &)