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

QxE, 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 (QEx, 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: 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, (∀xE, A(x)) ⇔ {xE | 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)) ⇔ ∃CA 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 (CA) 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)) ⇒ (∀By, ∃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:

(∃xE, A(x)) → (∃x, xEA(x))
(∀xE, A(x)) → (∀x, xEA(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 sub-formulas written in set-theoretic symbols.

The set-builder K = {xE| A(x)} was defined by a statement (∀x, xK ⇔ (xEA(x))) but 1.11 will redefine it without open quantifier (except on its parameters).

Set theory and Foundations of Mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Quantifiers
1.10. Formalization of set theory
1.11. Set generation principle
Philosophical aspects
Time in model theory
Time in set theory
Open quantifiers
Interpretation of classes
Concepts of truth in mathematics
2. Set theory (continued) 3. Model theory

Other languages:
FR : 1.9. Quantificateurs