1.9. Quantifiers
A quantifier is a binder taking a unary predicate (formula) and giving a
Boolean value.
In set theory, the full syntax for a quantifier Q binding a
variable x with range E on a unary predicate A,
is
Qx∈E, A(x)
where A(x) abbreviates the formula defining A,
whose free variables are x and possible parameters.
A shorter notation puts the range as an index (Q_{E}x,
A(x)), or deletes it altogether (Qx, A(x))
when it may be kept implicit (unimportant, or fixed by the context, such
as a type in a generic theory).
The two main quantifiers (from which others will be defined later) are:
 The universal quantifier ∀, read as «For all x (in...),... »).

The existential quantifier ∃, read as «There exists x (in...) such that... »
The universal quantifier of set theory can be seen as defined from the set builder:
(∀x∈E, A(x)) ⇔ {x∈E
 A(x)} = E.
The one of firstorder logic can be defined in set theoretical interpretations,
seeing A as a function and its Boolean values as objects:
(∀x, A(x)) ⇔ A = (x ↦ 1)
Anyway (∀x, 1) is always true.
∃ can be defined from ∀ with the same range :
(∃x, A(x))
⇎ (∀x, ¬A(x)).
Thus (∃x, A(x)) ⇔
A ≠ (x ↦ 0).
With classes,
(∃_{C } x, A(x)) 
⇔ (∃x, C(x) ∧ A(x))
⇔ ∃_{C∧A} x, 1 
(∀_{C } x, A(x)) 
⇔ (∀x, C(x) ⇒ A(x)) 
∀x, C(x)

⇔ ∃_{C } y, x=y

Inclusion between classes
A class A is said to be included in a class
B when ∀x, A(x) ⇒ B(x). Then
A is a
subclass of B, as ∀x, A(x) ⇔ (B(x)
∧ A(x)). Conversely, any subclass of B is
included in B.
The inclusion of A in B
implies for any predicate C (in cases of definiteness):
(∀_{B}
x, C(x)) ⇒ (∀_{A} x,
C(x))
(∃_{A} x, C(x)) ⇒ (∃_{B}
x, C(x))
(∃_{C }x, A(x)) ⇒ (∃_{C
}x, B(x))
(∀_{C }x, A(x)) ⇒ (∀_{C
}x, B(x))
Rules of proofs for quantifiers on a unary predicate
Existential Introduction. If we have terms t,
t′,… and a proof of (A(t) ∨ A(t′)
∨ …), then ∃x, A(x).
Existential Elimination. If ∃x, A(x),
then we can introduce a new free variable z with the
hypothesis A(z) (the consequences will be
true without restricting the generality).
These rules express the meaning of ∃ : going from some term to ∃ then from
∃ to z, amounts to letting z represent that term
(without knowing which, but they can be gathered into one by the conditional operator). They give
the same meaning to ∃_{C } as to its 2 above
equivalent formulas, bypassing (making implicit) the extended
definiteness rule for (C ∧ A) by focusing on the
case when C(x) is true and thus A(x)
is definite.
While ∃ appeared as the designation of an object, ∀ appears as a
deduction rule: ∀_{C }x, A(x)
means that its negation ∃_{C }x, ¬A(x)
leads to a contradiction.
Universal Introduction. If from the mere hypothesis C(x)
on a new free variable x we could deduce A(x),
then ∀_{C }x, A(x).
Universal Elimination. If ∀_{C }x,
A(x) and t is a term satisfying C(t),
then A(t).
Introducing then eliminating ∀ is like replacing x by t
in the initial proof.
These rules can be used to justify the following logically valid formulas
((∀_{C }x, A(x))
∧ (∀_{C }x, A(x) ⇒ B(x)))
⇒ (∀_{C }x, B(x))
((∃_{C }x, A(x))
∧ (∀_{C }x, A(x) ⇒ B(x)))
⇒ (∃_{C }x, B(x))
((∀_{C }x, A(x))
∧ (∃_{C }x, B(x))) ⇒
(∃_{C }x, A(x) ∧
B(x))
(∀_{C }x,
A(x)∨B(x)) ⇒ ((∀_{C }x,
A(x)) ∨ (∃_{C }x,
B(x)))
(∃_{A} x, ∀_{B}
y, R(x,y)) ⇒ (∀_{B} y,
∃_{A} x, R(x,y))
∀x, (∀y, R(x,y)) ⇒
R(x,x) ⇒ (∃y, R(x,y))
The formula (∃_{C }x, A(x)) ∧
(∀_{C }x, A(x) ⇒ B(x))
will be abbreviated as (∃_{C }x, A(x) ∴
B(x)) while it implies but is not generally equivalent to
(∃_{C }x, A(x) ∧ B(x)).
Secondorder quantification
Let us call secondorder quantifier, a quantifier binding a variable structure symbol
over the range of all structures of its symbol
type, may this be conceived as the
range of all definable ones (with all possible defining expressions whose free variables may have
any list of parameters beyond the given arguments) or as the full set theoretical
range, that is the range of all such structures which exist in the universe, relating the given interpreted types.
The use of such a quantifier (and thus of variable structure symbols) is not allowed in firstorder logic,
but belongs to some other logical frameworks instead, such as secondorder logic (part 5).
Still while keeping firstorder logic as the main framework of a given theory,
some secondorder quantifiers may be used to describe some of its
meta level aspects in the following ways (which will be
involved in the formalization of set theory in 1.10 and 1.11). Let T be
a firstorder theory, T' its extension by a structure symbol s
(without further axiom) and F a ground formula of T' (in firstorder logic)
also denoted F(s) when seen as a formula of T using the
variable structure symbol s in secondorder logic.
Secondorder Universal Introduction. If T'⊢F then T
entails the secondorder statement (∀s, F(s)).
This holds for any model and the full set theoretical range of s, independently of
the universe in which models and structures s are searched for.
Secondorder Universal Elimination. Once a secondorder statement
(∀s, F(s)) is accepted in a theory T,
it is manifested in firstorder logic as a schema of statements,
that is an infinite list of statements of the form (∀parameters, F(s)) for each
possible replacement of s by a defining expression with parameters.
Applying secondorder universal elimination after secondorder universal introduction,
means deducing from T a schema of theorems, each one indeed deducible
in firstorder logic by the proof obtained from the original proof by replacing s by its definition.
In secondorder logic, a new binder B can be defined by an expression here abbreviated
as F(A) using a symbol A of variable unary structure whose argument will be
bound by B:
∀A, (Bx, A(x)) = F(A)
By secondorder universal elimination, this comes down to a schema of definitions in firstorder logic :
for each expression defining A, it defines (Bx, A(x)) like a structure symbol,
by the expression F(A) whose available free variables are the parameters
of F plus those of A.
Axioms of equality
In firstorder logic with given types and a given language, some ground formulas involving
= are logically valid for the range of interpretations keeping = as the = predicate
of set theory, but no more for the larger range of interpretations letting
it become any other predicate. A possible list of axioms of equality, is a list of
some of such formulas which suffice to imply all others in this context. One such list
consists in the following 2 axioms per type, where the latter is meant as an axiom schema
by secondorder universal elimination of the variable unary predicate A:
 ∀x, x = x (reflexivity)

∀A,∀x,∀y, (x = y ∧ A(y)) ⇒ A(x).
Variables x and y can also serve among parameters in definitions of A.
This can be understood by reordering quantifiers as (∀x,
∀y, ∀A), or as deduced from cases only using other free variables a, b, by
adapting an above logically valid formula as ∀a, ∀b,
(∀x, ∀y, R(a, b, x,y)) ⇒ R(a, b, a,b).
Diverse definitions of A give diverse formulas (assuming reflexivity):
Formula
3. ∀x,∀y, x = y ⇒ y = x
4. ∀x, ∀y, ∀z, (x = y ∧ y = z) ⇒
x = z
5. ∀f, ∀x, ∀y, x = y ⇒ f(x) = f(y)
6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x, ∀y, ∀z, (x = y ∧ z = y) ⇒
z = x 
Name
Symmetry Transitivity

A(u) used
y = u u = z
f(u) = f(y)
¬A(u) z = u 
We shall abbreviate (x = y
∧ y = z) as x = y = z.
5. is an axiom schema with f ranging among functors between any two types.
6. can also be deduced from symmetry.
Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
Another possible list of axioms of equality consists in formulas 1. to 5. where f and
A range over the mere symbols of the language, each taken once per argument :
the full scheme of 2. is implied by successive deductions for each occurrence of symbol
in A. This will be further justified in 2.9 (equivalence
relations).
Introducing a variable x defined by a term t by writing (x = t ⇒ ...),
in other words putting the axiom x = t, can be
seen as justified by the above rules in this way : t = t ∴
∃x, (x = t ∴ ...).
Other languages:
FR : 1.9. Quantificateurs