On the Notions of Rudimentarity, Primitive Recursivity and Representability of Functions and Relations

TL;DR

This paper clarifies the relationships between rudimentary, primitive recursive, and representable functions and relations, providing new proofs and insights to resolve common misunderstandings in mathematical logic.

Contribution

It offers a simple proof that some primitive recursive relations are not rudimentary and establishes the equivalence of weak and strong representability in arithmetical theories.

Findings

Primitive recursive relations are not all rudimentary.

Weak and strong representability are equivalent in strong arithmetical theories.

Provides clearer understanding of function and relation notions in logic.

Abstract

It is quite well-known from Kurt Godel's (1931) ground-breaking result on the Incompleteness Theorem that rudimentary relations (i.e., those definable by bounded formulae) are primitive recursive, and that primitive recursive functions are representable in sufficiently strong arithmetical theories. It is also known, though perhaps not as well-known as the former one, that some primitive recursive relations are not rudimentary. We present a simple and elementary proof of this fact in the first part of the paper. In the second part, we review some possible notions of representability of functions studied in the literature, and give a new proof of the equivalence of the weak representability with the (strong) representability of functions in sufficiently strong arithmetical theories. Our results shed some new light on the notions of rudimentary, primitive recursive, and representable functions and relations, and clarify, hopefully, some misunderstandings and confusing errors in the literature.

Equations

$${\Gamma }_f=\{(x,y)\in X\times Y\mid y=f(x)\}.$$

$$\eta(x,y)=\big{[}\exists!z\,\theta(x,z)\wedge\theta(x,y)\big{]}\vee\big{[}\neg\exists!z\,\theta(x,z)\wedge y\!=\!0\big{]}.$$

Full text

2010 AMS Subject Classification: 03F40 $\cdot$ 03D20 $\cdot$ 03F30.

Keywords: bounded formula $\cdot$ the incompleteness theorem $\cdot$ primitive recursive functions / relations $\cdot$ rudimentary relations $\cdot$ representability.

1 Introduction and Preliminaries

Primitive recursive functions are what were called “rekursiv” by Kurt Gödel in his seminal 1931 paper [6, 7] where he proved the celebrated incompleteness theorem. The main features of the primitive recursive functions used by Gödel were the following:

They are computable (i.e., for each primitive recursive function there exists an algorithm that computes it). However, we now know that they do not make up the whole (intuitively) computable functions (from tuples of natural numbers to natural numbers, $\mathbb{N}^{k}\rightarrow\mathbb{N}$). So, “rekursiv” functions are now called “primitive recursive” functions, which constitute a sub-class of recursive functions that are believed to constitute the whole computable functions. 2. 2.

They are representable in (sufficiently expressive and sufficiently strong) formal arithmetical theories. It is now known that, more generally, (only) recursive functions are representable in (all the) recursively enumerable, sufficiently strong and sufficiently expressive theories (see Section 3 below). 3. 3.

Theories whose set of axioms are primitive recursive and extend a base theory (such as Robinson’s Arithmetic Q), are incomplete. It was later found out that this holds more generally for recursively enumerable extensions of Q. Also, by William Craig’s Trick, every such theory is equivalent with another theory whose set of axioms is rudimentary (i.e., definable by a bounded formula).

Even though one can set up the whole theory of computable functions (aka recursion theory) and the incompleteness theorems without introducing the notion of primitive recursive functions (and relations), the theory of primitive recursive functions is a main topic in the literature on recursive function theory and the incompleteness theorems. For the sake of completeness we review some basic notions of this theory.

Definition** 1.1**** (Primitive Recursive Functions)**

The class of primitive recursive (pr) functions is the smallest class that contains the initial functions

(i) the constant zero function $\boldsymbol{\zeta}\colon\mathbb{N}\rightarrow\mathbb{N},\,\boldsymbol{\zeta}(x)\!=\!0$,

(ii) the successor function $\boldsymbol{\sigma}\colon\mathbb{N}\rightarrow\mathbb{N},\,\boldsymbol{\sigma}(x)\!=\!x\!+\!1$, and

(iii) the projection functions $\boldsymbol{\pi}_{i}^{n}\colon\mathbb{N}^{n}\rightarrow\mathbb{N},\,\boldsymbol{\pi}_{i}^{n}(x_{1},\cdots,x_{n})\!=\!x_{i}$, for

any $n\geqslant 1$ where $i\in\{1,\cdots,n\}$;

and is closed under

(I) composition of functions, i.e., contains the function $h\colon\mathbb{N}^{n}\rightarrow\mathbb{N}$, if it already contains the functions $g_{1},\cdots,g_{m}\colon\mathbb{N}^{n}\rightarrow\mathbb{N}$ and $f\colon\mathbb{N}^{m}\rightarrow\mathbb{N}$, where h(x_{1},\cdots,x_{n})\!=\!f\big{(}g_{1}(x_{1},\ldots,x_{n}),\cdots,g_{m}(x_{1},\cdots,x_{n})\big{)}, and

(II) primitive recursion, i.e., contains the function $h\colon\mathbb{N}^{n+1}\rightarrow\mathbb{N}$, if it already contains the functions $f\colon\mathbb{N}^{n}\rightarrow\mathbb{N}$ and $g\colon\mathbb{N}^{n+2}\rightarrow\mathbb{N}$, where $h\colon\mathbb{N}^{n+1}\rightarrow\mathbb{N}$ is inductively defined by

\begin{cases}h(x_{1},\cdots,x_{n},0)\!=\!f(x_{1},\cdots,x_{n}),&\\ h(x_{1},\cdots,x_{n},x\!+\!1)\!=\!g\big{(}h(x_{1},\cdots,x_{n},x),x_{1},\cdots,x_{n},x\big{)}.&\end{cases}

✧

By Hermann Grassmann’s recursive definition of addition and multiplication, it can be shown that these functions ($+\!\colon\!\mathbb{N}^{2}\rightarrow\mathbb{N},(x,y)\mapsto x\!+\!y$ and $\times\!\colon\!\mathbb{N}^{2}\rightarrow\mathbb{N},(x,y)\mapsto x\!\cdot\!y$) are pr; so are the following sign functions are primitive recursive:

${\sf sg}(x)=\begin{cases}0&\mbox{ if }\ x\!=\!0,\\ 1&\mbox{ if }\ x\!\neq\!0,\end{cases}$   and   $\widetilde{\sf sg}(x)=\begin{cases}1&\mbox{ if }\ x\!=\!0,\\ 0&\mbox{ if }\ x\!\neq\!0.\end{cases}$

Definition** 1.2**** (Primitive Recursive Relations)**

The characteristic function of a relation $R\!\subseteq\!\mathbb{N}^{n}$ is $\boldsymbol{\chi}_{R}\colon\mathbb{N}^{n}\rightarrow\{0,1\}$, $\boldsymbol{\chi}_{R}(x_{1},\cdots,x_{n})=\begin{cases}1&\mbox{ if }(x_{1},\cdots,x_{n})\in R,\\ 0&\mbox{ if }(x_{1},\cdots,x_{n})\not\in R.\end{cases}$

A relation is called primitive recursive (pr), if its characteristic function is primitive recursive.

• ✧*

For example, the equality ($=$) and inequality ($\leqslant$) can be shown to be pr relations. The following identities show that the class of pr relations is closed under Boolean operations and bounded quantifications:

$\boldsymbol{\chi}_{R\cap S}\!=\!\boldsymbol{\chi}_{R}\cdot\boldsymbol{\chi}_{S};\quad\boldsymbol{\chi}_{R^{\complement}}\!=\!\widetilde{\sf sg}(\boldsymbol{\chi}_{R});\quad\boldsymbol{\chi}_{R\cup S}\!=\!{\sf sg}(\boldsymbol{\chi}_{R}\!+\!\boldsymbol{\chi}_{S});$

$\begin{cases}\boldsymbol{\chi}_{\forall x\leqslant\alpha R(\vec{z},x)}(\vec{z},0)\!=\!\boldsymbol{\chi}_{R}(\vec{z},0),&\\ \boldsymbol{\chi}_{\forall x\leqslant\alpha R(\vec{z},x)}(\vec{z},\alpha\!+\!1)\!=\!\boldsymbol{\chi}_{\forall x\leqslant\alpha R(\vec{z},x)}(\vec{z},\alpha)\cdot\boldsymbol{\chi}_{R}(\vec{z},\alpha\!+\!1);&\end{cases}$

\begin{cases}\boldsymbol{\chi}_{\exists x\leqslant\alpha R(\vec{z},x)}(\vec{z},0)\!=\!\boldsymbol{\chi}_{R}(\vec{z},0),&\\ \boldsymbol{\chi}_{\exists x\leqslant\alpha R(\vec{z},x)}(\vec{z},\alpha\!+\!1)\!=\!{\sf sg}\big{(}\boldsymbol{\chi}_{\forall x\leqslant\alpha\,P(\vec{z},x)}(\vec{z},\alpha)\!+\!\boldsymbol{\chi}_{P}(\vec{z},\alpha\!+\!1)\big{)}.&\end{cases}

Definition** 1.3**** (Rudimentary Relations)**

A formula in the language of arithmetic $\langle 0,1,+,\times,\leqslant\rangle$ is called bounded, if it has been constructed from atomic formulas (of the form $t\!=\!s$ or $t\!\leqslant\!s$, for terms $s,t$) by means of negation, conjunction, disjunction, implication, and bounded quantifications (of the form $\forall x\!\leqslant\!t$ or $\exists x\!\leqslant\!t$, where the formula $\forall x\!\leqslant\!t\,\mathcal{A}(x,t)$ abbreviates \forall x\big{[}x\!\leqslant\!t\rightarrow\mathcal{A}(x,t)\big{]} and $\exists x\!\leqslant\!t\,\mathcal{A}(x,t)$ is an abbreviation for \exists x\big{[}x\!\leqslant\!t\wedge\mathcal{A}(x,t)\big{]} for term $t$ and variable $x$ which is not free in $t$).

The class of bounded formulas is denoted by $\Delta_{0}$.

A relation $R\subseteq\mathbb{N}^{n}$ is called rudimentary or bounded definable, or simply $\Delta_{0}$, if it can be defined by a $\Delta_{0}$-formula, i.e., there exists a $\Delta_{0}$-formula $\varphi(x_{1},\cdots,x_{n})$ such that $R=\{(x_{1},\cdots,x_{n})\mid\mathbb{N}\models\varphi(x_{1},\cdots,x_{n})\}$.

• ✧*

The above arguments show that all the $\Delta_{0}$ relations are pr; see also e.g. [3, 9, 18]. The question as to whether the converse holds, i.e., whether every pr relation is $\Delta_{0}$, has been mentioned in very few places. Unfortunately, as will be indicated, some of them are wrong or misleading:

• (1)

On page 315 of [9] we read: “A relation is primitive recursive if and only if it is definable by a $\Delta_{0}$ formula. We presently prove one direction of this fact. The other direction shall become apparent after Section 8.3 of the next chapter and is left as Exercise 8.6.”

This leaves the reader wondering what (theorems or techniques) will be provided in Chapter 8 (the incompleteness theorems) of the book [9] that will enable the reader to show that every pr relation is rudimentary, i.e., $\Delta_{0}$ definable. The fact of the matter is that, as will be seen below, it is not true that every pr relation is $\Delta_{0}$.

• (2)

On page 239 of [18] we read as Remark 1, “Induction on the $\Delta_{0}$-formulas readily shows that all $\Delta_{0}$-predicates are p.r. The converse does not hold; an example is the graph of the very rapidly growing hyperexponentiation, recursively defined by ${\rm hex}(a,0)\!=\!1$ and ${\rm hex}(a,Sb)\!=\!a^{{\rm hex}(a,b)}$.”

The graph of a function $f\colon X\rightarrow Y$ is, by definition, the relation

[TABLE]

Let us note that the graph $\Gamma_{f}$ of a pr function $f$ is a pr relation, since $\boldsymbol{\chi}_{\Gamma_{f}}(\vec{a},b)\!=\!\boldsymbol{\chi}_{=}(f(\vec{a}),b)$. Now, ${\rm hex}$ is a pr function, and so its graph is a pr relation. But the claim that this relation is not $\Delta_{0}$ has not been proved in [18]. In fact, it has been shown in [1] (see also [5]) that this is not true: the graph of ${\rm hex}$ is actually $\Delta_{0}$.

• (3)

We read in the Abstract of [5], “The question of whether a given primitive recursive relation is rudimentary is in some cases difficult and related to several well-known open questions in theoretical computer science”. Also, on page 130 of [5] we read, “However, it is difficult to exhibit a natural arithmetical relation which can be proved not to be rudimentary” (emphasize in the original) and that “This paper is an attempt to systemize … proving that various primitive recursive relations are rudimentary”. Later, on page 132 we read, “Hence, the main way of exhibiting a primitive recursive relation which is not rudimentary is to choose it in $\textswab{C}^{3}_{\ast}\setminus\textswab{C}^{2}_{\ast}$. Although it is true that infinitely many [such] relations exist, we know no natural example”. Here, by “natural” the authors mean a relation ($\subseteq\mathbb{N}^{k}$) that the number-theorists use and work with.

• (4)

On page 85 of [3] after proving that “Every $\Delta_{0}$ relation is primitive recursive” as a Lemma, we read, “Remark: The converse of the above lemma is false, as can be shown by a diagonal argument. For those familiar with complexity theory, we can clarify things as follows. As noted in the Side Remark above, all $\Delta_{0}$ relations can be recognized in linear space on a Turing machine. On the other hand, it follows from the Ritchie-Cobham Theorem that all relations recognizable in space bounded by a primitive recursive function of the input length are primitive recursive. In particular, space ${\rm O}(n^{2})$ relations are primitive recursive, and a straightforward diagonal argument shows that there are relations recognizable in $n^{2}$ space which are not recognizable in linear space, and hence are not $\Delta_{0}$ relations.”

The mentioned side-remark (that “All $\Delta_{0}$ relations can be recognized in linear space on a Turing machine, when input numbers are represented in binary notation”) has not been proved in [3]. This was proved first by J. R. Myhill in [15].

So, there should exist some pr relations that are not $\Delta_{0}$. In Section 2 we will show that a specific pr relation is not $\Delta_{0}$, by a carefully detailed proof with little background in complexity theory or formal arithmetics. This relation may not look natural for number-theorists, but is sufficiently natural for logicians.

In the second part, Section 3, we will study some possible notions of representability of functions and relations in arithmetical theories and will compare their strength with each other; we will provide a new proof for an old theorem which appears in a very few places with a much longer proof. The theorem says that every weakly representable function is (strongly) representable; this is usually proved by showing that (A) every weakly representable function is recursive, and (B) every recursive function is (strongly) representable. Our proof is direct and elementary.

2 Rudimentarity vs. Primitive Recursivity

Let us be given a fixed Gödel coding $\alpha\mapsto\ulcorner\!\alpha\!\urcorner$, which is primitive recursive (as is usually presented in the literature). Our example of a pr relation that is not $\Delta_{0}$, uses an idea of Alfred Tarski; that the truth relation of arithmetical sentences is not arithmetically definable. Likewise, the truth of $\Delta_{0}$-sentences is not $\Delta_{0}$; but, as will be shown later, it is pr.

Definition** 2.1**** ($\Delta_{0}$-Satisfaction)**

Let ${\tt Sat}_{\Delta_{0}}$ be the set of all the ordered pairs $(\ulcorner\!\theta(\vec{\nu})\!\urcorner,a)$, where $\theta(\vec{\nu})$ is a $\Delta_{0}$-formula with the shown free variables and $a\!\in\!\mathbb{N}$, such that $\mathbb{N}\vDash\theta(\vec{a})$; i.e., the sentence resulted from substituting $a$ for every free variable of $\theta$ is true (in the standard model of natural numbers).

• ✧*

In the other words, ${\tt Sat}_{\Delta_{0}}=\{(\ulcorner\!\theta(\vec{\nu})\!\urcorner,a)\mid\mathbb{N}\!\vDash\!\theta(\vec{a})\;\&\;\theta\!\in\!\Delta_{0}\}.$

Theorem** 2.2**** (Non-Rudimentarity of $\Delta_{0}$-Satisfaction)**

The relation ${\tt Sat}_{\Delta_{0}}(x,y)$ is not definable by any $\Delta_{0}$-formula.

Proof:

If a $\Delta_{0}$-formula such as $\boldsymbol{\varsigma}(x,y)$ defines the relation ${\tt Sat}_{\Delta_{0}}$, then for the formula $\theta(x)\!=\!\boldsymbol{\neg}\boldsymbol{\varsigma}(x,x)$ (which is $\Delta_{0}$) and number $m\!=\!\ulcorner\!\theta(x)\!\urcorner$, we have $\mathbb{N}\vDash\theta(m)\!\equiv\!{\tt Sat}_{\Delta_{0}}(\ulcorner\theta(x)\urcorner,m)\!\equiv\!\boldsymbol{\varsigma}(m,m)\!\equiv\!\boldsymbol{\neg}\theta(m)$, a contradiction! ❑

In the rest of this section, we show that ${\tt Sat}_{\Delta_{0}}$ is a pr relation. This can already be inferred from the results of [13]; see also [2, Definition 4.1.3 and Lemma 4.1.4] and [17, Theorem 2] and [8, Corollary 5.5]. All of them use advanced arguments that cannot be mentioned in more elementary texts like [3, 9, 18]. Our aim here is to provide an elementary proof for primitive recursivity of ${\tt Sat}_{\Delta_{0}}$ in such a way that it can be used, along with Theorem 2.2, in textbooks for clarifying the status of pr vs. $\Delta_{0}$ relations.

Remark** 2.3**** (On Gödel Coding)**

We can assume that the set of the Gödel codes of the variables is definable by a $\Delta_{0}$-formula; for example we can keep even numbers $2,4,6,\cdots$ for coding the variables $v_{0},v_{1},v_{2},\cdots$ respectively, and then code the rest of the language (propositional connectives, quantifiers, parentheses and function and relation symbols) by odd numbers. As a result of this way of coding, ${\tt var}(x)\!\equiv\!\exists y\!\leqslant\!x\,(y\!=\!2x\!+\!2)$ is a $\Delta_{0}$-formula that defines the variables. Other syntactical notions of terms, formulas, sentences, bounded sentences, proofs, etc. can be shown to be pr as usual (see e.g. [8, 9, 14, 18]). Let $\mathfrak{p}_{0},\mathfrak{p}_{1},\mathfrak{p}_{2},\cdots$ be the sequence of all prime numbers ($2,3,5,\cdots$). Let us code the sequence $\langle\alpha_{0},\alpha_{1},\cdots,\alpha_{k}\rangle$ by the number $\prod_{i\leqslant k}\mathfrak{p}_{i}^{\alpha_{i}+1}$. Let us note that this way, the code of any such sequence will be non-greater than $\mathfrak{p}_{k}^{kA}$, where $A$ is any number greater than all $\alpha_{i}$’s. Also let us recall that the functions $i\mapsto\mathfrak{p}_{i}$ and $(k,A)\mapsto\mathfrak{p}_{k}^{kA}$ are both pr (see e.g. [9, 14, 18]).

• ✧*

Definition** 2.4**** (Terms, Bounded Formulas, Valuations, etc.)**

For a fixed Gödel coding, let the relation

• •

${\tt var}(x)$ hold, when “$x$ is (the Gödel code of) a variable”.

• •

${\tt trm}(x)$ hold, when “$x$ is (the Gödel code of) a term”.

• •

${\tt atm}(x)$ hold, when “$x$ is (the Gödel code of) an atomic formula”.

• •

${\tt fml}_{\Delta_{0}}(x)$ hold, when “$x$ is (the Gödel code of) a $\Delta_{0}$-formula”.

• •

${\tt val}(x,y,z)$ hold, when “$x$ is (the Gödel code of) a term with the free variables $\langle\nu_{0},\cdots,\nu_{\ell}\rangle$, $y$ is (the Gödel code of) a sequence of numbers $\langle a_{0},\cdots,a_{\ell}\rangle$, and $z$ is the value of the term $x$ when each $\nu_{i}$ is substituted with $a_{i}$, for $i\!\leqslant\!\ell$”. ✧

Lemma** 2.5**** (${\tt var}$, ${\tt trm}$, ${\tt fml}_{\Delta_{0}}$ and ${\tt val}$ are pr)**

The relations ${\tt var}$, ${\tt trm}$, ${\tt atm}$, ${\tt fml}_{\Delta_{0}}$ and ${\tt val}$ are pr.

Proof:

We already noted (in Remark 2.3) that the ${\tt var}$ relation can even be $\Delta_{0}$ (and so it is a pr relation) by a modest convention on coding. There is also a $\Delta_{0}$ relation ${\tt seq}(x)$ which holds of $x$ when $x$ is (the Gödel code of) a sequence. Let $\ell en(x)$ denote the length of $x$ and $[x]_{i}$, for each $i\!<\!\ell en(x)$, denote the $i$-th element of $x$. Thus, if ${\tt seq}(x)$ holds, then $x$ codes the sequence $\langle[x]_{0},[x]_{1},\cdots,[x]_{\ell en(x)-1}\rangle$. Let us recall that $x\mapsto\ell en(x)$ and $(i,x)\mapsto[x]_{i}$ are both pr functions. Let $y\!=\!\ell ast(x)$ abbreviate $y\!=\![x]_{\ell en(x)-1}$.

${}^{{}_{\bullet}}$ Let ${\tt trmseq}(x)$ be the following $\Delta_{0}$ relation:

{\tt seq}(x)\wedge\forall i\!<\!\ell en(x)\Big{[}[x]_{i}\!=\!\ulcorner 0\urcorner\vee[x]_{i}\!=\!\ulcorner 1\urcorner\vee{\tt var}([x]_{i})\;\vee

\exists j,k\!<\!i\Big{(}[x]_{i}\!=\!\ulcorner\!([x]_{j}\!+\![x]_{k})\!\urcorner\vee[x]_{i}\!=\ulcorner\!([x]_{j}\!\times\![x]_{k})\!\urcorner\Big{)}\Big{]}.

Now, ${\tt trm}(x)$ can be written as $\exists s\!\leqslant\!\mathfrak{p}_{x}^{(x+1)^{2}}{\tt trmseq}(s)\wedge\ell ast(s)\!=\!x$; noting that the building sequence of a term $x$ has length at most $x$ and all the elements of that sequence are non-greater than $x$. So, ${\tt trm}(x)$ is pr.

${}^{{}_{\bullet}}$ That ${\tt atm}(x)$ is a pr relation, follows from the following:

{\tt atm}(x)\!\equiv\!\exists u,v\!<\!x\big{[}{\tt trm}(u)\wedge{\tt trm}(v)\wedge\big{(}x\!=\!\ulcorner\!(u\!=\!v)\!\urcorner\vee x\!=\!\ulcorner\!(u\!\leqslant\!v)\!\urcorner\big{)}\big{]}.

${}^{{}_{\bullet}}$ Without loss of generality we can assume that the propositional connectives are only $\neg$ and $\rightarrow$ and the only quantifier is $\forall$. Now, the following $\Delta_{0}$-formula defines the building sequence of a bounded formula:

{\tt fml}_{\Delta_{0}}{\tt seq}(x)\!\equiv\!{\tt seq}(x)\wedge\forall i\!<\!\ell en(x)\Big{[}{\tt atm}([x]_{i})\vee

\exists j,k\!<\!i\Big{(}[x]_{i}\!=\!\ulcorner\!(\neg[x]_{j})\!\urcorner\vee[x]_{i}\!=\!\ulcorner\!([x]_{j}\!\rightarrow\![x]_{k})\!\urcorner\vee

\exists v,t\!<\!x\big{[}{\tt var}(v)\wedge{\tt trm}(t)\wedge[x]_{i}\!=\!\ulcorner\!(\forall v\!\leqslant\!t)[x]_{j}\!\urcorner\big{]}\Big{)}\Big{]}.

So, ${\tt fml}_{\Delta_{0}}(x)\!\equiv\!\exists s\!\leqslant\!\mathfrak{p}_{x}^{(x+1)^{2}}{\tt fml}_{\Delta_{0}}{\tt seq}(s)\wedge\ell ast(s)\!=\!x$ is a pr relation.

${}^{{}_{\bullet}}$ Let ${\tt valseq}(y,s,t)$ be the following $\Delta_{0}$ relation:

{\tt seq}(y)\wedge{\tt termseq}(s)\wedge{\tt seq}(t)\wedge\ell en(t)\!=\!\ell en(s)\,\wedge\forall i\!<\!\ell en(s)\Big{[}

\big{(}[s]_{i}\!=\!\ulcorner 0\urcorner\wedge[t]_{i}\!=\!0\big{)}\vee\big{(}[s]_{i}\!=\!\ulcorner 1\urcorner\wedge[t]_{i}\!=\!1\big{)}\vee\big{(}{\tt var}([s]_{i})\wedge[t]_{i}\!=\![y]_{i}\big{)}\vee

\exists j,k\!<\!i\big{[}\big{(}[s]_{i}\!=\!\ulcorner\!([s]_{j}\!+\![s]_{k})\!\urcorner\wedge[t]_{i}\!=\![t]_{j}\!+\![t]_{k}\big{)}\vee

\big{(}[s]_{i}\!=\!\ulcorner\!([s]_{j}\!\times\![s]_{k})\!\urcorner\wedge[t]_{i}\!=\![t]_{j}\!\cdot\![t]_{k}\big{)}\big{]}\Big{]},

which states that $y,t$ are (the Gödel code of) sequences (of numbers) and $s$ is (the Gödel code of) a building sequence of a term such that $t$ is the result of substituting the variables of $s$ with the corresponding elements of $y$. Finally, ${\tt val}(x,y,z)$ is pr since it is equivalent with

$\exists s\!\leqslant\!\mathfrak{p}_{x}^{(x+1)^{2}}\exists t\!\leqslant\!\mathfrak{p}_{z}^{(z+1)^{2}}{\tt valseq}(y,s,t)\wedge\ell ast(s)\!=\!x\wedge\ell ast(t)\!=\!z$. ❑

Remark** 2.6**** (${\tt Sat}_{\Delta_{0}}$ In the Border of pr and $\Delta_{0}$)**

The main idea of the proofs of Lemma 2.5 and Theorem 2.7 are from [11, Chapter 9]. Actually, by the techniques of [8, Chapter V] one can show that all the relations ${\tt var}(x)$, ${\tt trm}(x)$, ${\tt atm}(x)$, ${\tt fml}_{\Delta_{0}}(x)$ and ${\tt val}(x,y,z)$ can be $\Delta_{0}$, under a suitable Gödel coding. In Theorem 2.7 we will show that ${\tt Sat}_{\Delta_{0}}(x,y)$ is a pr relation, which, by Theorem 2.2, cannot be $\Delta_{0}$ under any Gödel coding. We will see in the proof of Theorem 2.7 that ${\tt Sat}_{\Delta_{0}}$ is definable by the relations ${\tt var}$, ${\tt trm}$, ${\tt atm}$, ${\tt fml}_{\Delta_{0}}$ and ${\tt val}$. So, we have a boundary result here: the pr relations ${\tt var}(x)$, ${\tt trm}(x)$, ${\tt atm}(x)$, ${\tt fml}_{\Delta_{0}}(x)$ and ${\tt val}(x,y,z)$ all can be $\Delta_{0}$ under some Gödel coding, while the pr relation ${\tt Sat}_{\Delta_{0}}(x,y)$ can never be $\Delta_{0}$.

• ✧*

Theorem** 2.7**** (${\tt Sat}_{\Delta_{0}}$ is a pr Relation)**

The relation ${\tt Sat}_{\Delta_{0}}(x,y)$ is pr.

Proof:

Define the relation ${\tt sat}_{\Delta_{0}}{\tt seq}(s,t)$ by “$s$ is a building sequence of a $\Delta_{0}$-formula, and $t$ is a sequence of triples $\langle i,z,w\rangle$ in which $i\!<\!\ell en(s)$ and $w\!\leqslant\!1$ is a truth value ($1$ for truth and [math] for falsity) of the formula $[s]_{i}$ when the variables $v_{0},v_{1},\cdots$ are interpreted by $[z]_{0},[z]_{1},\cdots$ respectively”. Let $z[r/k]$ denote the sequence resulted from $z$ by substituting its $k$-th element with $r$. The function $z,r,k\mapsto z[r/k]$ is pr, and when ${\tt val}(u,z,x)$ holds, then we can have ${\tt val}(u,z,x)$ for some $x\!\leqslant\!\mathfrak{p}_{u}^{z^{u}+1}$, since the value of a term $u$ when its free variables are substituted by the elements of $z$ is non-greater than $\mathfrak{p}_{u}^{z^{u}+1}$. Now, ${\tt sat}_{\Delta_{0}}{\tt seq}(s,t)$ is pr since it is defined by:

${\tt fml}_{\Delta_{0}}{\tt seq}(s)\wedge{\tt seq}(t)\wedge\forall l\!<\!\ell en(t)\,\exists i,z,w\!\leqslant\!t$

\Big{[}[t]_{l}\!=\!\langle i,z,w\rangle\wedge i\!<\!\ell en(s)\wedge w\!\leqslant\!1\,\wedge

\Big{(}\big{[}\exists u,v\!\leqslant\!s\big{(}{\tt trm}(u)\wedge{\tt trm}(v)\wedge[s]_{i}\!=\!\ulcorner\!(u\!=\!v)\!\urcorner\,\wedge

[w=1\leftrightarrow\exists x\!\leqslant\!\mathfrak{p}_{u+v}^{(z^{u+v}+1)^{2}}{\tt val}(u,z,x)\wedge{\tt val}(v,z,x)]\big{)}\big{]}\vee

\big{[}\exists u,v\!\leqslant\!s\big{(}{\tt trm}(u)\wedge{\tt trm}(v)\wedge[s]_{i}\!=\!\ulcorner\!(u\!\leqslant\!v)\!\urcorner\,\wedge

[w=1\leftrightarrow\exists x,y\!\leqslant\!\mathfrak{p}_{u+v}^{(z^{u+v}+1)^{2}}{\tt val}(u,z,x)\wedge{\tt val}(v,z,y)\wedge x\!\leqslant\!y]\big{)}\big{]}\vee

\big{[}\exists j\!<\!i\big{(}[s]_{i}\!=\!\ulcorner\!(\neg[s]_{j})\!\urcorner\,\wedge\exists p\!<\!l\exists w^{\prime}\!\leqslant\!1([t]_{p}\!=\!\langle j,z,w^{\prime}\rangle\;\wedge

[w\!=\!1\leftrightarrow w^{\prime}\!=\!0])\big{)}\big{]}\vee

\big{[}\exists j,k\!<\!i\big{(}[s]_{i}\!=\!\ulcorner\!([s]_{j}\rightarrow[s]_{k})\!\urcorner\,\wedge\exists p,q\!<\!l\exists w^{\prime},w^{\prime\prime}\!\leqslant\!1

([t]_{p}\!=\!\langle j,z,w^{\prime}\rangle\wedge[t]_{q}\!=\!\langle k,z,w^{\prime\prime}\rangle\wedge[w\!=\!1\leftrightarrow w^{\prime}\!=\!0\vee w^{\prime\prime}\!=\!1])\big{)}\big{]}\vee

\big{[}\exists j\!<\!i\exists u,v\!<\!s\big{(}{\tt trm}(u)\wedge{\tt var}(v)\wedge[s]_{i}\!=\!\ulcorner\!(\forall v\!\leqslant\!u)[s]_{j}\!\urcorner\wedge\exists x\!\leqslant\!\mathfrak{p}_{u}^{z^{u}+1}

$[{\tt val}(u,z,x)\wedge\forall r\!\leqslant\!x\exists p\!<\!l\exists w^{\prime}\!\leqslant\!1([t]_{p}\!=\!\langle j,z[r/\ulcorner\!v\!\urcorner],w^{\prime}\rangle)]\wedge$

[w\!=\!1\leftrightarrow\forall r\!\leqslant\!x\exists p\!<\!l\exists w^{\prime}\!\leqslant\!1([t]_{p}\!=\!\langle j,z[r/\ulcorner\!v\!\urcorner],1\rangle]\big{)}\big{]}\Big{)}\Big{]}.

As a result, ${\tt Sat}_{\Delta_{0}}(x,y)$ is pr too, since it be written as

\exists s\!\leqslant\!\mathfrak{p}_{x}^{(x+1)^{2}}\exists t\!\leqslant\!\mathfrak{p}_{x^{2}}^{2^{\mathfrak{p}_{x}^{(x+1)^{2}}}\cdot 3^{\mathfrak{p}_{x}^{\mathfrak{p}_{x}^{(y+1)^{2}}}}\cdot 5}\Big{[}{\tt sat}_{\Delta_{0}}{\tt seq}(s,t)\wedge\ell ast(s)\!=\!x\wedge\ell ast(t)\!=\!\langle\ell en(s)\!-\!1,y,1\rangle\Big{]}.

Note that we took $\neg,\rightarrow$ and $\forall$ as the only logical connectives and we coded $\langle i,z,w\rangle$ as $2^{i}\cdot 3^{z}\cdot 5^{w}$ which imply the desired pr bounds. ❑

3 Representability in Arithmetical Theories

A (most) natural definition for representability of a relation on the natural numbers in a theory, whose language contains terms $\overline{n}$ indicating each natural number $n\!\in\!\mathbb{N}$, is the following:

Definition** 3.1**** (Weak Representability of Relations)**

A relation $R\subseteq\mathbb{N}$ is weakly representable in a theory $T$, if for some formula $\varphi(x)$ the equivalence $R(n)\iff T\vdash\varphi(\overline{n})$ holds for every $n\in\mathbb{N}$.

• ✧*

However, the following stronger definition is usually used in the literature on the incompleteness theorem:

Definition** 3.2**** (Representability of Relations)**

A relation $R\subseteq\mathbb{N}$ is representable in a theory $T$, if for some formula $\varphi(x)$ the implications $R(n)\Longrightarrow T\vdash\varphi(\overline{n})$ and $\neg R(n)\Longrightarrow T\vdash\neg\varphi(\overline{n})$ hold for every $n\in\mathbb{N}$.

• ✧*

Trivially, representability of a relation in a consistent theory implies its weaker representability in that theory. The converse does not hold, in the sense that a relation may be weakly representable in a theory without being representable (cf. [16, Theorem II.2.16]):

Remark** 3.3**** (On the Representability of Provability)**

Let ${\rm Prov}_{\textsl{{Q}}}(x)$ be a provability predicate for Robinson Arithmetic Q; then for every sentence $\phi$, we have $\textsl{{Q}}\vdash\phi$ if and only if $\textsl{{Q}}\vdash{\rm Prov}_{\textsl{{Q}}}(\ulcorner\phi\urcorner)$, since ${\rm Prov}_{\textsl{{Q}}}$ is a $\Sigma_{1}$-formula and Q is $\Sigma_{1}$-complete and sound. On the other hand, there can be no formula $\Psi(x)$ such that for any formula $\phi$:

${}^{{}_{\bullet}}\,$ if ${\rm Prov}_{\textsl{{Q}}}(\ulcorner\!\phi\!\urcorner)$, then $\textsl{{Q}}\vdash\Psi(\ulcorner\phi\urcorner)$; and

${}^{{}_{\bullet}}\,$ if $\neg{\rm Prov}_{\textsl{{Q}}}(\ulcorner\!\phi\!\urcorner)$, then $\textsl{{Q}}\vdash\neg\Psi(\ulcorner\phi\urcorner)$.

Since, otherwise, provability in Q would be decidable: for a given formula $\phi$ by running an exhaustive proof search algorithm in Q for the formulas $\Psi(\ulcorner\phi\urcorner)$ and $\neg\Psi(\ulcorner\phi\urcorner)$ in parallel, one could decide if $\textsl{{Q}}\vdash\phi$ (exactly when $\textsl{{Q}}\vdash\Psi(\ulcorner\phi\urcorner)$) or $\textsl{{Q}}\nvdash\phi$ (exactly when $\textsl{{Q}}\vdash\neg\Psi(\ulcorner\phi\urcorner)$) holds; and this is a contradiction (with Alonzo Church’s Theorem).

• ✧*

For (total) functions we can have four different definitions for representability in theories (originated from [20]).

Definition** 3.4**** (Weakly Representable Functions)**

A function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is weakly representable in a theory $T$, if for some formula $\varphi(x,y)$ we have

$(1)\,$ if $f(n)=m$, then $T\vdash\varphi(\overline{n},\overline{m})$; and

$(2)\,$ if $f(n)\neq m$, then $T\not\vdash\varphi(\overline{n},\overline{m})$;

for every $n,m\in\mathbb{N}$.

• ✧*

Definition** 3.5**** (Representable Functions)**

A function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is representable in a theory $T$, if for some formula $\psi(x,y)$ we have

$(1)\,$ if $f(n)=m$, then $T\vdash\psi(\overline{n},\overline{m})$; and

$(2)\,$ if $f(n)\neq m$, then $T\vdash\neg\psi(\overline{n},\overline{m})$;

for every $n,m\in\mathbb{N}$.

• ✧*

Definition** 3.6**** (Strongly Representable Functions)**

A function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is strongly representable in a theory $T$, if for some formula $\theta(x,y)$ we have

$(1)\,$ $T\vdash\theta(\overline{n},\overline{f(n)})$; and

(2)\,T\vdash\forall y,z\big{(}\theta(\overline{n},y)\wedge\theta(\overline{n},z)\rightarrow y=z\big{)};

for every $n\in\mathbb{N}$.

• ✧*

Definition** 3.7**** (Provably Total Functions)**

A function $f\colon\mathbb{N}\rightarrow\mathbb{N}$ is provably total in a theory $T$, if for some formula $\eta(x,y)$ we have

$(1)\,$ $T\vdash\eta(\overline{n},\overline{f(n)})$; and

(2)\,T\vdash\forall x\exists y\big{(}\eta(x,y)\wedge\forall z\big{[}\eta(x,z)\rightarrow y=z\big{]}\big{)};

for every $n\in\mathbb{N}$.

• ✧*

Indeed, these definitions get stronger from top to bottom: If $T$ is consistent and can prove $\overline{i}\!\neq\!\overline{j}$ for every distinct $i,j\!\in\!\mathbb{N}$, then every provably total function is strongly representable, and every strongly representable function is representable, and every representable function is weakly representable in $T$ with the same formula. It is a folklore result that representability implies strong representability (cf. [16, Proposition I.3.3]):

Lemma** 3.8**** (Representability $\Longrightarrow$ Strong Representability)**

In a theory $T$ which can prove the sentences $\forall y(y\!<\!\overline{n}\,\vee\,y\!=\!\overline{n}\,\vee\,\overline{n}\!<\!y)$, $\forall y(y\not<0)$ and $\forall y(y\!<\!\overline{n\!+\!1}\leftrightarrow y\!=\!\overline{0}\,\vee\,\cdots\,\vee\,y\!=\!\overline{n})$, for all $n\!\in\!\mathbb{N}$, representability of a function implies its strong representability.

Proof:

If $f$ is representable by the formula $\psi(x,y)$ in $T$, then let $\theta(x,y)$ be $\psi(x,y)\wedge\forall z\!<\!y\neg\psi(x,z)$. We now show that $T\vdash\theta(\overline{n},\overline{f(n)})$ and $T\vdash\theta(\overline{n},y)\rightarrow y=\overline{f(n)}$ hold for any $n\!\in\!\mathbb{N}$ as follows. Reason in $T$: If $z\!<\!\overline{f(n)}$, then if $f(n)\!=\!0$ we have a contradiction, otherwise (if $f(n)\!\neq\!0)$ we have $z\!=\!\overline{i}$ for some $i\!<\!f(n)$. Of course for any such $i$ we have $\neg\psi(\overline{n},\overline{i})$; thus $\neg\psi(\overline{n},z)$. If $\theta(\overline{n},y)$ and $y\!\neq\!\overline{f(n)}$, then either $y\!<\!\overline{f(n)}$ or $\overline{f(n)}\!<\!y$. In the former case we have $y\!=\!\overline{i}$ for some $i\!<\!f(n)$, if $f(n)\!\neq\!0$; otherwise $y\!<\!0$ is a contradiction, and so by $\neg\psi(\overline{n},\overline{i})$ we have $\neg\psi(\overline{n},y)$, which is a contradiction with $\theta(\overline{n},y)$. In the latter case, by $\forall z\!<\!y\neg\psi(\overline{n},z)$ we should have $\neg\psi(\overline{n},\overline{f(n)})$; a contradiction again. ❑

The question if the strong representability implies the provable totality was mentioned open in the first edition (1964) of the classical book [14]. In 1965, Verena Esther Huber-Dyson showed that the strong representability implies the provable totality [4], and as a result this was Exercise 3.35 in the second edition (1979) of that book, and Exercise 3.32 in the third edition (1987), attributed to V.  H. Dyson. Then in the fourth (1997), the fifth (2009) and the sixth (2015) editions, this has been proved in Proposition 3.12, attributed to V.  H. Dyson again.

Theorem** 3.9**** (Strong Representability $\Longrightarrow$ Provable Totality)**

If a function is strongly representable in a theory, then it is provably total in that theory.

Proof:

Let us note that we do not put any condition on the theory $T$; let $f$ be strongly representable by $\theta$ in $T$. Let $\exists!u\,\mathcal{A}(u)$ be an abbreviation for the formula \exists u\big{(}\mathcal{A}(u)\wedge\forall v[\mathcal{A}(v)\rightarrow v\!=\!u]\big{)}. Put

[TABLE]

For any $n\!\in\!\mathbb{N}$ we have $T\vdash\exists!y\,\theta(\overline{n},y)$; thus from $T\vdash\theta(\overline{n},\overline{f(n)})$ we get $T\vdash\eta(\overline{n},\overline{f(n)})$. Now, we show that $T\vdash\forall x\exists!y\,\eta(x,y)$. Reason inside $T$: If $\exists!z\,\theta(x,z)$, then that unique $z$ which satisfies $\theta(x,z)$ also satisfies $\eta(x,z)$ and \forall u\big{[}\eta(x,u)\rightarrow u\!=\!z\big{]}, whence $\exists!y\,\eta(x,y)$. If $\neg\exists!z\,\theta(x,z)$, then $y\!=\!0$ is the unique $y$ that satisfies $\eta(x,y)$. ❑

The above proof of Dyson appears also in [10, page 63], [12, Proposition 3.8] and [19, Proposition 9.4.2]. The following theorem is usually proved by showing that every weakly representable function is recursive and that every recursive function is (strongly) representable; see e.g. [16, Corollary I.7.8] or [18, Theorem 4.5]. Here we present a new proof.

Theorem** 3.10**** (Weak Representability $\Longrightarrow$ Representability)**

For a theory $T$, suppose the formula ${\rm Proof}_{T}(z,x)$ states that “$z$* is (the Gödel code of) the proof of a formula (with Gödel code) $x$ in $T$”, and suppose that $T$ has the following properties:*

(a)*  $T\vdash\overline{i}\!\neq\!\overline{j}$ and $T\vdash\overline{n}\!\leqslant\!\overline{m}$ and $T\vdash\forall y(\overline{m}\!\leqslant\!y\rightarrow\overline{n}\!\leqslant\!y)$, for any $i,j,n,m\!\in\!\mathbb{N}$ with $i\!\neq\!j$ and $n\!\leqslant\!m$;*

(b)*  $T\vdash\forall y(y\!\leqslant\!\overline{n}\,\vee\,\overline{n}\!\leqslant\!y)$, for all $n\!\in\!\mathbb{N}$;*

(c)*  $T\vdash\forall y(y\!\leqslant\!\overline{n}\leftrightarrow\bigvee\!\!\!\!\!\bigvee_{i=0}^{n}y\!=\!\overline{i})$, for all $n\!\in\!\mathbb{N}$;*

(d)*  if $T\vdash\phi$ and $k$ is the Gödel code of this proof, then $T\vdash{\rm Proof}_{T}(\overline{k},\ulcorner\phi\urcorner)$;*

(e)*  if $k$ is not the Gödel code of a proof of $\phi$ in $T$, then $T\vdash\neg{\rm Proof}_{T}(\overline{k},\ulcorner\phi\urcorner)$, in particular, if $T\not\vdash\phi$, then $T\vdash\neg{\rm Proof}_{T}(\overline{l},\ulcorner\phi\urcorner)$, for any $l\!\in\!\mathbb{N}$.*

Then weak representability of a function implies its representability in $T$.

Proof:

Suppose the function $f$ is weakly representable by $\varphi$ in $T$. For the (bounded provability) predicate $\boldsymbol{\varrho}(z,x)=\exists u\!\leqslant\!z\,{\rm Proof}_{T}(u,x)$, let \psi(x,y)=\exists z\big{[}\boldsymbol{\varrho}(z,\ulcorner\varphi(x,y)\urcorner)\wedge\forall y^{\prime}\!\leqslant\!z\,[y^{\prime}\!\neq\!y\rightarrow\neg\boldsymbol{\varrho}(z,\ulcorner\varphi(x,y^{\prime})\urcorner)]\big{]}. For showing the representability of $f$ by $\psi$ in $T$ we prove that:

(1) $T\vdash\psi(\overline{n},\overline{f(n)})$ for all $n\!\in\!\mathbb{N}$, and

(2) $T\vdash\neg\psi(\overline{n},\overline{m})$ for all $n,m\!\in\!\mathbb{N}$ with $m\!\neq\!f(n)$.

(1): Fix an $n\!\in\!\mathbb{N}$ and let $k\!\in\!\mathbb{N}$ be a Gödel code for the proof of $T\vdash\varphi(\overline{n},\overline{f(n)})$; so, we have $f(n)\!\leqslant\!k$. By (d) above we have $T\vdash{\rm Proof}_{T}(\overline{k},\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$, and so $T\vdash\boldsymbol{\varrho}(\overline{k},\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$ by (a) above. Now, for any $i\!\in\!\mathbb{N}$ with $i\!\neq\!f(n)$ we have that $T\not\vdash\varphi(\overline{n},\overline{i})$, and so by (e) above, $T\vdash\neg{\rm Proof}_{T}(\overline{l},\ulcorner\varphi(\overline{n},\overline{i})\urcorner)$ for any $l\!\in\!\mathbb{N}$. Thus, by (c) above, $T\vdash\neg\boldsymbol{\varrho}(\overline{l},\ulcorner\varphi(\overline{n},\overline{i})\urcorner)$. Reason in $T$: for any $y^{\prime}$ with $y^{\prime}\!\leqslant\!\overline{k}$ and $y^{\prime}\!\neq\!\overline{f(n)}$, by (c) above, we have $y^{\prime}\!=\!\overline{j}$ for some $j\!\leqslant\!k$ with $j\!\neq\!f(n)$. For any such $j$ we have $\neg\boldsymbol{\varrho}(\overline{k},\ulcorner\varphi(\overline{n},\overline{j})\urcorner)$; and so, by (c) above, the sentence $\forall y^{\prime}\!\leqslant\!\overline{k}\,[y^{\prime}\!\neq\!y\rightarrow\neg\boldsymbol{\varrho}(\overline{k},\ulcorner\varphi(\overline{n},y^{\prime})\urcorner)]$ holds. Thus, $\psi(\overline{n},\overline{f(n)})$.

(2): Fix some $n,m\!\in\!\mathbb{N}$ with $m\!\neq\!f(n)$. Let us note that we already have:

\neg\psi(x,y)\!\equiv\!\forall z\big{[}\boldsymbol{\varrho}(z,\ulcorner\varphi(x,y)\urcorner)\rightarrow\exists y^{\prime}\!\leqslant\!z\,[y^{\prime}\!\neq\!y\wedge\boldsymbol{\varrho}(z,\ulcorner\varphi(x,y^{\prime})\urcorner)]\big{]}.

For proving $T\vdash\neg\psi(\overline{n},\overline{m})$ we show that

T\vdash\forall z\big{[}\boldsymbol{\varrho}(z,\ulcorner\varphi(\overline{n},\overline{m})\urcorner)\rightarrow\overline{f(n)}\!\leqslant\!z\wedge\overline{f(n)}\!\neq\!\overline{m}\wedge\boldsymbol{\varrho}(z,\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)\big{]}.

Let $k\!\in\!\mathbb{N}$ be a Gödel code for the proof of $T\vdash\varphi(\overline{n},\overline{f(n)})$; so, $f(n)\!\leqslant\!k$. Also, from $T\not\vdash\varphi(\overline{n},\overline{m})$, by (e) above, we have $T\vdash\neg\boldsymbol{\varrho}(\overline{l},\varphi(\ulcorner\overline{n},\overline{m})\urcorner)$, for any $l\!\in\!\mathbb{N}$. Reason in $T$: for any $z$, by (b) above, we have either (2.i) $z\!\leqslant\!\overline{k}$ or (2.ii) $\overline{k}\!\leqslant\!z$. (2.i): If $z\!\leqslant\!\overline{k}$ then $z=\overline{i}$ for some $i\!\leqslant\!k$, by (c) above. Now, $\boldsymbol{\varrho}(\overline{i},\ulcorner\varphi(\overline{n},\overline{m})\urcorner)\rightarrow\overline{f(n)}\!\leqslant\!\overline{i}\wedge\overline{f(n)}\!\neq\!\overline{m}\wedge\boldsymbol{\varrho}(\overline{i},\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$ follows from $\neg\boldsymbol{\varrho}(\overline{i},\ulcorner\varphi(\overline{n},\overline{m})\urcorner)$; thus $\neg\psi(\overline{n},\overline{m})$ holds. (2.ii): If $\overline{k}\!\leqslant\!z$, then $\overline{f(n)}\!\leqslant\!z$, by (a) above, which also implies $\overline{f(n)}\!\neq\!\overline{m}$. On the other hand, we have ${\rm Proof}_{T}(\overline{k},\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$ and so $\exists u\!\leqslant\!z\,{\rm Proof}_{T}(u,\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$, or equivalently $\boldsymbol{\varrho}(z,\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$. Thus, $\neg\psi(\overline{n},\overline{m})$ holds since we have $\overline{f(n)}\!\leqslant\!z\wedge\overline{f(n)}\!\neq\!\overline{m}\wedge\boldsymbol{\varrho}(z,\ulcorner\varphi(\overline{n},\overline{f(n)})\urcorner)$. ❑

Let us note that the (very weak) finitely axiomatizable Robinson’s Arithmetic Q satisfies all the conditions (a,b,c,d,e) in Theorem 3.10.

Acknowledgements:

​​​​​The author was supported by grant №  S​ /​ 712 from the University of Tabriz, Iran.