We define a direct translation from finite rooted trees to finite natural functions which shows that the Worm Principle introduced by Lev Beklemishev is equivalent to a very slight variant of the well-known Kirby-Paris' Hydra Game. We further show that the elements in a reduction sequence of the Worm Principle determine a bad sequence in the well-quasi-ordering of finite sequences of natural numbers with respect to Friedman's gapembeddability. A characterization of gap-embeddability in terms of provability logic due to Lev Beklemishev (...) is also presented. (shrink)

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories (...) whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms. (shrink)

We elaborate Weiermann-style phase transitions for well-partial-orderings (wpo) determined by iterated finite sequences under Higman-Friedman style embedding with Gordeev’s symmetric gap condition. For every d-times iterated wpo \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}\right)}$$\end{document} in question, d > 1, we fix a natural extension of Peano Arithmetic, \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${T \supseteq \sf{PA}}$$\end{document}, that proves the corresponding second-order sentence \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{WPO}\left({\rm (...) S}{\textsc{eq}}^{d}, \trianglelefteq _{d}\right) }$$\end{document}. Having this we consider the following parametrized first-order slow well-partial-ordering sentence \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d}, r\right):}$$\end{document}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\left( \forall K > 0 \right) \left( \exists M > 0\right) \left( \forall x_{0},\ldots,x_{M}\in {\rm S}\text{\textsc{eq}}^{d}\right)$$\end{document}\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\left( \left( \forall i\leq M\right) \left( \left| x_{i}\right| 1}$$\end{document} then \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{d}, \trianglelefteq _{d},r \right) }$$\end{document} is not provable in T.Moreover, by the well-known proof theoretic equivalences we can just as well replace T by PA or ACA0 and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Delta _{1}^{1}\sf{CA}}$$\end{document}, if d = 2 and d = 3, respectively.In the limit case d → ∞ we replaceEFA-provably computable reals r by EFA-provably computable functions \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${f: \mathbb{N} \rightarrow \mathbb{R}_{+}}$$\end{document} and prove analogous theorems. (In the sequel we denote by \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb{R}_{+}}$$\end{document} the set of EFA-provably computable positive reals). In the basic case T = PA we strengthen the basic phase transition result by adding the following static threshold clause\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2}, 1\right)}$$\end{document} is still provable in T = PA (actually in EFA). Furthermore we prove the following dynamic threshold clauses which, loosely speaking are obtained by replacing the static threshold t by slowly growing functions 1α given by \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${1_{\alpha }\left( i\right)\,{:=}\,1+\frac{1}{H_{\alpha }^{-1}\left(i\right) }, H_{\alpha}}$$\end{document} being the familiar fast growing Hardy function and \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${H_{\alpha }^{-1}\left( i\right)\,{:=}\,\rm min \left\{ j \mid H_{\alpha } \left ( j\right) \geq i \right\}}$$\end{document} the corresponding slowly growing inversion. If \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\alpha < \varepsilon _{0}}$$\end{document}, then \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left({\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2}, 1_{\alpha}\right)}$$\end{document} is provable in T = PA. \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\sf{SWP}\left( {\rm S}\text{\textsc{eq}}^{2}, \trianglelefteq _{2},1_{\varepsilon _{0}}\right)}$$\end{document} is not provable in T = PA. We conjecture that this pattern is characteristic for all \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${T\supseteq \sf{PA}}$$\end{document} under consideration and their proof-theoretical ordinals o (T ), instead of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\varepsilon _{0}}$$\end{document}. (shrink)

We introduce the appropriate iterated version of the system of ordinal notations from [G1] whose order type is the familiar Howard ordinal. As in [G1], our ordinal notations are partly inspired by the ideas from [P] where certain crucial properties of the traditional Munich' ordinal notations are isolated and used in the cut-elimination proofs. As compared to the corresponding “impredicative” Munich' ordinal notations (see e.g. [B1, B2, J, Sch1, Sch2, BSch]), our ordinal notations arearbitrary terms in the appropriate simple term (...) algebra based on the notion of collapsing functions (which we would rather identify as projective functions). In Sect. 1 below we define the systems of ordinal notationsPRJ( ), for any primitive recursive limit wellordering . In Sect. 2 we prove the crucial well-foundness property by using the appropriate well-quasi-ordering property of the corresponding binary labeled trees [G3]. In Sect. 3 we interprete inPRJ( ) the familiar Veblen-Bachmann hierarchy of ordinal functions, and in Sect. 4 we show that the corresponding Buchholz's system of ordinal notationsOT( ) is a proper subsystem ofPRJ( ), although it has the same order type according to [G3] together with the interpretation from Sect. 2 in the terms of labeled trees. In Sect. 5 we use Friedman's approach in order to obtain an appropriate purely combinatorial statement which is not provable in the theory of iterated inductive definitions ID< λ, for arbitrarily large limit ordinalλ. Formal theories, axioms, etc. used below are familiar in the proof theory of subsystems of analysis (see [BFPS, T, BSch]). (shrink)