`+`

(addition) or `∪`

(union). Because `term`

is a ghilbert keyword, we use the word ''object'' to refer to a term.
kind (object)
var (object x y z x0 x1 y0 y1)
tvar (object s t u s0 s1 t0 t1)
#
# == Quantification ==
# We extend the available formulas with [[w:Universal quantification|universal quantification]]:
term (formula (∀ x φ))
stmt (QuantifiedImplication () () ( → (∀ x (→ φ ψ)) (→ (∀ x φ) (∀ x ψ)) ) )
stmt (QuantifiedNegation () () ( → (¬ (∀ x φ)) (∀ x (¬ (∀ x φ))) ) )
stmt (QuantifierCommutation () () ( → (∀ x (∀ y φ)) (∀ y (∀ x φ)) ) )
#
# [[w:Generalization (logic)|Generalization]]:
stmt (Generalization ((φ x)) () (→ φ (∀ x φ)))
stmt (generalize () (φ) (∀ x φ))
#
# Although a usable theory of predicate logic will generally have at least one more quantifier (∃ for "there exists"), it can be defined in terms of ∀, so we have avoided it in the above axioms and do not need to define it here.
#
# == Equality ==
# In this set of axioms we are concerned with equality between two variables, rather than two terms. [[Interface:Axiom of quantifiability]] takes up equality of terms in one way, and [[Interface:Equality of classes]] has a different approach.[http://us.metamath.org/mpeuni/df-cleq.html df-cleq], metamath's set.mm, accessed April 16, 2012 However, as a matter of syntax we do say that equality is between two terms, so that those interfaces can adopt an axiom concerning equality between terms without having to use two different equality symbols, one for variables and one for terms.
#
term (formula (= s t))
#
# === Building equalities ===
# We need some axioms defining equality. Because it seems like the path of least resistance, we adopt reflexivity, symmetry, and transitivity for terms. Other approaches would just assume these for variables, or a smaller set of axioms which imply these.[http://us.metamath.org/mpeuni/ax-8.html ax-8], metamath's set.mm, accessed April 16, 2012
stmt (EqualityReflexivity () () (= s s))
stmt (EqualitySymmetry () () (↔ (= s t) (= t s)))
stmt (EqualityTransitivity () () (→ (∧ (= s t) (= t u)) (= s u)))
#
# === Axioms combining equality and quantification ===
#
# The `Existence`

axiom asserts that there is at least one object:
stmt (Existence () () (¬ (∀ x (¬ (= x y)))) )
stmt (QuantifierSubstitution () () (→ (∀ x (= x y)) (∀ y (= y x))) )
#
# The `VariableSubstitution`

axiom converts a statement about one variable to a statement about another. In most uses, `φ`

will contain `x`

as a free variable. Then the axiom allows one to deduce `∀ x (x = y → φ)`

, a statement where `x`

is not free, but where `y`

is free. `∀ x (x = y → φ)`

means (in some sense), `φ`

with `y`

substituted for `x`

. Metamath contains several equivalent variations of this axiom;[http://us.metamath.org/mpeuni/ax11v.html ax11v], [http://us.metamath.org/mpeuni/ax-11.html ax-11], and [http://us.metamath.org/mpeuni/ax-11o.html ax-11o] in metamath's set.mm, accessed March 14, 2010 we pick ax11v, which is the most convenient one for us.
stmt (VariableSubstitution () ()
(→ (= x y) (→ φ (∀ x (→ (= x y) φ)))) )
#
# There is also the principle of "equals can be substituted for equals". In our system, there is no way to express this generally, and it must be provided separately for each kind of predicate or operation which exists in the theory (for example, `∈`

(is an element of), for set theory, or `S`

(successor) or `+`

(addition) for Peano arithmetic). Such a statement for equals itself, `(s0 = s1 ∧ t0 = t1) → (s0 = t0 ↔ s1 = t1)`

, can be proved from the above axioms, so an additional axiom is not needed here.
#
# == Axiom of quantifiability ==
# In the axioms as shown above, we do not preclude the possibility of a term which cannot be equal to any variable (this will be true of [[w:proper class|proper classes]] in some formulations of set theory, for example). If this generality is not needed, assuming the [[Interface:Axiom of quantifiability]] may make life easier.
#
# == References ==
#