Notes on Proof Theoretic Strength
Overview
 There are a variety of orderings of deductives systems which purport to measure their strength. This is an informal survey of what I "know" about this topic.
 Introduction These are my notes as I try to piece this topic together, rather fitfully, from what sources I have to hand. Beeson Some definitions taken from Michael Beeson Beeson80.
 Tarski/Friedman A definition due to Tarski and used in Friedman's Concept Calculus [FriedmanHarvey]. Pohlers 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.
Introduction
 These are my notes as I try to piece this topic together, rather fitfully, from what sources I have to hand.
 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
 Some definitions taken from Michael Beeson Beeson80.
 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".
Tarski/Friedman
 A definition due to Tarski and used in Friedman's Concept Calculus [FriedmanHarvey].
 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.
Pohlers
 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.
 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.
Large Cardinals
 Proof theoretic strength of strong set theories by measured by large cardinals.