Fix a $\Sigma_1$-sound theory $\mathcal{T}$ containing basic (Robinson) arithmetic.

On the one hand, by diagonalizing over the provably total computable functions in $\mathcal{T}$, we can construct a computable function whose totality (well-definedness on all inputs) is not provable in $\mathcal{T}$.

On the other hand, for any computable function $f$, the well-definedness of $f$ on inputs up to any given $n \in \mathbb{N}$ is provable in $\mathcal{T}$. But the proof, in general, grows with $n$ almost as fast as $f$ itself.

It's therefore interesting to consider which functions $f$ are "barely unprovable" in $\mathcal{T}$: that is, within $\mathcal{T}$, the totality of $f$ is not provable, but its well-definedness on inputs up to $n \in \mathbb{N}$ has a proof that grows slowly (polynomially or even linearly) with $n$.

For example, if we're allowed to duplicate / reuse variables, then double exponential functions are barely unprovable in Robinson arithmetic. (Otherwise, only single exponential functions are.) Unlike provably total functions, barely-unprovable ones are not closed under composition. Situations where we want to consider single or double exponentials but not higher elemementary functions seem reasonably common, in some sense precisely because they are barely unprovable using basic arithmetic without induction: e.g. to talk about nodes or subtrees in a fixed-valence tree of height $n$ requires $O(n)$ symbols.

My question is simply whether this notion is discussed at all in the literature, and if so what are some typical or interesting applications (ideally with sources).

  • $\begingroup$ I don't understand your second paragraph. First of all, it seems to assume $\mathcal{T}$ is consistent (else $\mathcal{T}$ can prove anything). More importantly, how can you apply a diagonalisation argument to the partial recursive functions that $\mathcal{T}$ can prove are actually total to get a total recursive function? $\endgroup$
    – Rob Arthan
    Commented Apr 2, 2021 at 20:28
  • $\begingroup$ Right, I'm assuming $\mathcal{T}$ is consistent (it can be $\Pi_2$-sound if need be). As for the diagonalization, my thought was to arrange the proofs of totality in lexicographic order and then define a new function whose value at $n$ is 1 more than the value of the function that the $n$th proof is about. Have I overlooked something? $\endgroup$ Commented Apr 2, 2021 at 23:38
  • $\begingroup$ I think actually $\Pi_2$-soundness (equivalently, $\Sigma_1$-soundness) is necessary, so I've added that in. $\endgroup$ Commented Apr 3, 2021 at 4:19
  • $\begingroup$ I think your ideas about the diagonalisation argument are right. Thanks for the clarification. $\endgroup$
    – Rob Arthan
    Commented Apr 3, 2021 at 22:38


You must log in to answer this question.