3.1. What is a mathematical theory

We first introduced the notion of mathematical theory with detailed explanations in our first text on the foundations of mathematics, especially sections 1.1, 1.3, 1.4, 1.5, 1.6, 1.8, 1.9 and the Platonism vs Formalism subsection.

The main useful formalisms (kinds of theories), from the weakest (less expressive) to the strongest (most expressive), except set theory, are:
We already explained the two most important formalisms : first-order theories (called there «generic theories»), and the formalism of set theory that is specific (with definiteness classes, and binders depending on sets) and escapes this hierarchical order between formalisms, as we described irreversible correspondences between both (not the inverse of each other):
Let us continue this exposition, summing up the content of theories (first mentioned in 1.3) and going further.

The contents of a theory

Once chosen a formalism, a theory is specified by its content (vocabulary and axioms), as follows.

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 :

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:

Let us examine in more details the properties of these concepts of "proof" and "contradictions"

Provability and the Completeness Theorem

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 TA 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:

Completeness Theorem. First-order logic has a proper proving system (a proof theory, with algorithmic verifiability), in the following (equivalent) senses
Sketch of proof of the first statement (making this fact intuitive but without entering the details ; specifying the rules of proof would be too tedious at this step and not so interesting) :
  1. Rewrite [through equivalences in 2.1 and 2.2] each axiom into a chain of quantifiers applied to a quantifier-free formula (prenex form).
  2. 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)).
  3. 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]
  4. 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.
  5. 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, occuring in the proof (each considered only once no matter its number of occurrences in the proof), for example terms L(t0,t1) and L(t0,t2) (where t0, t1 and t2 are closed terms), produced by an axiom like
    (∀x,∃y,∀z,∃u, A(x,y,z,u)) ⇢ (∀x,z, A(x,K(x),z, L(x,z)))
    then the reasoning in T should start by
    "Let y such that ∀z,∃u, A(t0,y,z,u);
    let u1 such that A(t0,y,t1,u1);
    let u2 such that A(t0,y,t2,u2);"
    and continue by using the proof from T' where y replaces K(t0), u1 replaces L(t0,t1) and u2 replaces L(t0,t2).
  6. 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).
  7. 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"). ∎
Deduction of the second statement from the first :
TA
⇔ The theory (T + ¬A) is inconsistent
⇔ The theory (T + ¬A) has no model
A is true in all models of T.  ∎

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,:

Later, incompleteness results will show how serious are these remaining gaps.

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