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