As we shall do for the axioms of equality (below) and for set theory (in 2.1 and 2.2), a theory may be first expressed in second-order logic for intuitive reasons, before formally interpreting this as a convenient meta level tool to abbreviate a first-order formalization, as follows.Let T be a first-order theory, T' its extension by a structure symbol s (without further axiom) and F a statement 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 deducible in first-order logic by replacing s by its respective definition in the original proof.
Arithmetic (the theory describing the system ℕ of natural numbers with four symbols 0, 1, +, ⋅ ) can be "completely" formalized in second-order logic (axioms listed in 4.3 and 4.4) in the sense of excluding non-standard models, thus determining in principle the values of all its first-order statements as true or false. The only component of this formalization beyond first-order logic is the axiom of induction, using a ∀ ranging over "all unary predicates" (including undefinable ones). However the incompleteness theorem (1.C) will refute the possibility for any algorithm to give the correct values of all first-order statements of arithmetic.But the range of the mere definable structures of a type cannot be completely defined either for the same reason, since defining the exact infinite range of all possible defining expressions, amounts to defining ℕ.
∀a, ∀b, (∀x, ∀y, R(a, b, x,y)) ⇒ R(a, b, a,b).
Diverse definitions of A give diverse statements (assuming reflexivity):
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
| A(u) used
y = u
u = z
f(u) = f(y)
z = u
Remark. (1.∧7.) ⇒ 3., then 3. ⇒ (4. ⇔ 7) so that (1.∧7.) ⇔ (1.∧3.∧4.).
We shall abbreviate (x = y ∧ y = z) as x = y = z.
(∀x, x = x) ∴ t = t ∴ ∃x, (x = t ∴ ...).Binding one parameter, the definition of a functor symbol f by a term here abbreviated t with variable x (which will justify this abbreviated notation t like a functor symbol), is declared by the axiom
∀x, f(x) = t(x).Similarly, operator symbols can be defined by binding multiple parameters, and relations can be defined in the same way replacing = by ⇔.
∀A, (Bx, A(x)) = F(A)
where = becomes ⇔ if values are Boolean. 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.
|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
⇨ Time in model theory
|2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations|