1.9. Axioms and proofs


An expression is ground if its list of available free variables is empty (all its variables are bound), so that its value only depends on the system where it is interpreted.
In first-order logic, a statement is a ground formula. Thus, it will have a definite Boolean value (true or false) only depending on the choice of a system that interprets its language.
The axioms list of a theory is a set of statements, meant to be all true in some given system(s) (models of the theory as discussed below).


A proof of a statement A in a theory T, is a finite model of proof theory, involving A and a finite list of axioms among those of T.
Specialists could establish a full formalization for the concept of proof (the full details of a proof theory), which can take the form of a proof verification algorithm (only requiring an amount of computing resources related to the size of a given proof). But most mathematical works are only partially formalized : semi-formal proofs are used with just enough rigor to give the feeling that a full formalization is possible, yet not fully written; an intuitive vision of a problem may seem clearer than a formal argument. Likewise, this work will present proofs naturally without explicit full formalization : sometimes using natural language articulations, proofs will mainly be written as successions of statements each visibly true thanks to previous ones, premises, axioms, known theorems and rules of proof, especially those of quantifiers (1.10). Let us review some theoretical properties.

We say that A is provable in T, or a theorem of T, and write TA if a proof of A in T exists. This may be conceived in terms of a proof searching algorithm processed by a theoretical computer with unlimited (infinite) available time and resources, to try every possible piece of proof regardless its size until it eventually finds a conclusive proof of the given statement.
In practice, we only qualify as theorems the statements known as such, i.e. for which a proof is known. But synonyms for "theorem" are traditionally used according to their importance: a theorem is more important than a proposition; either of them may be deduced from an otherwise less important lemma, and easily implies an also less important corollary.

A statement A is called logically valid, which is written ⊢ A, if it is provable without using any axiom (thus a theorem of any theory regardless of axioms). Then A is true in every system by virtue of the logical framework. The simplest ones are the tautologies; others will be given in 1.10.
A proof of A from some axioms can also be seen as a proof of (conjunction of these axioms ⇒ A) without axiom, thus showing the logical validity of this implication.

Again in T, a refutation of A is a proof of ¬A. If one exists (T ⊢ ¬A), the statement A is called refutable (in T).
A statement is called decidable (in T) if it is either provable or refutable.

A theory T is called contradictory or inconsistent if T ⊢ 0, otherwise it is called consistent. If a statement is both provable and refutable in T then all are, because it means that T is inconsistent, independently of the chosen statement:

⊢ (A ∧ ¬A) ⇔ 0
((TA) ∧ (TB)) ⇔ (TAB)
((TA) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).

In an inconsistent theory, every statement is provable. Such a theory has no model.

Realistic vs. axiomatic theories in mathematics and other sciences

Apart from the distinction of nature (mathematical vs. non-mathematical), theories may also differ by the intention of their use, between realism and formalism.

A realistic theory is a theory involved to describe either a fixed system or the systems from a range, seen as given from some independent reality. For this, a list of axioms is chosen as a set of statements which, for some reason, are considered known as true on the intended system(s). Such a theory is said to be "true" if its axioms are indeed true there.

The truth of realistic theories is usually well ensured in pure mathematics, but those of other fields may be questionable: non-mathematical statements over non-mathematical systems may be ambiguous (ill-defined), while the truth of theories of applied mathematics may be approximative, or speculative as the intended system(s) may be unknown (contingent among alternative possibilities, that are equally possible thus mathematically "existing"). A theory beyond pure mathematics is called falsifiable if, in principle, the case of its falsity can be discovered by finding a mismatch between its predictions (theorems) and observations. For example, biology is relative to a huge number of random choices silently accumulated by Nature on Earth during billions of years ; it has lots of "axioms" which are falsifiable and require a lot of empirical testing.

An axiomatic theory is a theory given formally with an axioms list that means to define the range of models, as the class of all systems, interpreting the given language, where all axioms are true (rejecting those where some axiom is false). This makes automatic the truth of axioms in any model. Outside pure mathematics, non-realistic theories (not well called axiomatic, as the use of axioms may lose clarity) would be works of fiction describing imaginary or possible future systems.

For example Euclidean geometry first came as a realistic theory of applied mathematics (for its role of first theory of physics), but is now understood as an axiomatic theory of pure mathematics in a landscape of diverse equally legitimate geometries, while the real physical space is more accurately described by the non-Euclidean geometry of General Relativity.

Completeness of first-order logic

The problem of formalizing the concept of «proof» actually has a perfect solution for first-order logic, in the sense of leading to the perfect concept of provability, equivalent to truth in all models. Indeed, as proofs must be logical deductions, every theorem will be true in each model (where all axioms are true), but the converse also interestingly holds, according to the completeness theorem, which was originally Gödel's thesis : if a statement is true in all models of a given first-order axiomatic theory, then it is provable in it. In other words, any formally consistent axiomatic theory (set of first-order statements) does match some existing system; and any undecidable formula will be true in some models and false in others. Thus different consistent theories may «disagree» without conflict, by being all true descriptions of different systems, all mathematically existing without any issue of «where they are».
Such a perfect formalization is essentially unique in the sense that any for any two of them, any "proof" for the one can be translated into a "proof" for the other.

This quality of first-order logic, with its ability to express all mathematics (any logical framework beyond it can anyway be developed from set theory, itself expressible in first-order logic), gives it a central importance in the foundations of mathematics, and dissolves much of a priori disagreements between realism (Platonism) and formalism : any consistent axiomatic theory describes some mathematical reality (model) that exists, but is generally not unique, as an unlimited diversity of models may remain. So, for a realistic theory to not be an axiomatic theory, requires to conceive its intended (range of) system(s) otherwise than by the criteria of mathematical existence and satisfaction of given first-order statements.

The proof of the completeness theorem (given in 4.6) will consist in building a model of any consistent first-order axiomatic theory, as follows. The infinite set of all ground terms with operation symbols derived from the theory (those of its language plus others coming from its existence axioms), is turned into a model by progressively defining each predicate symbol over each combination of values of its arguments there, while keeping consistency. As this construction just involves the data of a theory and the set ℕ of natural numbers, the validity of this theorem only depends on the axiom of infinity, that is the existence of ℕ as an actual infinity.
The very definition of provability already involves infinity, as it means the existence of a proof without any limit of size. The size (complexity) of a proof, reflects the number of elements that need to be described in an attempted construction of a counter-example to a given theorem, to observe the necessary failure of this construction (while the choice of formalization only affects the size of proofs in more moderate proportions); this is not a priori predictable from, say, the size of the statement, for reasons which will be developed later.

Provability (with a fixed language) can also be expressed as a formula of first-order arithmetic (theory with the only type "natural number", constants 0,1, and operation of addition and multiplication), stating the existence of a number which encodes a proof, related to the free variable which encodes a statement (candidate theorem), depending on a predicate that encodes the axioms list. This is independent of the formalism of proof encoding, in the sense that all formulas expressing valid solutions to encode "provability" are provably equivalent to each other, under the ordinary axioms of first-order arithmetic which will be sketched in 4.3 and 4.4.
However, these axioms do not suffice to make these formulas decidable for every value of the free variable. To give full definiteness (Boolean values) to these formulas and any other formulas of arithmetic, requires to interpret arithmetic not axiomatically but realistically, in its ideal model called the standard model of arithmetic, intuitively described as the true set ℕ of exactly all really finite natural numbers, as will be clarified in Part 4.

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
1.9. Axioms and proofs
1.10. Quantifiers
Philosophical aspects
Time in model theory
Set theory as unified framework
2. Set theory - 3. Algebra - 4. Arithmetic 5. Second-order foundations
Other languages:
FR : Aspects philosophiques