param (PROP ../prop.ghi () "") kind (nat) tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) term (wff (A. x ph)) # 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))))