View file src/slc/prop-new.prf - Download

# Proof of p => p

# Axioms
! MP ^p ^q ((imp p q) (p q) = [*])
! AK ^p ^q (imp p (imp q p) = [*])
! AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*])
! EFQ ^p (imp false p = [*])
! RAA ^p (imp (imp (imp p false) false) p = [*])
! GEN ^p (p (all ^x p) = [*])
! PART ^p ^t (imp (all p) (p t) = [*])
! PERMUT ^p ^q (imp (all ^x  : imp p (q x)) (imp p (all q)) = [*])
! SOME ^p (imp (imp (all p) false) 
                   (imp (p (some ^x (imp (p x) false))) false)
               = [*])

# Proof

! lemma1 (AS p (imp p p) p)

! lemma2 (AK p (imp p p))

! lemma3 (MP (imp p (imp (imp p p) p))
               (imp (imp p (imp p p)) (imp p p)))

! lemma4 ( lemma1 ( (imp p (imp (imp p p) p))
                      (imp (imp p (imp p p)) (imp p p)) ) )

! lemma5 ( lemma4 ; lemma3 )

! lemma6 ( lemma2 
              (imp 
               (imp p (imp p p))
               (imp p p) ) )

! lemma7 ( lemma6 ; lemma5 )

! lemma8 (AK p p)

! lemma9 
 (MP 
    (imp p (imp p p))
    (imp p p) )

! lemma10 (lemma7 ((imp p (imp p p)) (imp p p)))

! lemma11 ( lemma10 ; lemma9 )

! lemma12 (lemma8 (imp p p))

! theorem1 ( imp p p ; lemma12 ; lemma11 )

theorem1