1.9. Axioms and proofs
Statements
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, a statement A
will have a definite Boolean value only depending on the choice of a system M
that interprets its language. We denote M⊨A the truth of A in M.
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. Let us explain.
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 formally given theory T=(τ, L, X) with an
axioms list X, that means to define the class of its models M, which
will be denoted M⊨T, as that of all systems interpreting the language L
where all axioms (elements of X) are true.
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 this case, 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.
Non-realistic theories outside mathematics (not called "axiomatic" by lack of mathematical form)
would be works of fiction describing imaginary or possible future systems.
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.
Provability
A proof of a statement A in a theory T, is a finite
model of a one-proof theory (reduction of proof theory to the description of a single proof),
having A as "conclusion" and involving a finite list of axioms among those of T.
Suitable full formalizations for the concept of proof for first-order logic could be found by specialists.
Such formalizations can take the form of precise (one-)proof theories, or proof verification algorithms
(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 T ⊢ A if a proof of A in T exists. 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 if it is provable with L, without using any axiom.
This might be written ⊢ A but for
full accuracy it needs to be written L ⊢ A (meaning that A is theorem of the
theory made of L without axiom, thus of any other theory containing L). 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.
A refutation of A in T amounts to a contradiction of the theory T∧A obtained
by adding A to the axioms of T.
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
((T ⊢ A) ∧ (T ⊢ B))
⇔ (T ⊢ A∧B)
((T ⊢ A) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).
So a contradiction can be presented as a proof of A with a refutation of A.
In an inconsistent theory, every statement is provable. Its framework being sound, such a theory has no model.
Beyond the required quality of soundness of the proof theoretical part of a logical framework,
more remarkable is its converse quality of completeness : that for any axiomatic theory
it describes, any statement that is true in all models is provable. In other words, any unprovable
statement is false somewhere, and any irrefutable statement is true somewhere. Thus, any
consistent theory has existing models, but often a diversity of them, as any undecidable
statement is true in some and false in others. Adding some chosen undecidable statements
to axioms leads to different consistent theories which can «disagree» without conflict, all
truly describing different existing systems.
Other languages:
FR : 1.9. Axiomes et preuves