No label defined (Q4247313)

The proof-theoretic strength \(\alpha\) of a theory is the supremum of all ordinals up to which we can prove transfinite induction in that theory. Whereas for classical theories the main problem is to show that \(\alpha\) is an upper bound for the strength -- this usually means to reduce the theory to a weak theory like primitive recursive arithmetic or Heyting arithmetic extended by transfinite induction up to \(\alpha\), which can be considered to be more constructive than the classical theory itself -- for constructive theories this is in most cases not difficult, since we can easily build a term model in a classical theory of known strength. For constructive theories in general the main problem is to show that \(\alpha\) is a lower bound: that despite the restricted principles available one has a proof-theoretically strong theory. In this article we will concentrate on the direct method for showing that \(\alpha\) is a lower bound, namely well-ordering proofs: to carry out in the theory a sequence of proofs of the well-foundedness of linear orderings of order type \(\alpha_n\), such that \(\sup_{n\in\omega} \alpha_n= \alpha\). Such proofs can be considered to be the logically most complex proofs which one can carry out in the theory; in most cases, in addition to transfinite induction up to \(\alpha_n\) for each \(n\), only primitive recursive arithmetic is needed in order to analyze the theory proof-theoretically and in order to prove the same \(\Pi^0_2\)-sentences. \textit{E. Griffor} and \textit{M. Rathjen} [Arch. Math. Logic 33, No. 5, 347-385 (1994; Zbl 0819.03047)] have used the more indirect method of interpreting theories of known strength in type theory for obtaining lower bounds for the strength of it. Apart from the fact that in the case of one universe and \(W\)-type Griffor and Rathjens' approach did not yield sharp bounds, we believe that the direct method has the advantage of giving a deeper insight into the theory, since one examines the principles of the theory directly without referring to the analysis of another theory, and that the programs obtained by it are of independent interest. For the entire collection see [Zbl 0899.00026].