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.

ArKiv Extended Version https://arxiv.org/abs/2311.15003

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.

We extend work of Lautemann, Schwentick and Stewart [Clemens Lautemann et al., 1996] on characterisations of the "positive" polynomial-time predicates (posP, also called mP by Grigni and Sipser [Grigni and Sipser, 1992]) to function classes. Our main result is the obtention of a function algebra for the positive polynomial-time functions (posFP) by imposing a simple uniformity constraint on the bounded recursion operator in Cobham's characterisation of FP. We show that a similar constraint on a function algebra based on safe recursion, in the style of Bellantoni and Cook [Stephen Bellantoni and Stephen A. Cook, 1992], yields an "implicit" characterisation of posFP, mentioning neither explicit bounds nor explicit monotonicity constraints.

Our goal is to approach the classes of computational complexity P, NP, and Pspace in a recursion-theoretic manner. Here we emphasize the connection between the structure of the recursion schemes and the underlying models of computation.

A celebrated contribution of Bellantoni and Cook was a function algebra to capture FPTIME. This algebra uses recursion on notation. Later, Oitavem showed that including primitive recursion, an algebra is obtained that captures FPSPACE. The main results of this article concern variants of the later algebra. First, we show that iteration can replace primitive recursion. Then, we consider the results of imposing a monotonicity constraint on the primitive recursion or iteration. We find that in the case of iteration, the power of the algebra shrinks to FPTIME. More interestingly, with primitive recursion, we obtain a new implicit characterization of the polynomial hierarchy (FPH). The idea to consider these monotonicity constraints arose from the results on write-once tapes for Turing machines. We review this background and also note a new machine characterization of ΔP2, that similarly to our function algebras, arises by combining monotonicity constraints with a known characterization of PSPACE.