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) called models of the theory (as discussed below).


A proof of a statement A in a theory T, is a finite model of proof theory, having A as "conclusion" and involving a finite list of axioms among those of T.
As explained later (and as precisely studied by specialists) the concept of proof can be fully formalized (a proof theory can be precisely written), 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, without actually writing it ; an intuitive vision of a problem may seem clearer than a formal reasoning. 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). Yet without giving details of proof theory, let us review some general 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 is the halting condition of a proof searching algorithm, processed by an abstract "computer" with unlimited (infinite) available time and resources, trying every possible piece of proof until it eventually finds a valid 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.

Any good proof theory needs of course to be sound, which means only "proving" always true statements : provability implies truth in every model (where all axioms are true).

Logical validity

For a given language L, a statement A is called logically valid, which is written ⊢ A, if it is provable with L, without using any axiom (thus a theorem of any theory containing L, regardless of axioms). Then A is true in every system interpreting L, thanks to the soundness of the logical framework. The simplest logically valid statements are the tautologies (whose Boolean variables are replaced by statements); others will be given in 1.10.

A proof of A using some axioms can also be seen as a proof of (conjunction of these axioms ⇒ A) without axiom, thus making this implication logically valid.

Refutability and consistency

A refutation of A in T, 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 provable or refutable.
A contradiction of a theory T is a proof of 0 in T. If one exists (T ⊢ 0), the theory T is called contradictory or inconsistent ; 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. Its framework being sound, such a theory has no model.
A refutation of A in T can be equivalently seen as a contradiction of the theory TA obtained by adding A to the axioms of T.

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.

An axiomatic theory is a theory given formally with an axioms list that means to define its 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. Non-realistic theories outside mathematics (not called "axiomatic" by lack of mathematical form) would be works of fiction describing imaginary or possible future systems.

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. Its given axioms are statements which, for some reason, are considered known as true on all these systems. Such a theory is true if all its axioms are indeed true there. In other words, these systems are models, qualified as standard for contrast with other, unintended models of that theory taken axiomatically.
This truth will usually be ensured for realistic theories of pure mathematics : arithmetic and set theory (though the realistic meaning of set theory will not always be clear depending on considered axioms). These theories will also admit non-standard models, making an effective difference between their realistic and axiomatic meanings.

Outside pure mathematics, the truth of realistic theories may be dubious (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 "real" systems may be unknown (contingent among other possible ones). There, a theory is called falsifiable if, in principle, the case of its falsity can be discovered by comparing its predictions (theorems) with 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.

Euclidean geometry was first conceived as a realistic theory of applied mathematics (for its role of first theory of physics), then became understood as an axiomatic theory of pure mathematics among diverse other, equally legitimate geometries in a mathematical sense; while the real physical space is more accurately described by the non-Euclidean geometry of General Relativity.

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