The main useful formalisms (kinds of theories), from the weakest (less expressive) to the strongest (most expressive), except set theory, 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;

- A natural inclusion of all first-order theories into set theory, viewing their possible models as objects in a common model (universe) of set theory (1.3, 1.4). This view is the usual framework for ordinary mathematics, able to study many systems as "sets together with relations or operations such that...", but also possible connections between them.
- Another procedure (sections 1.9, 1.10) to translate a set theory into the format of a first-order theory (but its interest is more restricted to specialized studies in the foundations of mathematics)

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**, whose translations into set theory are**names of sets**. For example, geometry can be seen with 2 types: «points» and «lines».

- A list of
**symbols of structures**. These symbols aim to designate structures, that is connections between objects with specific types. They give their roles to the objects of each type in connection with those of 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 arguments of an operation is called its arity.

- A constant is the particular case of a nullary operation
(it has no argument).

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

*n*-ary operations f(*x*_{1},...,*x*_{n}) as particular cases of (*n*+1)-ary relations, namely, those with a unique value of*y*related to any combination of values of*x*_{1},...,*x*_{n}, to serve as the relation (*y*=f(*x*_{1},...,*x*_{n})). - 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) plus possible logical connectives and quantifiers (∀and ∃), supposed to be true when these symbols are interpreted in a given system. Axioms are expressions of a selection of models: a choice to only consider those systems of sets with structures where these axioms are true, to be called models of this theory (a system of objects described by the theory), excluding other systems from this title.

But for having any interest for most practical purposes, a
theory should be such that **there cannot exist**, built on
the above, any of the 4th 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).

A *proof * of a formula *A* in a first-order theory
*T*, is a finite model of *proof theory*, connecting *A*
to some axioms 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.

A theory *T* is said *contradictory* or *inconsistent*
if there exists a contradiction, i.e. *T*⊢ 0. Or
equivalently, there are proofs of any 2 formulas that are the
negation of each other. In an inconsistent theory, every formula
is provable. Such a theory has no model. A theory without
contradiction is said *consistent*.

Let us assume that there is such a thing as proof theory (a
system of rules of proof) that will make things fit, so that the
existence of a proof of *A* in *T* ensures the truth
of *A* in every model of *T*. The converse property
constitutes the completeness theorem (Gödel's thesis) ; it gives
model theory its strength, establishing the equivalence between
realism and formalism for first-order theories. Proven for a
specific system of rules of proof, it makes the concept of
provability perfect and independent of the choice of formalism
with the same quality:

- Any consistent first-order theory has a model.

- Any «true consequence» of any first-order axiomatic theory (formula true in all models) is a theorem (formally provable by these rules).

- 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 occurrence of ∃ in an axiom by an additional
operator symbol
*K*to the language of the theory, following the rule that generalizes in the obvious way

(∀*x*,*x'*, ∃*y*, ∀*z*,*A*(*x*,*x'*,*y*,*z*)) ⇢ (∀*x*,*x'*,∀*z*,*A*(,*x*,*x'**K*(*x*,*x'*),*z*)).

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

- Replacing the remaining variables of each axiom (now all under
∀) 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.

- Observe that the resulting theory
*T'*is still consistent, as any contradiction in*T'*can be converted into a contradiction in the initial theory*T*(without using the axiom of choice that anyway cannot be used in proofs outside set theory), as follows:

For every (closed) subterm whose root is a new symbol *L*, occurring in the proof (each considered only once no matter its number of occurrences in the proof), for example terms*L*(*t*_{0},t_{1}) and*L*(*t*_{0},t_{2}) (where*t*_{0},*t*_{1}and*t*_{2}are closed terms), produced by an axiom like

(∀*x*,∃*y*,∀*z*,∃*u,**A*(*x*,*y*,*z,u*)) transformed into (∀*x,z,**A*(*x,K*(*x*),*z*,*L*(*x,z*)))

the reasoning in*T*should start by

"Let*y*such that ∀*z*,∃*u,**A*(*t*_{0},*y*,*z,u*);

let*u*_{1}such that*A*(*t*_{0},*y*,*t*_{1}*,**u*_{1});

let*u*_{2}such that*A*(*t*_{0},*y*,*t*_{2}*,**u*_{2});"

and continue by using the proof from*T'*where*y*replaces*K*(),*t*_{0}*u*_{1}replaces*L*(*t*_{0},t_{1}) and*u*_{2}replaces*L*(*t*_{0},t_{2}).

- 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 (if infinite, the language needs to be well-orderable for this step to proceed).
- Then the quotient [see 2.9] 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, this still does not make everything clear about provability and existence of models:ese constructions are not really as explicit as they might seem,:

- 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 choice of order between formulas, an infinity of other models are possible, resulting from other choices, that can be as worthy and legitimate but with different properties ;
- Once this choice is made, the contruction of the model is
still not really effective, as it cannot be processed by any
finite being such as human thought or computer, thus it cannot
be called explicit from such viewpoints. Instead, this
construction requires an infinity of steps, each of which
involves an infinite knowledge (to decide if a new axiom remains
consistent consistent with previous axioms: this is the answer
to a halting
problem of search for contradiction). Actually, for many
theories (and especially foundational ones such as set theory),
no model can ever be built in an algorithmic manner.

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