These are my notes as I try to piece this topic together, rather fitfully, from what sources I have to hand.
|
Some definitions taken from Michael Beeson Beeson80.
|
|
A definition due to Tarski and used in Friedman's Concept Calculus [ FriedmanHarvey].
|
A more comprehensive discussion is in Wolfgang Pohlers' book "Proof Theory" [ Pohlers89], which is basically about ordinal analysis, which means discovering the proof theoretic (or ordinal) strength of axiom systems.
|
|
Proof Theoretic Strength is a measure of the Power of a formal system.
We know, from Gödels incompleteness results and also from later results in the theory of recursive functions, that where the
subject matter of a theory is sufficiently rich the theory will be incomplete.
Since being able to express quite elementary propositions about arithmetic is sufficient to qualify for this limitation any system which is a contender as a foundation for mathematics will be incomplete.
Not only do we know that such systems will be incomplete, we also know that there is no maximal system, which can prove more
than any other.
It therefore is meaningful to rank formal systems according to how much can be proven in the system.
Proof theoretic strength is one such measure.
There are several different ways in which the proof theoretic strength can be measured.
The first is also known as ordinal strength.
There are two variants of ordinal strength of which I am aware.
Variant (a) concerns what orderings of the natural numbers can be proven in the system to be well-orderings, the strength
being the smallest which is not provably well-ordered in the system.
Variant (b) concerns what is required to prove the consistency of the system, and is the least well-ordering necessary for
that purpose.
|
|
The second is perhaps more independent of the kind of mathematics addressed in the formal system, and is hence more generally
applicable.
This measure is more conspicuously related to the consequences of Gödels incompleteness results, particularly his second incompleteness
theorem about the provability of consistency of a formal system in itself.
Under this account of Proof Theoretic Strength one formal system is at strictly stronger than another if the consistency of
the second can be proven in the first.
There is some kind of connection between these two definitions, which I think are supposed to be definitions of the same thing.
One way of seeing this is by asking what the simplest way of proving the consistency of one set theory in another is.
You can prove the consistency of a formal system by giving a semantics to it, and then proving that all the theorems of the
system have some property, defined in terms of the semantics (e.g.
truth), which is known not to be universal.
Giving a semantics is done most straightforwardly by constructing a model (which is a co-domain for semantic mappings).
The natural model for a set theory is a set which turns out to be too large to be in the domain of the set theory (for well-founded
theories).
This means that if of two set theories one can prove the existence of a larger ordinal than the other then the first will
be able to prove the consistency of the second (but not vice-versa).
So under some conditions these definitions look as if they might coincide.
And also, under those conditions, the ordering must be linear (since the ordinals are well-ordered).
|
|
Beeson I - reducibility
Let T and S be theories.
Then T ≤ S if there is an interpretation from T to S, i.e. a map taking formulae φ of T onto formulae φ* of S such that T ⊢ φ implies S ⊢ φ* and ⊥* = ⊥.
Moreover. the interpretation must be recursively definable, i.e. φ* depends effectively on φ and the statement of the previous sentence, when formulated in peano arithmetic PA, must be a theorem
of PA.
By T ≡ S we mean T ≤ S and S ≤ T.
|
|
Beeson II - Ordinal Strength
Beeson writes I(«, φ), where « is some primitive-recursive well-ordering, for:
(∀x«y(φ(x))→φ(y))→∀x ∈ Field(«)φ(x)
I think that should be read:
(∀y(∀x«y(φ(x))→φ(y)))→∀x ∈ Field(«)φ(x)
He then proposes I(«) as an abbreviation for:
∀Y(I(«, x ∈ Y))
and if is a fixed natural well-ordering of type α then this may be further abbreviated as I(α).
By TI(α) we mean the schema I(, A) for all formulae A.
Proof theorists say that α is the ordinal of a theory T provided that α is the supremum of the provable well-orderings of T in the sense that for some natural primitive recursive
well-ordering « of type α, T proves I(Q) for every initial segment Q of « but fails to prove some instance of I(«).
There is an issue here about what "natural" means.
It may be that there is no incontestably correct formal interpretation of this term, and that there might therefore be multiple
conceptions of ordinal strength corresponding to different interpretations of the word "natural".
|
|
In this case the ordering is derived from a pre-order "T interprets S".
The degrees are then the equivalence classes derived from this pre-order.
Interpretation as here conceived is a relation between first order theories.
|
|
Definition of Interpretation
An interpretation of S in T consists of
- A one place relation defined in T which is meant to
carve out the domain of objects that S is referring to,
from the point of view of T.
- A definition of the constants, relations, and functions
in the language of S by formulas in the language of T,
whose free variables are restricted to the domain of
objects that S is referring to (in the sense of i).
- It is required that every axiom of S, when translated
into the language of T by means of i,ii, becomes a theorem
of T.
|
|
Flexibility
It is now standard to allow quite a lot of flexibility in
i-iii. Specifically
- Parameters are allowed in all definitions.
- The domain objects can be tuples.
- The equality relation in S need not be interpreted as
equality â but, instead, as an equivalence relation. The
interpretations of the domain, constants, relations must
respect this equivalence relation. Functions are
interpreted as "functional" relations that respect this
equivalence relation.
|
|
Definition of Proof Theoretic Ordinal - I
The Proof Theoretic Ordinal of a formal theory T is the order type of the smallest well-ordering which is needed for a consistency proof of T.
|
|
Provable Ordinals
An ordinal is provable in a theory T if it is the order type of a primitive recursive order which can be proven in T to be
a well-order.
|
Definition of Proof Theoretic Ordinal - II
The Proof Theoretic Ordinal of a formal theory T is the least ordinal not provable in T.
|
|