Abstract We study numeral forms of completeness and consistency for $\mathsf {S}^1_2$ and other weak theories, like $\mathsf {EA}$. This gives rise to an exploration of the derivability conditions needed to establish the mentioned results; a presentation of a weak form of Gödel’s Second Incompleteness Theorem without using ‘provability implies provable provability’; a provability predicate that satisfies the mentioned derivability condition for weak theories; and a completeness result via consistency statements. Moreover, the paper includes characterizations of the provability predicates for which the numeral results hold, having $\mathsf {EA}$ as the surrounding theory, and results on functions that compute finitist consistency statements.

Abstract This volume is one of two special issues collecting articles by invited speakers of the conference ‘Celebrating 90 Years of Gödel’s Incompleteness Theorems’ held in Nürtingen (Germany) in July 2021. The conference was organized by the Carl Friedrich von Weizsäcker Center at the University of Tübingen with support by the ERC-funded project Gödel Enigma: Rediscovering Kurt Gödel through his unpublished works at the University of Helsinki and by the Kurt Gödel Society in Vienna.

Abstract In this paper, we study the metamathematics of consistent arithmetical theories $T$ (containing $\textsf {I}\varSigma _{1}$); we investigate numerical properties based on proof predicates that depend on numerations of the axioms. Numeral Completeness. For every true (in $\mathbb {N}$) sentence $\vec {Q}\vec {x}.\varphi (\vec {x})$, with $\varphi (\vec {x})$ a $\varSigma _{1}(\textsf {I}\varSigma _1)$-formula, there is a numeration $\tau $ of the axioms of $T$ such that $\textsf {I}\varSigma _1\vdash \vec {Q}\vec {x}. \texttt {Pr}_{\tau }(\ulcorner \varphi (\overset {\text{.} }{\vec {x}})\urcorner )$, where $\texttt {Pr}_{\tau }$ is the provability predicate for the numeration $\tau $. Numeral Consistency. If $T$ is consistent, there is a $\varSigma _{1}(\textsf {I}\varSigma _1)$-numeration $\tau $ of the axioms of $\textsf {I}\varSigma _{1}$ such that $\textsf {I}\varSigma _1\vdash \forall\, x. \texttt {Pr}_{\tau }(\ulcorner \neg \textit {Prf}(\ulcorner \perp \urcorner , \overset {\text{.}}{x})\urcorner )$, where $\textit {Prf}(x,y)$ denotes a $\varDelta _{1}(\textsf {I}\varSigma _1)$-definition of ‘$y$ is a $T$-proof of $x$’. Finitist consistency is addressed by generalizing a result of Artemov: Partial finitism. If $T$ is consistent, there is a primitive recursive function $f$ such that, for all $n\in \mathbb {N}$, $f(n)$ is the code of an $\textsf {I}\varSigma _{1}$-proof of $\neg\, \textit{Prf}(\ulcorner \perp \urcorner ,\overline {n})$. These results are not in conflict with Gödel’s Incompleteness Theorems. Rather, they allow to extend their usual interpretation and show a deep connection to reflections in Hilbert’s last papers of 1931.

Probabilistic complexity classes, despite capturing the notion of feasibility, have escaped any treatment by the tools of so-called implicit-complexity. Their inherently semantic nature is of course a barrier to the characterization of classes like BPP or ZPP, but not all classes are semantic. In this paper, we introduce a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.

Abstract This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories and ; the exact proof-theoretic ordinals of these systems are presented.

We investigate Frege structures as a truth theory over applicative theories in a partial framework. In a first approach we simply ignore undefinedness in the truth definition yielding a theory with total truth. Then we introduce a certain notion of pointer to avoid strictness problems. This approach is closely related to the concept of promises in SCHEME which is used to introduce streams in strict functional programming languages.