param (PROP prop.ghi () "") # All is identical to equality, but instead of importing as a parameter # predicate_min, predicate, and equality_min those statements are listed here. Basically, # this cuts down the parameters from five to one. kind (nat) tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) term (wff (= A B)) term (wff (A. x ph)) term (wff (E. x ph)) #------------ Axioms ---------------------- ## ## redirect predicate_min.ghi ## # roughly equivalent to ax-17 ## Axiom of Quantifier Introduction ## ## Axiom to quantify a variable over a formula in which it does not occur. ## One of the axioms of predicate calculus. ## ## stmt (alnfi ((ph x)) () (-> ph (A. x ph))) ## Generalization Axiom ## ## Rule of Generalization. One of the axioms of predicate calculus. ## This rule says that if something is unconditionally true, then it is true for all values of a variable. ## Theorem a4i shows we can go the other way. In other words, ## we can add or remove universal quantifiers from the beginning of any theorem as required. ## ## ## [ ph ] ## (A. x [ ph ] ) ##
## stmt (gen () (ph) (A. x ph)) # roughly Margaris A5, but without the subst ## Axiom 4: Specialization ## ## Axiom of Specialization. One of the axioms of predicate calculus. ## A quantified wff implies the wff without a quantifier. In other words if ## something is true for all x, it is true for any specific x. Note that the converse of this axiom does ## not hold in general, but a weaker inference form of the converse holds in the ## Rule of Generalization. A conditional forms of the converse is given by the ## Axiom alnfi. ## ## right('Remove', '∀') ## stmt (ax-4 () () (-> (A. x ph) ph)) # Margaris A4, a.k.a. ax-5 ## Axiom 5: Quantified Implication ## One of the axioms of predicate calculus. ## stmt (ax-alim () () (-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))) ## Axiom 6: Quantified Negation ## One of the axioms of predicate calculus. ## stmt (ax-6 () () (-> (-. (A. x ph)) (A. x (-. (A. x ph))))) ## Axiom 7: Quantifier Commutation ## ## Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. ## It is one of the axioms of predicate calculus. ## ## stmt (ax-7 () () (-> (A. x (A. y ph)) (A. y (A. x ph)))) #------------ Equality Axioms ---------------------- ## ## redirect equality_min.ghi ## ## Equality Reflexive Property ## stmt (eqid () () (= A A)) ## Symmetric Property ## ## (<-> (= A B) (= B A)) ##
## right('Commute', '=') stmt (eqcom () () (<-> (= A B) (= B A))) ## Equality Transitive Property ## right('Simplify', '=') ## ## (-> (/\ (= A B) (= B C)) (= A C)) ##
## stmt (eqtr () () (-> (/\ (= A B) (= B C)) (= A C))) # Similar to ax-9, but expanded to nat's instead of var's. ## There is a number equal to any expression ## ## One of the axioms of predicate calculus with equality. ## One thing this tells us is that at least one number exists. ## ## stmt (tyex ((A x)) () (E. x (= x A))) #------------ Pure Predicate Calculus without Equality ---------------------- ## ## redirect predicate.gh ## ## 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)))) #------------ Equality ---------------------- ## ## redirect equality.gh ## ## Transitive Property ## ## (= A [ [ [ B) ## (= A [ C ] ] ) ## [ (= C ] [B ) ##
stmt (eqtr2 () () (-> (/\ (= A B) (= A C)) (= B C))) term (wff (E! x ph)) stmt (df-eu ((ph y)) () (<-> (E! x ph) (E. y (A. x (<-> ph (= x y)))))) stmt (eubid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> (E! x ps) (E! x ch)))) ## Quantifier variable exchange stmt (eualpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E! x ph) (E! y ps))) stmt (tyeu ((A x)) () (E! x (= x A))) ## A number exists that proves the antecedent ## ## (-> (= x A) [ ph) ## [ ph ##
stmt (vtocle ((A x) (ph x)) ((-> (= x A) ph)) ph) term (wff ([/] A x ph) (x A)) stmt (df-subst ((A z) (ph z)) () (<-> ([/] A x ph) (E. z (/\ (= z A) (E. x (/\ (= x z) ph)))))) term (wff (rwff x ph)) stmt (df-rwff () () (<-> (rwff x ph) (A. x (<-> ph ([/] x x ph))))) ## Symmetric Property ## ## (= A B) ## (= B A) ##
stmt (eqcomi () ((= A B)) (= B A)) ## Symmetric Property ## ## (-> ph (= A B)) ## (-> ph (= B A)) ##
stmt (eqcomd () ((-> ph (= A B))) (-> ph (= B A))) ## Equivalence over Equality stmt(eqeq1 () () (-> (= A B) (<-> (= A C) (= B C)))) ## Equivalence over Equality stmt(eqeq2 () () (-> (= A B) (<-> (= C A) (= C B)))) ## Equivalence over Equality ## ## (= A ] ] [ B ] ) ## (<-> (= A ] C) ] [ (= B ] C)) ##
stmt (eqeq1i () ((= A B)) (<-> (= A C) (= B C))) ## Equivalence over Equality ## ## (= [ A ] [ [ B) ## (<-> (= C [ A) ] [ (= C [ B)) ##
stmt (eqeq2i () ((= A B)) (<-> (= C A) (= C B))) ## Equivalence over Equality ## ## (-> ph (= A ] ] [ B ] )) ## (-> ph (<-> (= A ] C) ] [ (= B ] C))) ##
stmt(eqeq1d () ((-> ph (= A B))) (-> ph (<-> (= A C) (= B C)))) ## Equivalence over Equality ## ## (-> ph (= [ A ] [ [ B)) ## (-> ph (<-> (= C [ A) ] [ (= C [ B))) ##
stmt(eqeq2d () ((-> ph (= A B))) (-> ph (<-> (= C A) (= C B)))) stmt (eqeq12 () () (-> (/\ (= A B) (= C D)) (<-> (= A C) (= B D)))) ## Transitive Property stmt (eqeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (<-> (= A C) (= B D)))) ## Equivalence over Equality stmt (eqeq12i () ((= A B) (= C D)) (<-> (= A C) (= B D))) ## Transitive Property ## ## (= A [ B ] ] ) ## [ (= B ] [ C) ## (= A [ [ [ C) ##
stmt (eqtri () ((= A B) (= B C)) (= A C)) ## Transitive Property ## ## (-> ph (= A [ B ] ] )) ## (-> ph [ (= B ] [ C)) ## (-> ph (= A [ [ [ C)) ##
stmt (eqtrd () ((-> ph (= A B)) (-> ph (= B C))) (-> ph (= A C))) ## Transitive Property ## ## (= A [ B ] ] ) ## (= A [ [ [ C) ## [ (= B ] [ C) ##
stmt (eqtr3 () ((= A B) (= A C)) (= B C)) ## Transitive Property ## ## (= A [ [ B) ## (= [ C [ B ) ## (= A [ C ] ) ##
stmt (eqtr4 () ((= A B) (= C B)) (= A C)) ## Transitive Property ## ## (= A [ [ [ B) ## (= A [ C ] ] ) ## [ (= C ] [ B ) ##
stmt (eqtr5 () ((= A B) (= A C)) (= C B)) ## Syllogism stmt (syl5eq () ((-> ph (= A B)) (= C A)) (-> ph (= C B))) ## Syllogism stmt (syl5eqr () ((-> ph (= A B)) (= A C)) (-> ph (= C B))) ## Syllogism ## ## (-> ph (= A [ B ] ] )) ## [ (= B ] [ C) ## (-> ph (= A [ [ [ C)) ##
stmt (syl6eq () ((-> ph (= A B)) (= B C)) (-> ph (= A C))) ## Syllogism stmt (syl6eqr () ((-> ph (= A B)) (= C B)) (-> ph (= A C))) ## Syllogism stmt (sylan9eq () ((-> ph (= A B)) (-> ps (= B C))) (-> (/\ ph ps) (= A C))) ## Make Implicit Substitution Explicit ## ## A representation of explicit substitution, inferred from an implicit substitution hypothesis. ## stmt (ceqsal ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (<-> (A. x (-> (= x A) ph)) ps)) ## Make Implicit Substitution Explicit ## ## A representation of explicit substitution, inferred from an implicit substitution hypothesis. ## stmt (ceqsex ((ps x) (A x)) ((-> (= x A) (<-> ph ps))) (<-> (E. x (/\ (= x A) ph)) ps)) stmt (vtocl ((A x) (ps x)) ((-> (= x A) (<-> ph ps)) ph) ps) ## Equality over substitution ## ## If A = B, then substituting A into an expression is the same as ## substituting B. ## stmt (dfsbcq () () (-> (= A B) (<-> ([/] A x ph) ([/] B x ph)))) ## Make an implicit substitution explicit stmt (sbcie ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (<-> ([/] A x ph) ps)) ## Convert Arbitrary Substitution into Universal Quantifier stmt (cla4g ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (-> (A. x ph) ps)) ## Quantifier variable exchange stmt (exalpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E. x ph) (E. y ps))) ## Quantifier variable exchange stmt (exalpha1 ((ph y) (ps x)) ((-> (= x y) (-> ph ps))) (-> (E. x ph) (E. y ps))) ## Relatively Well-Formed Formula Infernece stmt (rwffi ((ps x) (ph y)) ((-> (= x y) (<-> ph ps))) (rwff x ph)) ## Symmetric Property stmt (eqcoms () ((-> (= A B) ph)) (-> (= B A) ph)) ## Add Substitutions to both sides stmt (sbcbid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> ([/] A x ps) ([/] A x ch)))) ## Existence when number is used in substitution stmt (sbcex ((A x) (ph x)) () (-> ([/] A y ph) (E. x ([/] x y ph)))) ## Substitute any number into a universal statement stmt (a4sbc () () (-> (A. x ph) ([/] A x ph))) ## Negation Preserves Relatively Well-Formed-ness stmt (not-rwff () ((rwff x ph)) (rwff x (-. ph))) ## Transitive Property stmt (3eqtr4g () ((-> ph (= A B)) (= C A) (= D B)) (-> ph (= C D))) stmt (alpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (A. x ph) (A. y ps))) stmt (substex ((ph x y) (ps y) (ch x) (A y)) ((-> (/\ ph (/\ (= y A) ps)) ch)) (-> (/\ ph (E. x ps)) (E. y ch))) stmt (eu4 ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E! x ph) (/\ (E. x ph) (A. x (A. y (-> (/\ ph ps) (= x y))))))) ## Unique Existence Implies Existence ## right('Infer', '∃') stmt (euex () () (-> (E! x ph) (E. x ph))) ## Substitution as Existence ## right('Equivalence', '∃') left('Equivalence', '[/]') stmt (sbc5 ((A x)) () (<-> ([/] A x ph) (E. x (/\ (= x A) ph)))) ## Commutativity of existential quantifiers ## right('Commute', '∃') stmt (excom () () (<-> (E. x (E. y ph)) (E. y (E. x ph)))) term (wff (E* x ph)) stmt (mo4 ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E* x ph) (A. x (A. y (-> (/\ ph ps) (= x y)))))) stmt (eu5 () ((rwff x ph)) (<-> (E! x ph) (/\ (E. x ph) (E* x ph))))