## redirect predicate.gh param (PROP prop.ghi () "") param (PREDICATE_MIN predicate_min.ghi (PROP) "") tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) # Definition of exists - could be done through def instead of axiom here. term (wff (E. x ph)) ## Definition of ∃ ## right('Equivalence', '∀') stmt (df-ex () () (<-> (E. x ph) (-. (A. x (-. ph))))) stmt (a4i () ((A. x ph)) ph) stmt (mpg () ((-> (A. x ph) ps) ph) ps ) stmt (19.3 ((ph x)) () (<-> (A. x ph) ph) ) # aka 19.7 stmt (alnex () () (<-> (A. x (-. ph)) (-. (E. x ph))) ) stmt (19.8a () () (-> ph (E. x ph)) ) stmt (19.8ai () (ph) (E. x ph)) stmt (19.2 () () (-> (A. x ph) (E. x ph)) ) ## Quantified Non-free Variable ## right('Simplify', '∃') stmt (19.9 ((ph x)) () (<-> (E. x ph) ph) ) stmt (19.9d ((ps x)) ((-> ph (E. x ps))) (-> ph ps)) stmt (19.15 () () (-> (A. x (<-> ph ps)) (<-> (A. x ph) (A. x ps)))) stmt (19.15i () ((A. x (<-> ph ps))) (<-> (A. x ph) (A. x ps)) ) stmt (19.15d () ((-> ph (A. x (<-> ps ch)))) (-> ph (<-> (A. x ps) (A. x ch))) ) ## Equivalence over Quantification ## ## (<-> [ ph ] [ ps ] ) ## (<-> (A. x [ ph ] ) (A. x [ ps ] )) ##
stmt (albii () ((<-> ph ps)) (<-> (A. x ph) (A. x ps)) ) ## Equivalence over Quantification ## ## (A. x [ ph ] ) ## (<-> [ ph ] [ ps ] ) ## (A. x [ [ [ ps ] ) ##
stmt (albiii () ((A. x ph) (<-> ph ps)) (A. x ps) ) ## Equivalence over Quantification ## ## (<-> [ ph ] [ ps ] ) ## (<-> (E. x [ ph ] ) (E. x [ ps ] )) ##
stmt (exbii () ((<-> ph ps)) (<-> (E. x ph) (E. x ps)) ) ## Equivalence over Quantification ## ## (E. x [ ph ] ) ## (<-> [ ph ] [ ps ] ) ## (E. x [ [ [ ps ] ) ##
stmt (exbiii () ((E. x ph) (<-> ph ps)) (E. x ps) ) # aka 19.6 ## Definition of ∃ ## right('Equivalence', '∃') stmt (alex () () (<-> (A. x ph) (-. (E. x (-. ph)))) ) stmt (19.20i () ((-> ph ps)) (-> (A. x ph) (A. x ps)) ) ## Quantifier Moved Around Non-free Variable ## right('Equivalence', '→∀') left('Equivalence', '∀→') stmt (19.21 ((ph x)) () (<-> (A. x (-> ph ps)) (-> ph (A. x ps))) ) stmt (19.21ai ((ph x)) ((-> ph ps)) (-> ph (A. x ps)) ) stmt (19.5 () () (<-> (A. x (A. y ph)) (A. y (A. x ph))) ) stmt (19.22 () () (-> (A. x (-> ph ps)) (-> (E. x ph) (E. x ps))) ) stmt (19.22i () ((-> ph ps)) (-> (E. x ph) (E. x ps)) ) stmt (19.22d ((ph x)) ((-> ph (-> ps ch))) (-> ph (-> (E. x ps) (E. x ch))) ) stmt (19.18 () () (-> (A. x (<-> ph ps)) (<-> (E. x ph) (E. x ps))) ) ## Change Quantifiers ## right('Equivalence', '→∃') left('Equivalence', '∀→') stmt (19.23 ((ps x)) () (<-> (A. x (-> ph ps)) (-> (E. x ph) ps))) stmt (exbid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> (E. x ps) (E. x ch))) ) ## Combine Existence Quantifiers ## right('Infer', '∃∃') stmt (doubleex ((ph y) (ps x)) () (-> (/\ (E. x ph) (E. y ps)) (E. x (E. y (/\ ph ps))))) ## Move Existential Quantifier stmt (eximp1 () () (-> (E. x (-> ph ps)) (-> (A. x ph) (E. x ps)))) ## Add existence quantifier ## ## (-> [ ph ] ps) ## (-> (E. x [ ph) ] ps) ##
stmt (19.23ai ((ps x)) ((-> ph ps)) (-> (E. x ph) ps)) ## Distributive Property ## right('Distribute', 'R') left('Distribute', '-R') stmt (19.26 () () (<-> (A. x (/\ ph ps)) (/\ (A. x ph) (A. x ps)))) ## Quantifiers Moved Around Non-free Variable ## right('Equivalence', '∧∃') left('Equivalence', '∃∧') stmt (19.41l ((ph x)) () (<-> (E. x (/\ ph ps)) (/\ ph (E. x ps)))) ## Quantifiers Moved Around Non-free Variable ## right('Equivalence', '∧∃') left('Equivalence', '∃∧') stmt (19.41r ((ph x)) () (<-> (E. x (/\ ph ps)) (/\ ph (E. x ps)))) # Move to prop stmt (albi2d ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> (A. x ps) (A. x ch)))) ## Quantifiers Moved Around Non-free Variable ## right('Equivalence', '→∃') left('Equivalence', '∃→') stmt (19.41 ((ps x)) () (<-> (E. x (/\ ph ps)) (/\ (E. x ph) ps))) ## Quantifiers Moved Around Non-free Variable ## right('Equivalence', '∧∀') left('Equivalence', '∀∧') stmt (alan1 ((ph x)) () (<-> (A. x (/\ ph ps)) (/\ ph (A. x ps)))) ## Combine universal and Existence Quantifiers ## right('Simplify', '∃') stmt (19.29 () () (-> (/\ (A. x ph) (E. x ps)) (E. x (/\ ph ps)))) stmt (mpexaxp () () (-> (E. x ph) (-> (A. x (-> ph ps)) (E. x (/\ ph ps))))) ## Remove Existential Quantifier stmt (exax1d () ((-> ph (E. x (A. x ps)))) (-> ph (A. x ps))) stmt (mpexax () () (-> (E. x ph) (-> (A. x (-> ph ps)) (E. x ps)))) ## Quantifiers Moved Around Non-free Variable stmt (aaan ((ph y) (ps x)) () (<-> (A. x (A. y (/\ ph ps))) (/\ (A. x ph) (A. y ps)))) stmt (albiim () () (<-> (A. x (<-> ph ps)) (/\ (A. x (-> ph ps)) (A. x (-> ps ph))))) ## Combine universal and Existence Quantifiers ## right('Simplify', '∃') stmt (19.29r () () (-> (/\ (E. x ph) (A. x ps)) (E. x (/\ ph ps)))) stmt (ex-nf ((ph x)) () (-> (E. x ph) ph)) ## Quantifier Moved Around Non-free Variable ## right('Equivalence', '→∃') left('Equivalence', '∃→') stmt (imex ((ph x)) () (<-> (-> ph (E. x ps)) (E. x (-> ph ps)))) ## Quantifiers Moved Around Non-free Variable stmt (exor2 ((ps x)) () (<-> (E. x (\/ ph ps)) (\/ (E. x ph) ps))) stmt (exani ((ps x)) ((-> ph ps)) (-> (E. x ph) ps)) ## Quantifiers Moved Around Non-free Variable stmt (alan2 ((ps x)) () (<-> (A. x (/\ ph ps)) (/\ (A. x ph) ps))) ## Distributive Property stmt (alan12 () () (-> (/\ (A. x ph) (A. x ps)) (A. x (/\ ph ps)))) ## Commutativity of existential quantifiers ## right('Commute', '∃') stmt (excom () () (<-> (E. x (E. y ph)) (E. y (E. x ph))))