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 limitationn 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 such a measure.
There are two 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. Variant (a) has the disadvantage that it may not be clear how it can be applied to systems which are not about numbers. Variant (b) has the disadvantage that it is not clear what other machinery is to be considered available for the consistency proof.
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).
Anyone know what the conditions are?
(answers in an email to: 
)
There is a little bit about this in Beeson's Foundations of Constructive Mathematics.
A more comprehensive discussion is in Pohlers' book Proof Theory, which is basically about ordinal analysis, which means discovering the proof theoretic (or ordinal) strength of axiom systems.
©
created 1994/9/18 modified 1998/7/27