3.1. What is a mathematical theory

We first introduced the notion of mathematical theory in our first text on the foundations of mathematics, especially sections

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:
Some first detailed comments on what is a mathematical theory, were moved from the present page to text 1. First foundations of mathematics, sections 1.1 to 1.3. There were completely rigorous (self-contained) presentations of the two most important cases for the foundations of mathematics
and detailed descriptions of
But both translations are not the inverse of each other.
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.

The contents of a theory

Once chosen the framework, a theory is specified by its content (vocabulary), 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 does not exist any of the 4th kind of components (also built using the previous kind of components):

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

Provability and the Completeness Theorem

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 TA if a proof of A exists; refutable in T, if T⊢ ¬A; undecidable if it is neither provable nor refutable.

The completeness theorem (Gödel's thesis) gives model theory its strength, establishing the equivalence between realism and formalism for first-order theories. Proven for a specific proving formalism (we shall skip here its effective expression that would not be so interesting), it makes the concept of provability perfect and independent of the choice of formalism with the same quality:

Completeness Theorem.   There exists general and complete (algorithmic) rules of proof for first-order logic (for all first-order theories), in the following (equivalent) senses
Proof of the first statement :
[quantifiers are introduced in 1.7; the language must be well-orderable in order for the below step 4 to proceed]
  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 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.
  3. 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]
  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).
  5. 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.
  6. 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"). ∎
Proof of the second statement as deduced from the first :
⇔ The theory (T + ¬A) is inconsistent
⇔ The theory (T + ¬A) has no model
A is true in all models of T.  ∎

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

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