logic tutorial

/\ = ∧
\/ = ∨
=> = ⇒ (also → and ⊃)
True = ⊤
False = ⊥
!- = ⊢

/\I:      X [G], Y [G] !- X /\ Y [G]

/\E1:     X /\ Y [G] !- X [G]

/\E2:     X /\ Y [G] !- Y [G]

=>I:      Y [X, G] !- X => Y [G]

=>E:      X => Y [G], X [G] !- Y [G]

\/I1:     X [G] !- X \/ Y [G]

\/I2:     Y [G] !- X \/ Y [G]

\/E:      X \/ Y [G], Z [X, G], Z [Y, G] !- Z [G]

TrueI:    !- True [G]

FalseE:   False [G] !- Z [G]

hyp:      !- X [X, G]



Proof of   A /\ B  [ A /\ (B /\ C) ]

  1.    A /\ (B /\ C)    [ A /\ (B /\ C) ]    (by hyp)
  2.    A                [ A /\ (B /\ C) ]    (by /\E1 on 1)
  3.    B /\ C           [ A /\ (B /\ C) ]    (by /\E2 on 1)
  4.    B                [ A /\ (B /\ C) ]    (by /\E1 on 3)
  5.    A /\ B           [ A /\ (B /\ C) ]    (by /\I on 2 and 4)



Proof of   B /\ A  [ A /\ B ]

  1.    A /\ B    [ A /\ B ]    (by hyp)
  2.    A         [ A /\ B ]    (by /\E1 on 1)
  3.    B         [ A /\ B ]    (by /\E2 on 1)
  4.    B /\ A    [ A /\ B ]    (by /\I on 3 and 2)



Proof of   A => ((A => B) => B)  []

  1.    A                       [ A, A => B ]    (by hyp)
  2.    A => B                  [ A, A => B ]    (by hyp)
  3.    B                       [ A, A => B ]    (by =>E on 2 and 1)
  4.    (A => B) => B           [ A ]            (by =>I on 3)
  5.    A => ((A => B) => B)    []               (by =>I on 4)