(∀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))
(∀_{C } x, A(x)) ⇔ (∀x, C(x) ⇒
A(x))
(∃_{C } x, A(x)) ⇔ (∃x, C(x) ∧ A(x))
⇔ ∃_{C∧A} x, 1
(∀_{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))
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. ((∀_{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))
(∃_{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))
(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)Firstorder 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 firstorder 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 firstorder 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 firstorder 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 firstorder theory.
The proof of the completeness theorem, which requires the axiom of infinity (existence of ℕ) will consist in building a model of any consistent firstorder 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 nonalgorithmic : 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,..., metaobjects 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.11.
Secondorder quantifiers
1.10. Quantifiers 
Philosophical
aspects 

2. Set theory  3. Algebra  4. Arithmetic  5. Secondorder foundations 