1.1. Introduction to the foundation of mathematics

1.3. Structure of theories: objects, meta-objects, types

1.4. Structures and expressions

Philosophical Aspects of the foundations of mathematics

Let us give here further details and remarks.

The most important formalisms (kinds of theories), from the weakest (less expressive) to the strongest (most expressive), are:

- Algebraic theories;
- First-order theories

- Duality theories (that is a fuzzy range of theories with some common features);
- Second-order theories;
- Higher-order theories;
- Set theories (that may escape this hierarchy, as they may be related to others in different ways).

**First-order theories**(called there «generic theories»),

**Set theories**(because there is a specifically suitable formalism for set theories, with binding symbols specifying the sets that variables range over).

- How to naturally include (translate) all first-order theories
into the framework (language) of set theory, and see all
possible models of these theories as objects in one same model
of set theory. Much of ordinary mathematics, such as the study
of algebra, implicitly uses this embedding of first-order
theories inside set theory, when describing diverse systems of
objects as "sets together with relations or operations such
that..."

- Another procedure (sections 1.7, 1.8) to translate a set
theory into the format of a first-order theory (usually ignored
in ordinary mathematics, but of central interest for specialists
in the foundations of mathematics, especially for the study of
the independence of some formulas in set theory, and paradoxes
about the powerset)

These things will be assumed to be known from now on.

Now in these Parts 3 and 4, we shall give a more general overview and describe some more directly "interesting cases" of mathematical theories for the practice of mathematics, especially algebra and geometry.

Every theory is made of 3 kinds of components. Each of these 3 kinds of components of a theory, is a finite system built using the previous kind of components :

- A list of
**types of objects**, which are elementary formal labels. During the translation into the framework of set theory, the types of a non-set theory become**names of sets**. (In the simplest case, there is only one). Example : «points» and «lines». - A list of
**symbols of structures**. These symbols aim to designate structures, that is connections between objects of specific types. They give their roles to the objects of each type in connection with other types.

In first-order theories, a structure is either

- An
*operation*between a list of variables with respectively specified types (which aim to specify the types of their values), with values of also one specified type. The number of variables is called the arity.

- A constant is the particular case of an operation with
no variable (its arity is zero)

- A
*relation*, that is an operation with value «true» or «false».

*n*-ary operation as a particular case of an (*n*+1)-ary relation with variables*x*_{1},..,*x*_{n},*y*such that for all combinations of possible values of*x*_{1},..,*x*there exists a unique value of_{n}*y*related to them. - An
- A list of
**axioms**. Each axiom is a closed formula expressed using these symbols (a system of occurrences of symbols among logical symbols and symbols of structures) together with logical connectives and quantifiers, supposed to be true when these symbols take meanings as structures between sets. Axioms are expressions of a selection of models: a choice to only study those systems of sets connected with such structures where these axioms are true, excluding others from consideration.

But for having any interest for most practical purposes, a
theory should be such that **there does not exist** any of the
4th kind of components (also built using the previous kind of
components):

- A
**contradiction**of a theory, is a system of formulas connecting axioms of*T*, that forms a proof of the formula "False" (0). Or equivalently, proofs of any 2 formulas that are the negation of each other. A theory*T*is said*contradictory*or*inconsistent*if there exists a contradiction (*T*⊢ 0). In an inconsistent theory, every formula is provable. Such a theory has no model. A theory without contradiction is said*consistent*.

Given a first-order theory *T*, a *proof * of a
formula *A* is a finite system, model of the *proof
theory*, connecting *A* to (a finite number of) axioms
of *T*, ensuring the truth of *A* in every model of *T*.

We say that *A* is *provable in T* (or a *theorem
of T*) and write *T*⊢ *A* if a proof of *A*
exists; *refutable in T*, if *T*⊢ ¬*A*; *undecidable*
if it is neither provable nor refutable.

- Any consistent first-order theory has a model. (there exists a system of objects that it describes).
- Any «true consequence» of any first-order axiomatic theory
(formula true in all models) is a theorem (formally provable by
these rules).

[quantifiers are introduced in 1.7; the language must be well-orderable in order for the below step 4 to proceed]

- Rewrite [through equivalences in 2.1 and 2.2] each axiom into
a chain of quantifiers applied to a quantifier-free formula (prenex
form).

- Replace each occurence of ∃ in an axiom by an additional
operator symbol
*K*to the language of the theory, following the rule that generalizes (∀*x*,*x'*, ∃*y*, ∀*z*,*A*(*x*,*x'*,*y*,*z*)) ⇢ (∀*x*,*x'*,∀*z*,*A*(,*x*,*x'**K*(*x*,*x'*),*z*)) in the obvious way.

- Replace the equality predicate in axioms by an ordinary
predicate symbol to play the role of equality, together with the
axioms of equality [end of 1.4]

- Replacing the variables of each axiom by all possible closed
terms, gives a system of logical axioms whose Boolean variables
are the (closed) formulas of the form R(t,t',...) where R is a
predicate symbol and t,t',... are closed terms. Any
contradiction here would only involve a finite list of terms,
thus giving a contradiction to the initial theory (without using
the axiom of choice).

- Add one by one to the axioms, each of these Boolean variables if it is consistent with previous axioms, so that all get values without contradiction.
- Then the quotient [by the theorem of 2.8] of the set of closed terms by the equivalence relation of "equality", forms a model (with the "true equality"). ∎

T⊢A

⇔ The theory (T+ ¬A) is inconsistent

⇔ The theory (T+ ¬A) has no model

⇔Ais true in all models ofT. ∎

However, these constructions are not really as explicit as they might seem, as incompleteness results will show :

- As for proofs, nothing says how to find them. In principle, a proof of any theorem can be found by a theoretical computer with infinite available time and resources. But we have no such a computer available, and some "existing" proofs may be too long to be effectively found in practice. There may be no way to distinguish whether a formula is truly unprovable or a proof has only not yet been found.
- For the construction of models, every possible specification
is very complex: as models built this way depend on an arbitrary
order between formulas, an infinity of similarly worthy variants
are possible, and, for many theories such as set theory, none of
the resulting models can ever be algorithmic.

Next : 3.2. How mathematical theories develop

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Basics of set theory

3. Basics of Model Theory

3.1.What is a mathematical theory

3.2. How mathematical theories develop

3.3. Notion of Algebra

3.4. Relational systems and their morphisms

3.5. The Galois connection between (invariant) structures and permutations (automorphisms)

3.6. Second-order theories

3.7. Formalizations of Arithmetic

3.8. Non-standard models of Arithmetic

3.9. The Incompleteness Theorem