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 domain 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 existential quantifier ∃, read as «There exists x
(in...) such that... »
 The universal quantifier ∀, read as «For all x (in...),... »).
Their interpretation can be defined in a set theoretical framework considering
A as a function, and treating its boolean values as objects:
(∀x, A(x))
⇔ A = (x ↦ 1)
(∃x, A(x)) ⇔ A ≠ (x ↦ 0)
(∀x, A(x)) ⇎ (∃x, ¬A(x))
In set theory, (∀x∈E, A(x)) ⇔ {x∈E
 A(x)} = E. The formula (∀x,1)
is always true. With classes,
(∃_{C } x, A(x))
(∀_{C } x, A(x))
∀x, (C(x)

⇔ (∃x, C(x) ∧ A(x))
⇔ ∃_{C∧A} x, 1
⇔ (∀x, C(x) ⇒ A(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 t, … to
∃ then from ∃ to z, amounts to letting z represent
one of t, t′, … (without knowing which). 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.
Deductions can be made by these rules, reflecting 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)) 
(∃_{A} x, ∀_{B}
y, R(x,y)) 
⇒ (∀_{B}y, ∃_{A} x,
R(x,y)) 
Also (∀_{C }x, A(x)∨B(x))
⇒ ((∀_{C }x, A(x)) ∨ (∃_{C }x,
B(x)))
Status of open quantifiers in set theory
Set theory is translated to a generic theory by converting to
classes the domains of quantifiers:
(∃x∈E,
A(x)) → (∃x, x ∈ E ∧ A(x))
(∀x∈E, A(x)) → (∀x, x
∈ E ⇒ A(x))
Set theory only admits quantifiers over sets, called bounded
quantifiers, in its formulas (also called bounded formulas
for insistence) that define predicates and can be used in terms. But
its translated form as a generic theory allows quantifiers on
classes (or the universe), called open quantifiers.
Formulas with open quantifiers in set theory will be called statements.
Their use will be essentially restricted to declarations of truth of
ground definite statements. These will first be axioms, then theorems
deduced from them.
Open quantifiers in statements will usually be expressed as common
language articulations (naturally using the above rules of proofs)
between their bounded subformulas written in settheoretic symbols.
The setbuilder K = {x∈E A(x)}
was defined by a statement (∀x, x∈K ⇔
(x∈E ∧ A(x))) but 1.11 will
redefine it without open quantifier (except on its parameters).
Other languages:
FR : 1.9. Quantificateurs