1.9. Axioms and proofs


An expression is ground if its list of available free variables is empty, 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 mathematical 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).


In this work like almost anywhere else, proofs will be written naturally without any full formalization of the concept of proof (the full details of a proof theory, which can take the form of a proof verification algorithm, that is known by specialists). Sometimes using natural language articulations, they will mainly be written as a succession 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 just review some theoretical properties.
A proof of a statement A in a theory T, is a finite model of proof theory, involving A and some axioms of T (in finite number).
We say that A is provable in T, or a theorem of T, and write TA if a proof of A in T exists.
By the design of proof theory, a proof is a logical deduction, so that every theorem is also true in each model (any system where axioms are true).
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.

Statements or formulas having like tautologies the property of being true in every system by virtue of the logical framework are called logically valid ; they are necessary theorems of any theory regardless of axioms where they need not appear. More logically valid formulas 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 establishing the logical validity of this implication. But, beyond tautologies, logically valid statements with some size may be only provable by proofs with indescribably larger size.

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 for those of 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 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 very many "axioms" which are falsifiable and keep requiring a lot of empirical testing.

An axiomatic theory is a theory given formally with an axioms list that means to define the selection (range) of models, as the class of all systems (interpreting the given language) where all these axioms are true, rejecting others where some axiom is false. By this definition, the truth of axioms in any model holds automatically. This way, any consistent axiomatic theory describes a mathematical reality (model) that exists, but is generally not unique, as an unlimited diversity of models may remain. In particular, any undecidable formula will be true in some models and false in other models (which are equally real and legitimate interpretations). Different consistent theories may «disagree» without conflict, by being all true descriptions of different systems, that may equally «exist» in a mathematical sense without any issue of «where they are». In fields outside pure mathematics, non-realistic theories (to not say axiomatic theories, as the use and truth of axioms may lose clarity) would be works of fiction describing imaginary or possible future systems.

For a concept of realistic theory to differ from that of axiomatic theory, requires another intended (range of) system(s) than the criteria of mathematical existence and satisfaction of given statements (as any consistent set of statements matches a possible and therefore existing system, by the below mentioned completeness theorem).

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

Completeness of first-order logic

While provability naturally implies truth in all models, an interesting property of provability in first-order logic is the converse property called completeness (forming an equivalence between truth in all models and provability): every statement that is true in all models of any given axiomatic theory in first-order logic, is provable. This completeness theorem, was originally Gödel's thesis. It gives to the concepts of «proof», «theorem» and «consistency» (vague a priori concepts from intuition) perfectly suitable mathematical definitions, and practically eliminates any object of disagreement between realism (Platonism) and formalism for first-order logic. This remarkable property of first-order logic, together with the fact that all mathematics is expressible there (what is not directly there can be made so by insertion into set theory, itself formalized as a first-order theory), gives this framework a central importance in the foundations of mathematics.

The proof of the completeness theorem, first expressed as the existence of a model of any consistent first-order theory, goes by constructing such models out of the infinite set of all ground expressions in a language constructed from the theory (the language of the theory plus more symbols extracted from its axioms). As the set of all ground expressions in a language can itself be constructed from this language together with 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, sufficient for all theories (ignoring the diversity of infinities in set theory).

However, these are only theoretical properties, assuming a computer with unlimited (potentially infinite) available time and resources, able to find proofs of any size. Not only the precise size of a proof may depend on the particular formalism, but even some relatively simple formulas may only have «existing» proofs that «cannot be found» in practice as they would be too long, even bigger than the number of atoms in the visible physical Universe (as illustrated by Gödel's speed-up theorem). Within limited resources, there may be no way to distinguish whether a formula is truly unprovable or a proof has only not yet been found.

To include their case, the universal concept of provability (existence of a proof) has to be defined in the abstract. Namely, it can be expressed as a formula of first-order arithmetic (the first-order theory of natural numbers with operations of addition and multiplication), made of one existential quantifier that is unbounded in the sense of arithmetic (∃ p, ) where p is an encoding of the proof, and inside is a formula where all quantifiers are bounded, i.e. with finite range (∀x < (...), ...), expressing a verification of this proof.

However, once given an arithmetical formula known to be a correct expression of the provability predicate (while all such formulas are provably equivalent to each other), it still needs to be interpreted. This involves the concept of the realistic truth in first-order arithmetic. This is the ideally meant interpretation of arithmetic: the interpretation of statements of first-order arithmetic in «the true set ℕ of all, and only all, really finite natural numbers», called the standard model of arithmetic.

Set theory and Foundations of mathematics
(general table of contents)
1. First foundations of mathematics
(detailed table of contents)
1.A. Philosophical aspects
(Each subsection roughly uses those left and up)
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
Intuitive representation and abstraction
Platonism vs Formalism
1.3. Form of theories: notions, objects, meta-objects
Realistic vs. axiomatic theories
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.B. Time in Model theory
The time of interpretation
The metaphor of the usual time
The infinite time between models
1.6. Logical connectives
1.7. Classes in set theory
1.C. Truth undefinability
The Berry paradox
Zeno's Paradox
1.8. Binders in set theory 1.D. Time in Set theory
Expansion of the set theoretical universe
Can a set contain itself ?
1.9. Quantifiers
The relative sense of open quantifiers
1.E. Interpretation of classes
Classes in an expanding universe
Concrete examples
1.10. Formalization of set theory
1.11. Set generation principle
Justifying the set generation principle
1.F. Concepts of truth in mathematics
Alternative logical frameworks
2. Set theory (continued)
Other languages:
FR : Aspects philosophiques