View file src/slc/prop.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