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