3
$\begingroup$

In the book Metamathematics of First-Order Arithmetic, I learned that a general recursive function can be defined by a $\Delta_1$-formula. I am curious about another matter: Since we have $Pr_T^\bullet (x)$that represents provability and a definition of a recursive function, perhaps we can discuss the finite sequence (arithmetic expression) of the supposed function expands into PA, and then find its corresponding value through provability.

For example, the exponentiation I define below:

Define a primitive recursive function:

$$ g(x) = \ulcorner 1 \urcorner \quad \text{(the code of 1)} $$

$$ h(a, b, c) = \ulcorner (\urcorner\overparen{} \ulcorner a \urcorner\overparen{} \ulcorner * \urcorner\overparen{} c \overparen{} \ulcorner )\urcorner $$

$$ f(x, 0) = g(x) = \ulcorner 1 \urcorner $$

$$ f(x, n+1) = h(x, n, f(x, n)) $$

Then there exists a formula $\varphi(x, y, z)$ such that $f(x, y) = z$ iff $\varphi(x, y, z)$. But here $z$ is just the code of a string of symbols, not the number as a result, so next define:

$$ \text{exp}(x, y) = (\text{min}\ z) (Pr_T^\bullet(\ulcorner (\urcorner\overparen{} f(x, y)\overparen{} \ulcorner = \urcorner\overparen{} \ulcorner z \urcorner\overparen{} \ulcorner )\urcorner )) $$

It seems to define exponentiation, but this should be wrong. The problem should occur in the last definition, because $(\text{min}\ z)$ acts on a predicate rather than a function. If so, how can this error be corrected? Another reason might be that $\{x | Pr_T^\bullet (x)\}$ is $\Sigma_1$, but I am not sure.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

You haven't said which theory $T$ you intend to use, but probably you have in mind something like PA. You are proposing to define exponentiation $x^y$ essentially as "the smallest $z$ for which $T$ can prove that $z=x*x*\cdots*x$, with $y$ factors."

This idea has problems and ultimately it won't be provably equivalent to exponentiation. One big issue is that it just doesn't work at all in models of $T$ in which $\text{Con}(T)$ fails. The reason is that in such a model, everything is provable, and so the least $z$ meeting that condition will be $z=0$, which is not the answer we want.

Because of this, your definition is not provably equivalent to exponentiation. And this issue is a serious obstacle in general to using provability in this way to define functions, which addresses your title question negatively.

Note also, however, that the proposal doesn't provide a computable means of computing exponentiation, since $\mu z\, \varphi(z)$ is not computable in general for $\Sigma_1$ assertions $\varphi$, which is your case. Basically, we can't computably determine if $z=0$ will be the right answer, since if $\text{Con}(T)$ fails it will be, but there is no computable means to determine this.

Improve this answer
$\endgroup$
13
  • 3
    $\begingroup$ What does, however, work is to take for a given $x,y$ the minimal proof of a formula of the form $\phi(\ulcorner x\urcorner, \ulcorner y\urcorner,\ulcorner z\urcorner)$, where $\phi$ is a $\Sigma_1$-definition of exponentiation, and output $z$. $\endgroup$
    – Emil Jeřábek
    Commented Jul 29 at 14:36
  • 2
    $\begingroup$ (Meanwhile, the larger issue is: why bother? We already have straightforward definitions of exponentiation that don't involve coding up the proof system. Just code the primitive recursive definition itself.) $\endgroup$
    – Joel David Hamkins
    Commented Jul 29 at 14:39
  • $\begingroup$ Well, the argument really shows that the proof predicate can serve the role of Kleene's $T$ predicate, giving an alternative proof of Kleene's normal form. I'm not sure how useful is that. $\endgroup$
    – Emil Jeřábek
    Commented Jul 29 at 15:14
  • 2
    $\begingroup$ For a related fact, one way of proving that $I\Delta_0+\mathrm{EXP}$ has a truth predicate for $\Sigma_1$ sentences is to take the cut-free provability predicate for Q. $\endgroup$
    – Emil Jeřábek
    Commented Jul 29 at 17:41
  • 1
    $\begingroup$ His proposal is to use the minimal proof, not the minimal value of $z$, but then extract $z$ from that proof. This fixes the problem that I had identified, at least for standard $x$ and $y$. But it doesn't work correctly for nonstandard $x$ and $y$, and so I still find it wrong-headed to use proofs at all in the way you suggest. $\endgroup$
    – Joel David Hamkins
    Commented Jul 30 at 19:36

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .