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 range 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:
• 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:

(∀xE, A(x)) ⇔ {xE | A(x)} = E.

The one of first-order 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 (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.

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

Second-order quantification

Let us call second-order 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 first-order logic, but belongs to some other logical frameworks instead, such as second-order logic (part 5).
Still while keeping first-order logic as the main framework of a given theory, some second-order 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 first-order theory, T' its extension by a structure symbol s (without further axiom) and F a ground formula of T' (in first-order logic) also denoted F(s) when seen as a formula of T using the variable structure symbol s in second-order logic.

Second-order Universal Introduction. If T'F then T entails the second-order 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.

Second-order Universal Elimination. Once a second-order statement (∀s, F(s)) is accepted in a theory T, it is manifested in first-order 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 second-order universal elimination after second-order universal introduction, means deducing from T a schema of theorems, each one indeed deducible in first-order logic by the proof obtained from the original proof by replacing s by its definition.

In second-order 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 second-order universal elimination, this comes down to a schema of definitions in first-order 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 first-order 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 second-order universal elimination of the variable unary predicate A:
1. x, x = x (reflexivity)
2. A,∀x,∀y, (x = yA(y)) ⇒ A(x).
Variables x and y can also serve among parameters in definitions of A. This can be understood by re-ordering 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 SymmetryTransitivity A(u) used y = u u = z f(u) = f(y) ¬A(u) z = u
We shall abbreviate (x = yy = 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 ∴ ...).

 Set theory and Foundations of Mathematics 1. First foundations of mathematics 1.9. Quantifiers ⇨1.10. Formalization of set theory Philosophical aspects Time in model theory ⇨ Time in set theory 2. Set theory - 3. Algebra - 4. Arithmetic 5. Second-order foundations

Other languages:
FR : 1.9. Quantificateurs