Some results on cut-elimination, provable well-orderings, induction and reflection (Q1295413)

The author begins this long paper by saying ``We gather the following miscellaneous results in proof theory from the attic''. This attic must be large and full of stuff. Apparently, in studying other people's papers, ideas, etc., the author came up with his own new, improved, etc. approaches, and kept them in the attic. Among them are the following eight topics. \S 1. A provably well-founded relation in PA can be embedded into an initial segment of \(\varepsilon_0\) by an elementary function. (This improves results of Gentzen, Takeuti, and Harrington.) \S 2. Shortest cut-free proofs in propositional calculus. Here, pruning is applicable, and so the length is bounded by an elementary function. This result in turn, is applied to bounded arithmetic, and various provabilities and non-provabilities are shown. \S 3 is about bar induction; in particular, its relation with reflection schema in \(\omega\)-logic, and with transfinite induction. \S 4 is of a quite different nature; it is about equational calculus. The possibility of direct computations (i.e. without extraneous function symbols) is discussed, and the decidability of inequalities is solved affirmatively. In \S 5, intuitionistic iterated fixed point theories for strongly positive operator forms are shown to be conservative over HA, via interpretation in elementary analysis. \S 6 bears a similar title: classical fixed point theories. But it is about computation of proof-theoretic ordinals, carrying on Kreisel's work of four decades ago. The themes of \S 7 are the equivalence of transfinite induction rule and iterated reflection schema over \(I\Sigma_n\), and that of iterated \(\Pi_2\)-reflection schema and the totality of the fast growing functions over \(I\Sigma_1\) . The final \S 8 is more in computer science, and the author estimates derivation lengths of finite rewriting systems by means of ordinal analysis, slow growing functions, etc. These eight sections are independent of one another, and ample background material is provided. Thus, the author could have made eight short papers.