Logical quantifiers

1.10. Quantifiers

A quantifier is a binder taking a unary predicate (formula) and giving a Boolean value.

Bounded vs open quantifiers

A quantifier Q is called bounded when following the use format for binders in set theory (1.8) : its range is a set given as an argument. For quantifiers this format is written (Q ∈ , ) filled as (Qx∈E, A(x)) to take as input a unary predicate A, by binding a variable x with range E on any formula here abbreviated as A(x) to mean it defines A with argument x and possible parameters.
Primitively in first-order logic, the ranges of quantifiers are types (the same type as the bound variable, not formally an argument). Any range E (type, class or set) may be marked as an index (Q_Ex, A(x)), or deleted altogether (Qx, A(x)) when it is unimportant or implicit as fixed by the context.
When set theory is formalized in first-order logic, the quantifiers from first-order logic, ranging over the universe, and their variants ranging over classes (defined from them below), are called open quantifiers to be distinguished from the restricted case of bounded quantifiers (as sets are there particular cases of classes). In this context, a formula is qualified as bounded if all its quantifiers are bounded. Only these formulas will be accepted for some uses (1.A, 1.C, 2.1, 2.2).

Both main quantifiers

There are two main quantifiers (from which others will be defined in 2.4):

The universal quantifier ∀ means «for all»: (∀x∈E, A(x)) is read «For all x in E, A(x)».
The existential quantifier ∃ means «there exists»: (∃x∈E, A(x)) is read «There exists x in E such that A(x)».

The bounded universal quantifier is definable from the set builder:

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

Quantifiers with any range can be defined in interpretations, seeing A as a function and its Boolean values as objects:

(∀x, A(x)) ⇔ A = (x ↦ 1)
(∃x, A(x)) ⇔ A ≠ (x ↦ 0)
(∃x, A(x)) ⇎ (∀x, ¬A(x))

(∀x, 1) is always true. Quantifiers over classes can be defined as

(∀_C x, A(x)) ⇔ (∀x, C(x) ⇒ A(x))
(∃_C x, A(x)) ⇔ (∃x, C(x) ∧ A(x)) ⇔ ∃_C∧A x, 1

Inversely any class is definable from a quantifier over it : ∀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))
(∃_Cx, A(x)) ⇒ (∃_Cx, B(x))
(∀_Cx, A(x)) ⇒ (∀_Cx, B(x))

Rules of proofs for quantifiers on a unary predicate

Just like expressions were described by allowing to take already made expressions to form new ones, the concept of proof may be formalized by using already known proofs to form new ones. Here are some intuitively introduced rules, still without claim of full formalization.

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: ∀_Cx, A(x) means that its negation ∃_Cx, ¬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 ∀_Cx, A(x).

Universal Elimination. If ∀_Cx, 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.

Some logically valid formulas

The above rules can be used to justify the following logically valid formulas

((∀_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x))) ⇒ (∀_Cx, B(x))
((∃_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x))) ⇒ (∃_Cx, B(x))
((∀_Cx, A(x)) ∧ (∃_Cx, B(x))) ⇒ (∃_Cx, A(x) ∧ B(x))
(∀_Cx, A(x)∨B(x)) ⇒ ((∀_Cx, A(x)) ∨ (∃_Cx, B(x)))
(∀_A x, ∀_B y, R(x,y)) ⇔ (∀_B y, ∀_A x, R(x,y))
(∃_A x, ∃_B y, R(x,y)) ⇔ (∃_B y, ∃_A x, R(x,y))
(∃_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))

We shall use the following abbreviations, also similarly with bounded quantifiers:

(∀_C x,y, ) means (∀_C x, ∀_C y, ) and so on for more variables with the same range.
(∃_C x,y, ) means (∃_C x, ∃_C y, ) (same remark).
(∀_Cx≠y, ) means (∀_Cx,y, x≠y ⇒ )
(∃_Cx≠y, ) means (∃_Cx,y, x≠y ∧ )
(∃_Cx, A(x) ∴ B(x)) means (∃_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x)), while it implies but is not always equivalent to (∃_Cx, A(x) ∧ B(x)).

Logical validity depends on language because, with only one type

(L ⊢ ∃x, 1) ⇔ (a constant symbol exists in L)

(With more types the condition is more complicated; but as most useful theories require all types to be nonempty, the dependence on language may be ignored in practice)

Completeness of first-order logic

First-order logic was found complete as expressed by the completeness theorem, which was originally Gödel's thesis : from a suitably formalized concept of «proof», the resulting class of (potential) theorems A of any first-order theory T was found to be the "perfect" one, coinciding with the class of universally true statements (true in all models M):

∀A, (T ⊢ A) ⇔ (∀M, (M⊨T)⇒(M⊨A))

Such a proof theory for first-order logic is essentially unique: the equivalence between any two sound and complete proof theories as concerns the existence of a proof of a statement in a theory, concretely appears by the possibility to translate any "proof" for the one into a "proof" for the other.

This quality of first-order logic confirms its central importance in the foundations of mathematics, after its ability to express all mathematics : any logical framework can anyway be developed from set theory (and more directly, any theory from any framework can be somehow interpreted in set theory), itself expressible as a first-order theory.

The proof of the completeness theorem, which requires the axiom of infinity (existence of ℕ) will consist in building a model of any consistent first-order axiomatic theory, as follows (details in 4.7). The (infinite) set of all ground terms with operator symbols derived from the theory (those of its language plus others coming from its existence axioms), is turned into a model by progressively defining each predicate symbol over each combination of values of its arguments there, by a rule designed to keep consistency.

This construction is non-algorithmic : it will involve an infinity of steps, where each step depends on an infinite knowledge (of whether the given predicate on given arguments, seen as a candidate additional axiom, preserves consistency with previously accepted ones). Actually, most foundational theories such as set theories, do not have any algorithmically definable model.

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,..., 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. Axioms and proofs ⇦ 1.10. Quantifiers ⇨1.11. Second-order quantifiers
	Philosophical aspects Time in model theory Truth undefinability Introduction to incompleteness Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations

Other languages:
FR : 1.10. Quantificateurs