%%% ====================================================================
%%% This file is part of the open source project *Hilbert II*, which 
%%% wants to present mathematical knowledge in a standardized and 
%%% formal correct form.
%%% See "http://www.qedeq.org" for more information about this project.
%%% 
%%% Permission is granted to copy, distribute and/or modify this 
%%% document under the terms of the GNU Free Documentation License, 
%%% Version 1.2 or any later version published by the 
%%% Free Software Foundation; with no Invariant Sections, 
%%% no Front-Cover Texts, and no Back-Cover Texts.
%%% See under "http://www.gnu.org/licenses/fdl.html".
%%% ====================================================================

Subject:   Deduction of propositional logic due to
           Hilbert and Ackermann [1928]
Date:      2004-08-31
Version:   $Revision: 1.1 $
Authors:   Michael Meyling, Franz Fritsche

The following logical operator symbols are used in formulas:
  "-"      negation    (prefix notation with exact one argument)
  "&"      conjunction (infix notation with exact two arguments)
  "v"      disjunction (infix notation with exact two arguments)
  "->"     implication (infix notation with exact two arguments)

"a", "b", "c" are proposition variables

Table of operator priority, sorted from highest to lowest:
  - 
  &
  v
  ->


Definition ->
  a -> b =df -a v b


Axiom HA1
  a v a -> a
  
  
Axiom HA2
  a -> a v b
  
  
Axiom HA3
  a v b -> b v a
  
  
Axiom HA4
  (a -> b) -> (c v a -> c v b)


Rule modus ponens
  a, a -> b
  ---------
     b


Rasis rule substititution
  A(a)
  ----
  A(B)

       
Theorem 1 (Form for Hypothetic Syllogism)
  (a -> b) -> ((c -> a) -> (c -> b))     

Proof:
  (a -> b) -> (-c v a -> -c v b)      (due to HA4)
  (a -> b) -> ((c -> a) -> (c -> b))  (definition ->)
  
  
Rule HS	// Hypothetic Syllogism
  a -> b, b -> c
  --------------
      a -> c
       
Proof:
  a -> b                             (precondition)
  b -> c                             (precondition)
  (a -> b) -> ((c -> a) -> (c -> b)) (1)
  (b -> c) -> ((a -> b) -> (a -> c)) (substitution)
  (a -> b) -> (a -> c)               (modus ponens)
  a -> c                             (modus ponens)
  

Theorem 2
  a -> a
  
Proof:
  a -> a v a                         (due to HA2)
  a v a -> a                         (HA1)
  a -> a                             (HS)
  
  
Theorem 3
  -a v a

Proof:
  a -> a                             (2)
  -a v a                             (definition ->)


Theorem 4
  a v -a
  
Proof:
  -a v a                             (3)
  a v -a                             (due to HA3)


Theorem 5
  a -> --a
  
Proof:
  a v -a                             (4)
  -a v --a                           (substitution)
  a -> --a                           (definition ->)


Theorem 6
  --a -> a
  
Proof:
  -a -> ---a                         (due to 5)
  a v -a -> a v ---a                 (due to HA4)
  a v -a                             (4)
  a v ---a                           (modus ponens)
  ---a v a                           (due to HA3)
  --a -> a                           (definition ->)


Theorem 7
  (a -> b) -> (-b -> -a)
  
Proof:
  b -> --b                           (5)
  -a v b -> -a v --b                 (due to HA4)
  -a v --b -> --b v -a               (due to HA3)
  -a v b -> --b v -a                 (HS)
  (a -> b) -> (-b -> -a)             (definition ->)


Rule ORK
       a -> b
  ----------------
   a v c -> b v c

Proof:
  a -> b                             (precondition)
  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)


Rule EQUI
     a -> b
     b -> a
  ------------
  A(a) -> A(b)
  A(b) -> A(a)

Proof:
  a -> b                             (precondition)
  (a -> b) -> (-b -> -a)             (7)
  -b -> -a                           (modus ponens)
  (a -> b) -> (c v a -> c v b)       (HA4)
  c v a -> c v b                     (modus ponens)
  a v c -> b v c                     (ORK)
  analogue for b -> a
  proof by structural induction from A(a) -> A(b) (using definiton of ->)


Theorem 8
  (a -> b) -> (a v c -> b v c)

Proof (a):
  (a -> b) -> (c v a -> c v b)       (HA4)
  (a -> b) -> (a v c -> b v c)       (EQUI HA3, 2-times)

Proof (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))  (due to HA4)
  (c v a -> c v b) -> (c v a -> b v c)          (definition ->)
* (a -> b) -> (c v a -> b v c)                  (HS)
  a v c -> c v a                                (HA3)
  -(c v a) -> -(a v c)                          (due to 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))  (due to 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))  (due to 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)          (definition ->)
  (a -> b) -> (a v c -> b v c)                  (HS *)


Theorem 9
  a -> b v a
  
Proof:
  a -> a v b                         (HA2)
  a v b -> b v a                     (HA3)
  a -> b v a                         (HS)


Theorem 10
  a v (b v c) -> b v (a v c)
  
Proof:
  c -> a v c                            (due to 9)
  b v c -> b v (a v c)                  (due to HA4)
  a v (b v c) -> a v (b v (a v c))      (due to HA4)
* a v (b v c) -> (b v (a v c)) v a      (EQUI HA3)
  a -> b v a                            (9)
  a v c -> b v (a v c)                  (substitution)
  a -> a v c                            (due to 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))  (due to 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 *)


Theorem 11
  a v (b v c) -> (a v b) v c
  
Proof:
  a v (b v c) -> a v (c v b)         (EQUI HA3)
  a v (c v b) -> c v (a v b)         (due to 10)
  a v (b v c) -> c v (a v b)         (HS)
  a v (b v c) -> (a v b) v c         (EQUI HA3)


Theorem 12
  (a v b) v c -> a v (b v c)     

Proof:
  c v (b v a) -> (c v b) v a         (due to 11)
  (a v b) v c -> a v (b v c)         (EQUI HA3, several times)


Theorem 13
  (a -> (b -> c)) -> (b -> (a -> c))

Proof:
  -a v (-b v c) -> -b v (-a v c)     (due to 10)
  (a -> (b -> c)) -> (b -> (a -> c)) (definition ->)

Definition &
  a & b =df -(-a v -b)

Theorem 14
  -(a & b) -> -a v -b

Proof:
  --(-a v -b) -> -a v -b             (due to 6)
  -(a & b) -> -a v -b                (definition &)


Theorem 15
  -a v -b -> -(a & b)

Proof:
  -a v -b -> --(-a v -b)             (due to 5)
  -a v -b -> -(a & b)                (definition &)


Theorem 16
  -(a v b) -> -a & -b

Proof:
  -(a v b) -> -(a v b)               (due to 2)
  -(a v b) -> -(--a v --b)           (EQUI 5, 6, 2-times)
  -(a v b) -> -a & -b                (definition &)


Theorem 17
  -a & -b -> -(a v b)

Proof:
  -(a v b) -> -(a v b)               (due to 2)
  -(--a v --b) -> -(a v b)           (EQUI 5, 6, 2-times)
  -a & -b -> -(a v b)                (definition &)
 

Theorem 18
  a & b -> b & a

Proof:
  a & b -> a & b                     (due to 2)
  a & b -> -(-a v -b)                (definition &)
  a & b -> -(-b v -a)                (EQUI HA3)
  a & b -> b & a                     (definition &)


Theorem 19
  a & b -> a
  
Proof:
  -a -> (-a v -b)                    (due to HA2)
  -(-a v -b) -> --a                  (due to 7)
  a & b -> --a                       (definition &)
  a & b -> a                         (EQUI 5, 6)
  
  
Theorem 20
  a & (b & c) -> (a & b) & c

Proof:
  (a v b) v c -> a v (b v c)                 (12)
  -(a v (b v c)) -> -((a v b) v c)           (due to 7)
  -(a v --(b v c)) -> -(--(a v b) v c)       (EQUI 5, 6, 2-times)
  -(-a v --(-b v -c)) -> -(--(-a v -b) v -c) (substitution)
  a & -(-b v -c) -> -(-a v -b) & a           (definition &)
  a & (b & c) -> (a & b) & a                 (definition &)


Theorem 21
  (a & b) & c -> a & (b & c) 

Proof:
  a v (b v c) -> (a v b) v c                 (11)
  -((a v b) v c) -> -(a v (b v c))           (due to 7)
  -(--(a v b) v c) -> -(a v --(b v c))       (EQUI 5, 6, 2-times)
  -(--(-a v -b) v -c) -> -(-a v --(-b v -c)) (substitution)
  -(-a v -b) & a -> a & -(-b v -c)           (definition &)
  (a & b) & a -> a & (b & c)                 (definition &)


Theorem 22
  a -> (b -> a & b)

Proof:
  a v -a                             (4)
  (-a v -b) v -(-a v -b)             (substitution)
  -a v (-b v -(-a v -b))             (12)
  a -> (b -> -(-a v -b))             (definition ->)
  a -> (b -> a & b)                  (definition &)