VARIANTS OF KREISEL’S CONJECTURE ON A NEW NOTION OF PROVABILITY
Paulo Guilherme Santos, Reinhard Kähle · Bulletin of Symbolic Logic · 2021
Abstract Kreisel’s conjecture is the statement: if, for all $n\in \mathbb {N}$ , $\mathop {\text {PA}} olimits \vdash _{k \text { steps}} \varphi (\overline {n})$ , then $\mathop {\text {PA}} olimits \vdash \forall x.\varphi (x)$ . For a theory of arithmeticT, given a recursive functionh, $T \vdash _{\leq h} \varphi $ holds if there is a proof of $\varphi $ inTwhose code is at most $h(\#\varphi )$ . This notion depends on the underlying coding. ${P}^h_T(x)$ is a predicate for $\vdash _{\leq h}$ inT. It is shown that there exist a sentence $\varphi $ and a total recursive functionhsuch that $T\vdash _{\leq h}\mathop {\text {Pr}} olimits _T(\ulcorner \mathop {\text {Pr}} olimits _T(\ulcorner \varphi \urcorner )\rightarrow \varphi \urcorner )$ , but , where $\mathop {\text {Pr}} olimits _T$ stands for the standard provability predicate inT. This statement is related to a conjecture by Montagna. Also variants and weakenings of Kreisel’s conjecture are studied. By the use of reflexion principles, one can obtain a theory $T^h_\Gamma $ that extendsTsuch that a version of Kreisel’s conjecture holds: given a recursive functionhand $\varphi (x)$ a $\Gamma $ -formula (where $\Gamma $ is an arbitrarily fixed class of formulas) such that, for all $n\in \mathbb {N}$ , $T\vdash _{\leq h} \varphi (\overline {n})$ , then $T^h_\Gamma \vdash \forall x.\varphi (x)$ . Derivability conditions are studied for a theory to satisfy the following implication: if , then $T\vdash \forall x.\varphi (x)$ . This corresponds to an arithmetization of Kreisel’s conjecture. It is shown that, for certain theories, there exists a functionhsuch that $\vdash _{k \text { steps}}\ \subseteq\ \vdash _{\leq h}$ .