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)))
**