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)) term (wff (= A B)) # 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)))) # Similar to ax-8, but for nat's instead of var's. ## Equality Transitive Axiom ## right('Simplify', '=') ## ## (-> (/\ (= A B) (= A C)) (= B C)) ##
## stmt (ax-eqtr () () (-> (/\ (= A B) (= A C)) (= B C))) # Similar to ax-9, but expanded to nat's instead of var's. ## Axiom of Existence ## ## One of the axioms of predicate calculus with equality. ## One thing this tells us is that at least one number exists. ## ## stmt (ax-tyex ((A x)) () (-. (A. x (-. (= x A))))) #stmt (ax-11 () () (-> (= x y) (-> (A. y ph) (A. x (-> (= x y) ph))))) # Properties of numbers: Peano axioms term (nat (0)) term (nat (S A)) term (nat (+ A B)) term (nat (* A B)) # Equality axiom for addition ## Addition of Equal Numbers Axiom ## ## When two equal numbers are added, their sums are equal. ## ## stmt (addeq12 () () (-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))) ## Multiplication of Equal Numbers Axiom ## ## When two equal numbers are added, their products are equal. ## ## stmt (muleq12 () () (-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))) ## Peano Axiom 1: 0 is the first natural number ## ## One of the Peano axioms ## for arithmetic. 0 is the first natural number. It has no predecessor. ## It is not a successor to anything. ## stmt (pa_ax1 () () (-. (= (0) (S A)))) ## Peano Axiom 2: Succession Equality ## ## Two natural numbers are equal iff their successors are equal. ## One of the Peano axioms ## for arithmetic. Note that the biconditional captures equality properties of ## successor just as well as the traditional Peano axiom 2. ## ## ## (<-> (= A B) (= (S A) (S B))) ##
## stmt (pa_ax2 () () (<-> (= A B) (= (S A) (S B)))) ## Peano Axiom 3: Additive Identity Axiom ## ## One of the Peano axioms ## for arithmetic. ## ## auto-right('Simplify', '0') ## stmt (pa_ax3 () () (= (+ A (0)) A)) ## Peano Axiom 4: Addition ## ## One of the Peano axioms ## for arithmetic. ## ## left('Equivalence', 'R') ## stmt (pa_ax4 () () (= (+ A (S B)) (S (+ A B)))) ## Peano Axiom 5: Multiply by 0 ## ## One of the Peano axioms ## for arithmetic. ## ## right('Simplify','0') ## stmt (pa_ax5 () () (= (* A (0)) (0))) ## Peano Axiom 6: Multiplication ## ## One of the Peano axioms ## for arithmetic. ## ## right('Distribute','+') ## stmt (pa_ax6 () () (= (* A (S B)) (+ (* A B) A))) ## Peano Induction Axiom ## ## One of the Peano axioms. ## The more traditional statement of mathematical induction is derived ## from this axiom in the finds ## and induction ## theorems. ## ## stmt (pa_ind ((ph y)) () (-> (/\ (A. x (-> (= x (0)) ph)) (A. y (-> (A. x (-> (= x y) ph)) (A. x (-> (= x (S y)) ph))))) (A. x ph)))