=Paper= {{Paper |id=Vol-2396/paper11 |storemode=property |title=Does Every Recursively Enumerable Set Admit a Finite-Fold Diophantine Representation? |pdfUrl=https://ceur-ws.org/Vol-2396/paper11.pdf |volume=Vol-2396 |authors=Domenico Cantone,Alberto Casagrande,Francesco Fabris,Eugenio Omodeo |dblpUrl=https://dblp.org/rec/conf/cilc/CantoneCFO19 }} ==Does Every Recursively Enumerable Set Admit a Finite-Fold Diophantine Representation?== https://ceur-ws.org/Vol-2396/paper11.pdf
Does Every Recursively Enumerable Set Admit a
          Finite-Fold Diophantine Representation??

                                   1                              2                         2
          Domenico Cantone , Alberto Casagrande , Francesco Fabris , and
                                                        2
                                          Eugenio Omodeo

      1
          Dept. of Mathematics and Computer Science, University of Catania, Italy.
                              domenico.cantone@unict.it
           2
             Dept. of Mathematics and Geosciences, University of Trieste, Italy.
                       {acasagrande,ffabris,eomodeo}@units.it



          Abstract.        The Davis-Putnam-Robinson theorem showed that every par-
          tially computable m-ary function f (a1 , . . . , am ) = c on the natural num-
          bers can be specied by means of an exponential Diophantine formula
          involving, along with parameters a1 , . . . , am , c, some number κ of ex-
          istentially quantied variables. Yuri Matiyasevich improved this theo-
          rem in two ways: on the one hand, he proved that the same goal can
          be achieved with no recourse to exponentiation and, thereby, he pro-
          vided a negative answer to Hilbert's 10th problem; on the other hand,
          he showed how to construct an exponential Diophantine equation speci-
          fying f which, once a1 , . . . , am have been xed, is solved by at most one
          tuple hv 0 , . . . v κ i of values for the remaining variables. This latter prop-
          erty is called single-foldness. Whether there exists a single- (or, at worst,
          nite-) fold polynomial Diophantine representation of any partially com-
          putable function on the natural numbers is as yet an open problem. This
          work surveys relevant results on this subject and tries to draw a route
          towards a hoped-for positive answer to the nite-fold-ness issue.
          Key words. Hilbert's 10     problem, exponential-growth relation, nite-
                                   th

          fold Diophantine representation, Pell's equation.


Introduction


The celebrated Davis-Putnam-Robinson theorem of 1961 ensures that every com-
                                                   m
putable function F from a subset of N                  into N = {0, 1, 2, . . . } can be specied as



                                                                            variables

          F(a1 , . . . , am ) = c ⇐⇒ (∃ x1 · · · ∃ xκ ) ϕ( a1 , . . . , am , c , x1 , . . . , xκ ) ,
                                                           z                 }|                {
                                                                                                       (†)
                                                           |        {z       } | {z }
                                                                   parameters        unknowns



for some formula ϕ that only involves:

?
    The authors acknowledge partial support from the INdAM-GNCS 2019 research
    project Logic Programming for early detection of pancreatic cancer and from Uni-
    versità degli Studi di Catania, Piano della Ricerca 2016/2018 Linea di intervento 2.
  the shown (pairwise distinct) variables,
  positive integer constants,
  addition, multiplication, and exponentiation operators,                              1


  the logical connectives & , ∨, ∃ v , = .
     Two major improvements to this result were achieved by Yuri Matiyasevich.
In [15] he showed that (†) can be set up without exponentiation; in [16], while
retaining exponentiation in it, he boiled ϕ down to the format


 ϕ( a1 , . . . , am , c , x1 , . . . , xκ ) :=
       P 0 (a1 , . . . , am , c, x2 , . . . , xκ ) = 4x1 + x1 + P 00 (a1 , . . . , am , c, x2 , . . . , xκ ),

                             0           00
where κ > 0 and P                and P        are polynomials with coecients in N, devoid of
occurrences of x1 , such that             no two tuples
               ha1 , . . . , am , v 0 , v 1 , . . . , v κ i , ha1 , . . . , am , u0 , u1 , . . . , uκ i

on N exist satisfying ϕ( a1 , . . . , am , v 0 , . . . , v κ )           & ϕ( a1 , . . . , am , u0 , . . . , uκ ).
Thus, every tuple ha1 , . . . , am i on N either admits no continuation hv 0 , . . . , v κ i
satisfying ϕand then ha1 , . . . , am i does not belong to the domain of F or
exactly one, and then v 0 is precisely the value F(a1 , . . . , am ).

     By introducing a little terminologyrather common in recursion theory, cf.
                                                                                 m
[4]we will be better-o in what follows. A set R ⊆ N                                , with m > 0, is called

recursively enumerable (or, shortly, r.e.): when it is the domain of a partially
     computable function F taking m arguments (see, e.g., [7, Sect. 2.4]);
exponential Diophantine : when it can be specied as
                                                                                  variables

                R(a1 , . . . , am ) ⇐⇒ (∃ x1 · · · ∃ xκ ) ϕ( a1 , . . . , am , x1 , . . . , xκ ) ,
                                                             z              }|               {
                                                                                                             (∗)
                                                             | {z } | {z }
                                                                        parameters          unknowns



     for some formula ϕ involving the syntactic means listed at the beginning;
Diophantine : when it can be specied in the form (∗), with ϕ involving the
     syntactic armory just recalled,               save exponentiation.
Moreover, a representation of R in the form (∗) is said to be

single-fold or univocal : when each tuple ha1 , . . . , am i of natural numbers has
     at most one continuation hv 1 , . . . , v κ i such that ϕ(a1 , . . . , am , v 1 , . . . , v κ );
nite-fold : when each tuple ha1 , . . . , am i of natural numbers has only nitely
     many continuations hv 1 , . . . , v κ i such that ϕ(a1 , . . . , am , v 1 , . . . , v κ ) holds.

     Let us sum up, utilizing these notions, the important results mentioned above,
along with two open issues raised many years ago, which still motivate us here:

 Dpr61 [6], known as DPR: Every r.e. set is exponential Diophantine.
1
    We name exponentiation the dyadic operation hr, pi 7→ rp (occasionally, also p 7→ 2p ).
 Mat70 [15], known as DPRM: Every r.e. set is Diophantine.
 Mat74 [16]: Every r.e. set admits a univocal exponential Diophantine representation.
 Dmr76 [5]: Does every r.e. set admit a univocal Diophantine representation?
 Mat10 [14]: Does every r.e. set admit a nite-fold Diophantine representation?

A positive answer to     Dmr76 would combine together both of Matiyasevich's
improvements to DPR, namely Mat70 and Mat74; in [14], Matiyasevich argues
on the signicance of this combination, and on the diculty (as yet unsolved)
of this reconciliation. In [17, p. 50], after discussing the issue again, he ends up
by saying: This relationship between undecidability and non-eectivizability is one
of the main stimuli to improve the DPRM-theorem to single-fold (or at least to nite-
fold) representations and thus establish the existence of non-eectivizable estimates for
genuine Diophantine equations.

     The derivation of DPRM from DPR required that exponentiation itself were
proved to be Diophantine. A result by Julia Robinson, which we recapitulate in
Sect. 2, played historically a key role in this arduous task: she had reduced the
task to the quest for a Diophantine relation of    exponential growth (a notion to be
recalled soon here); and, indeed, Matiyasevich found a polynomial Diophantine
representation of a specic exponential-growth relation.
     After Matiyasevich [14], we have some hope that a positive answer to Mat10
can likewise be obtained by proving two facts:


  there exists a relation M(p, q), sharing with the relation 2p = q (seen as the
     set {hp , 2 i | p ∈ N}) a certain special property (see Fig. 1 ), that admits a
               p                                                      2


     nite-fold Diophantine representation;
  consequently, via a reduction technique reminiscent of J. Robinson's one,
     exponentiation will have a nite-fold Diophantine representation. (Hence, via
     Mat74, every r.e. set will inherit the nite-fold Diophantine representability.)


     Concerning the former goal, [1,2] propose four exponential-growth relations
as candidate    M's; moreover, [2] proves that one of them enjoys the special
property shown in Fig. 1. It is hard to establish whether any of these candidates
is Diophantine; clearly enough, though, if any of them is indeed Diophantine,
then it has a nite-fold representation.
     Concerning the latter goal, in order to convince ourselves (as well as our
readers) that the sought reduction technique reminiscent of J. Robinson's one
does exist, and to get closer to it, we undertake in this paper a comparison
among various published versions of Robinson's technique, discussing how her
idea evolved over the years from its original formulation of 1952 towards simpler
implementations, one of which might t our needs.
     In preparation for some conclusive answer to Mat10be it positive or neg-
ative, this paper brings together scattered notes on nite-fold Diophantine
representability. The forthcoming material is organized as follows.

2
    Notice that in the case of the relation 2p = q we could take α = β = δ = γ/2 = 2
    and then p = w + 2, q = 2w+2 .
     There exist integersα > 1 , β > 0 , γ > 0 , δ > 0 such
     that to each w ∈ N other than 0 there correspond p , q
                                β              w
     such that M(p, q), p < γ w , and q > δ α     hold.



Fig. 1. A property (elicited in [14]) which, if enjoyed by a relation M ⊆ N × N ad-
mitting a nite-fold Diophantine representation, would ensure existence of a nite-fold
Diophantine representation of exponentiation.


      Sect. 1 reports the construction of a univocal exponential Diophantine rep-
resentation of any given r.e. set R. Out of a formally specied register machine
that reaches termination on the tuples belonging to Rand only on those, the
proposed construction technique generates a formula ϕ such that (∗) holds. By
and large, singlefold-ness results from the determinism of the device emulated
by the exponential constraints embodied into ϕ.
      Then Sect. 2 discusses two ways of reducing exponentiation to any exponential-
growth dyadic relation J (p, q); both techniques are due to Julia Robinson, who
proposed them in 1952 and 1969 respectively. They ensure that if a (polyno-
mial) Diophantine representation for J is found, then it can be converted into
a Diophantine representation of exponentiation, and hence of any given r.e. set.
Appendix A expounds the original correctness proof regarding the result of 1969.
      Sect. 3 reports three ways, devised by Davis, Matiyasevich, and J. Robinson,
                                         y i (a) i∈N of solutions to the special-
of reducing exponentiation to the sequence
                           2         2            3
form Pell equation (a − 1) y + 1 =  with a > 1. Appendices B and C dwell
upon the techniques by which those three reductions were obtained.




1      Univocal exponential representation of any r.e. set


Where does singlefold-ness of the exponential representation of an r.e. set R ⊆
Nm whatsoever stem from? In [16], where it was rst achieved, such a represen-
tation took the form


 R(a1 , . . . , am ) ⇐⇒ (∃ x1 · · · ∃ xκ ∃ y ∃ w) 2y = w &
                                                 
                                                                                                    
                                                   D( a1 , . . . , am , x1 , . . . , xκ , y, w ) = 0 ,

where D is a polynomial in the variables a1 , . . . , am , x1 , . . . , xκ , y, w with inte-
gral coecients; this was then rewritten, by exploiting an idea of Hilary Putnam,
as


 R(a1 , . . . , am ) ⇐⇒ (∃ x1 · · · ∃ xκ ∃ y ∃ z ∃ u)            4u + u =
                           y + (y + z)2 1 − D2 ( a1 , . . . , am , x1 , . . . , xκ , y, y + z ) .
                                                                                            

3
     `Q = ' means that the value of Q must be a perfect square.
                                  4
This format is very elegant,          but the proof of the associated representability
result less transparent than later single-fold-representability proofs where ex-
                                                                   register
ponentiation was employed more liberally. Various proofs referred to
machines, a popular model of abstract computing device, to which James P.
Jones and Yu. V. Matiyasevich resorted in three papers (see, e.g., [8]). We rely
upon Martin Davis's account [4, Chapter 6] of the Jones-Matiysevich's approach
in carrying out our considerations below.

     A register machine  π consists of a list =0 , . . . , =` of instructions ; any execu-
tion of   π begins with instruction =0 and, unless it goes on forever, it terminates
                                                                           regis-
with =` . Finitely many program variables, R0 , R1 , . . . , Rm , . . . , Rr , called
ters, occur in π ; of these, R0 will hold the result a0 of the computation upon
termination, if execution does reach =` . At the outset, the registers R1 , . . . , Rm
must hold the respective input values a1 , . . . , am , while the values of all remain-
ing registers are supposed to be 0. Here, w.l.o.g., we shall require that a0 = 0.
     There are instructions of ve types:


                      Rj ← R j + 1              increment

                      Rj ← R j − 1              decrement

                      IF Rj = 0 GOTO k          conditional branch

                      GOTO k                    un conditional branch
                      STOP                      halt



Suitable programming rules enforce that: (0)           STOP only appears at the end of
π , namely as =` ; (1) the number k that follows GOTO in a branch instruction
always belongs to the interval 0, . . . , `; (2) it never happens that a decrement
Rj ← Rj −1 is reached when the current value of its register Rj is 0; (3) whenif
everthe instruction =` is reached, each one of (R0 ,) R1 , . . . , Rr has value 0.
    The behavior of π when its execution is triggered with input values ai loaded
in its input registers R1 , . . . , Rm should be readily grasped by any person familiar
with procedural programming. In order to describe that functioning, we must
specify by means of exponential Diophantine constraints how the values of the
registers evolve over time and which instruction is about being eected at each
of the discrete time instants beating the execution.
     An unknown, s, representing the overall number of execution steps, will play
a crucial role; in fact, we are interested in the r.e. set R consisting of those tuples
ha1 , . . . , am i which, when fed into π , lead π to termination. Unless execution
terminates, no natural number s should be an acceptable value for s under the
constraints to be associated with         π ; on the other hand, when a tuple leads
to termination, an acceptable value s for s must exist and it must be unique,
because the abstract computing device which we are modeling is deterministic.

4
    Notice that the polynomial y + (y + z)2 belongs to Kosovski's family of polynomials
    x1 + (x1 + x2 )2 + (x1 + x2 + x3 )3 + · · · + (x1 + · · · + xn )n dening, for each n ∈ N,
    an injective function of Nn into Nsee [9].
In the latter case, the course of values of each register Rj (j = 0, . . . , r ) can be
modeled as the sequence hrj,0 , . . . , rj,s i formed by its initial value rj,0 and by its
subsequent values rj,t with t > 0, where rj,t is the value held by Rj right after the
execution of the t-th step. Notice that if execution terminates in s computation
steps, no register will ever hold a value exceeding the quantity a1 + · · · + am + s;
therefore we can represent the course of values of each Rj by a single unknown,
                                        t Ps
rj , designating the amount   t=0 rj,t Q , where Q > a1 + · · · + am + s is a
base for the positional encoding of numbers large-enough in order that every
rj,t acts as a digit. Since s is a priori unknown, Q must in its turn show as an
unknown, Q, in the constraints specifying π . Out of practical concerns, it turns
out convenient to subject Q, along with a buddy unknown [, to the conditions


               2[ 6 (2 a1 + · · · + 2 am + 2 s) max (` + 1) < 2[ · 2 = Q ,

ensuring its uniquenessand thus, thanks to the determinism of                                  π , also the
uniqueness of r0 , . . . , rr .
     Additional unknowns l0 , . . . , l` are needed to describe which instruction is
                                                                 t              Ps
executed at each instant: li designates the amount     t=0 li,t Q , where li,t = 1 if
the instruction to be executed at time t is =i , and li,t = 0 otherwise. One nal
unknown, I , is required to satisfy the equations

                                                                             `
                                                                             X
                                  1 + (Q − 1) I = Qs+1 =                            li ,
                                                                             i=0
                          Ps          t
so that I designates             t=0 Q . Thus, with respect to the bases Q and 2, I reads


                           |1 . {z
                                . . 11}       and           0| .{z
                                                                 . . 0} 1 . . . 0| .{z
                                                                                     . . 0} 1
                              s+1                                [                   [
                                                             |            {z                }
                                                                         s+1

and the equation on the right reects the fact that exactly one instruction is
executed at each step. Putting

                             
                                  0 when =i does not aect Rj , else
              ∆j,i =Def
                                 ±1 according to whether =i is Rj ← Rj ± 1 ,

we must then require, for j = 0, . . . , r that

                                                                    
                                  P`                                  aj if 0 < j 6 m ,
                   rj = rj +              i=0 ∆j,i li       Q+
                                                                         0 otherwise,
                                                                                                          5
to state how the course of values of each variable is ruled by the execution steps.

5
    Rather than presupposing that the value a0 of the output register be 0 at
    the end,
              here we could  have modied the condition associated with R0 into
    r0 = r0 + `i=0 ∆0,i li Q − Qs+1 a0 , thus capturing the graph ha0 , a1 , . . . , am i
                 P

    an r.e. set on its own rightof the function computed by π instead of its domain.
     To perfect the constraint-based description of the execution of        π ,k we shall
                  dominance relation a v b that occurs between a =                     h
                                                                            P
resort to the
           Pk                                                                  h=0 ah 2
                       h
and b =     h=0 bh 2 , with a0 , b0 ,. . . , ak , bk ∈ {0, 1}
                                                             , if 1and   if ah 6 bh
                                                                      only
                                      0                    0            1
holds for h = 0, 1, . . . , k . Since     =  0  and 1 =        =      =
             Pk                       1                    0       0    1 , the Lucas's
                         h
                   b h 2          Q k   b
                                          
congruence Pk h=0
                         h     ≡ h=0 ahh (mod 2) yields that a v b holds if and
              h=0 ah 2
        b
          
only if       is odd. Hence dominance is exponential Diophantine; in fact, thanks
          a
to the binomial theorem, a v b holds if and only if the remainder of the integer
              j             b        k
division of    2b+1 + 1 / 2b a+a by 2b+1 is odd. The nal constraints needed
are, for j = 0, 1, . . . , r and i = 0, 1, . . . , `:


 • rj v bQ/2 − 1c I and li v I , 1 v l0 , l` v Qs ;
 • Q li v li+1 when =i is an incre-/decre-ment instruction;
 • Q li v lk when =i is an unconditional branch instruction GOTO k ;
 • Q li v li+1 + lk and Q li v li+1 + Q I − 2 rj when =i is a conditional branch
   instruction IF Rj = 0 GOTO k .


Example 1 (Adapted from [5]). Goldbach's conjecture, stating that every even
integer greater than 2 is the sum of two prime numbers, can be formulated in a
rst-order arithmetic of natural numbers by the sentence
                                                                               
                      ( p = u·v ∨ q = u·v ) =⇒ ( u = 1 ⇐⇒ v 6= 1 ) & a+a+4 = p+q .
                                                                  
∀ a∃ p∃ q∀ u∀ v

     Thanks to DPR, the conjecture can also be formulated with no quantier
alternations, by means of a sentence of the form
                          ¬(∃ x0 · · · ∃ xκ ) γ( 0 , x0 , x1 , . . . , xκ ) ,
where γ is a quantier-free exponential Diophantine formula enforcing that

                                                                  variables

                   G(a) = c ⇐⇒ (∃ x1 · · · ∃ xκ ) γ( c , a , x1 , . . . , xκ ) ,
                                                     z       }|            {
                                                     |{z} | {z }
                                                          param's    unknowns


holds, where
                                
                                 1 if there are prime numbers p, q
                      G(a) =Def     such that a + a + 4 = p + q ,
                                  0 otherwise.
                                

     Such a γ can be built by conjoining together all constraints that specify the
behavior of a register machine         γ computing G , in the manner discussed above.  6




2     Two admirable ways of specifying exponentiation in
      terms of a relation of exponential growth


In the seminal paper [18] published in 1952, Julia Robinson discussesamong
many thingshow to specify the graph of exponentiation, namely the triadic

6
    Bear in mind, here, the remark made in the preceding footnote.
              n
relation b        = c, in the format
                                                                variables


                      bn = c ⇐⇒ (∃ x1 · · · ∃ xκ ) ϕ( b, n, c , x1 , . . . , xκ )
                                                      z         }|            {
                                                                                            ( ‡)
                                                      | {z } | {z }
                                                         param's    unknowns



closely analogous to (†), with permission to employ in the construction of ϕ,
instead of exponentiation, a dyadic relation J which is                of exponential growth in
the following sense:


i)     J (p, q) implies q < pp ;
                                                                 `
ii)    for each ` > 0, there are p and q such that J (p, q) and p < q .


      The essence of such a specication is best explained in terms of a polynomial
which, chronologically (see [12, p.531]), made its rst appearance long after 1952:


Lemma 1. There is a polynomial Q in two variables with coecients in N such
that (using τ =  as a short for ∃ q ( τ = q 2 ) ):
  Q(w, h) =  =⇒ h > ww ;
  to every w, there correspond h's such that Q(w, h) = .
Proof (just a clue). It suces to take Q(w, h) := (w + 2)3 (w + 4) (h + 1)2 + 1.
Theorem 1. Let Q be as in Lemma 1. The following bi-implication then holds
if J meets the exponential-growth requirements i) and ii).

                                                       
         b = c ⇐⇒ (∃ w , h , a , d , ` , u , v , s , q) (c − 1)2 + b + n = 0 ∨
          n


                                                                (c + b = 0 & n > 1) ∨
                     
                         b > 1 & c > 1 & d > ` & J (a, d)                             &
                                                  2
                                                                                      &
                                    
                         `2 = a2 − 1 n + (a − 1) s + 1

                         w > b max n & Q(w , h) = q 2 & a > h max (c + 1) &
                                                          
                         u = (a b − 1) v + 1 & c = bu/`c
                          2    2 2      2
                                                             .

This rule, if there exists a Diophantine relation J satisfying i) & ii), provides a
Diophantine representation of exponentiation.
Proof. Proving the stated bi-implication is not a simple matter: we refer the
interested reader to [2, Appendix A] for details on this.
      Concerning the second part of the claim, we must show that certain relations
are Diophantine; namely: x > y ⇔ ∃ v (x = v + y), x > y ⇔ x > y + 1,
x = y max z ⇔ (x = y > z ∨ x = z > y), x = by/zc ⇔ ∃ q q z 6 y < (q+1) z .
    In [19, p. 109 and p. 112], J. Robinson simplies the above construction and
proof, getting:


Theorem 2. Suppose that J is an exponential-growth relation such that J (p, q)
implies p > 1, and let Q be as in the proof of Lemma 1. Then the bi-implication
                                           
         b = c ⇐⇒ (∃ a , d , ` , s , x , h) (c − 1)2 + n = 0
          n
                                                                               ∨
                                                 (n > 1 & c + b = 0)           ∨
         
             n > 1 & b > 1 & J (a, d) & d > ` & a > b + n                      &
                                        2
             `2 = (a2 − 1) n + (a − 1) s + 1 & Q(b + n − 2, h) = x2 &
                          


                                                                               &
                                                    
             2 a b − b2 − 1 > (b + n + 1) x max c + 1
                                                                    
                                                      
             2 a b − b2 − 1 | ` −    a − b (a − 1) s + n − c

holds, which gives us a Diophantine repr. of exponentiation if J is Diophantine.
Proof. A proof of the stated bi-implication is provided in Appendix A; clearly
divisibility is Diophantine, since x | y       ⇔ ∃ v (y = v x).


3    Three ways of specifying exponentiation in terms of the
     sequence of solutions to a special-form Pell equation

                                        2
Pell equations of the special form x        −(a2 −1) y 2 = 1 , with a > 1, have peeped in
in the preceding section. Through one such equation we enforced a relationship
                                     
between ` and r :=     n + (a − 1) s in Theorems 1 and 2. Constraints involving
                                                                               2
the tricky polynomial Q(w, h) have also shown up; as one sees, Q(w, h) = q can
                                             2
                                                        2
                                                                           2
be put in the said Pell format, becoming q − (w +3) −1 (w +2) (h+1)              = 1.
                                               2      2
   Generally speaking, the Pell equation x − d y = 1 in the unknowns x, y has
innitely many solutions in N, provided that the parameter d (also in N) is not
                                                    2
a perfect square. In the special case when d = a − 1 with a > 1, the increasing
sequence hxi (a) , y i (a)i     of its solutions satises the double recurrence
                            i∈N

                  y 0 (a) = 0 ,     y 1 (a) = 1 = x0 (a) ,      a = x1 (a) ,
                             y i+2 (a) = 2 a y i+1 (a) − y i (a) ,
                             xi+2 (a) = 2 a xi+1 (a) − xi (a) .

We summarize in Fig. 2 the combinatorial interplay among items in this sequence
yielded by their generating rules (see, e.g., [18, pp. 439440] and [12, pp. 527
528]).
    Many of the facts in Fig. 2 are needed, of course, in order to detail the proofs
of Theorems 1 and 2. They also enter Davis's proof [3] of the following:
    1. (2 a)i > y i+1 (a) > y i+1 (a) /a > y i (a) > i and y i+1 (a) > (2 a − 1)i ;
    2. xi+1 (a) > xi+1 (a)/a > xi (a) > ai > i and
       a2 i+2 > (2 a)i+1 > xi+1 (a), xi+2 (a) > ai+2 ;
    3. xi (a) − (a − b) y i (a) ≡ bi (mod 2 a b − b2 − 1);
    4. y i (a) ≡ i (mod a − 1);
    5. (b > 1 & a > bn ) =⇒ [ bn = c ⇐⇒ c xn (a) 6 xn (a b) < (c + 1) xn (a) ];
    6. (b > 1 & a > bn ) =⇒ xn (a) 6 xm (a b) < a xn (a) ⇐⇒ m = n ;
    7. y n (a) | y ` (a) if and only if n | `;   if y 2n (a) | y ` (a), then y n (a) | `.


Fig. 2. The wealth of interplay among solutions to the Pell equation x −(a −1) y = 1 .
                                                                      2   2     2




Theorem 3. The bi-implication
                         
 bn = c ⇐⇒ (∃ a , ` , r ) (c − 1)2 + b + n + a + ` + r = 0                                   ∨
                                  (n > 1 & c + b + a + ` + r = 0)                            ∨
                                  
                                    b > 1 & ` = xn (a) & r = y n (a)                         &

                                     a = xb+n (b + n + 1) & b + n | y b+n (b + n + 1) &

                                     2 a b − b2 − 1 > c                                      &
                                                                                        
                                     c ≡ ` − (a − b) r ( mod 2 a b − b2 − 1 )

holds, where a, `, and r are uniquely determined. This gives us a Diophantine
representation of exponentiation, whichever way we manage to get a Diophantine
representation of the triadic relation y i (a) = y (whose arguments are: i, a, y ).

Proof. A proof of the stated bi-implication results from Appendix B; clearly
                                                                          
congruency is Diophantine, since x ≡ y (mod               z) ⇔ ∃ v v 2 z 2 − (x − y)2 = 0 .

      What we are seeing here is, in essence, a   singlefold representation of expo-
nentiation     in terms of the triadic relation y i (a) = y .7 In fact, for any triple
b, n, c of natural numbers: if bn 6= c, the shown system in the unknowns a, `, r
                          n
etc. has no solution; if b = c, then it has exactly one solution. Matters change
if we specify the relation y i (a) = y by polynomial Diophantine means (which is

7
    To see this more clearly, one should set aside various eliminable constructs. E.g.
    `|', along with xb+n (b + n + 1), can be eliminated by rewriting the fourth line of
    the above specication as a constraint involving a new unknown w, as: (b + n) w =
                                                      2
    y b+n (b + n + 1) & (b + n + 1)2 − 1 (b + n) w + 1 = a2 . Likewise, ` = xn (a)
                                          

    becomes (a2 − 1) r2 + 1 = `2 , and three unknowns will result from elimination of
    >, >, and ≡.
doablesee, e.g., [3] and [12]); for, then, additional unknowns enter into play,
which lead to innitely many solutions when any solution exists.
     As stressed in [17, pp. 4344], all today known methods of constructing
a polynomial Diophantine representation (‡) are in fact based on the study
of the behavior of recurrent sequences like the famous Fibonacci progression
h0, 1, 1, 2, 3, 5, 8, . . .i, or a sequence hy 0 (a) , y 1 (a) , y 2 (a) , . . .i,  taken some mod-
ulo; clearly, this behavior is periodic and as a consequence each known Diophantine
representation of exponentiation is innite-fold.
     The situation does not improve, as for the nitefold-ness issue, even if we
resort to the elegant specication of exponentiation proposed in [13] by Matiya-
sevich, who considers the sequence hm0 (a), m1 (a), m2 (a), . . .i with a ∈ N\{0, 1}
characterized by the recurrence

             m0 (a) = 0 , m1 (a) = 1 , mi+2 (a) = a mi+1 (a) − mi (a) .
The distinguished scholar achieves a singlefold representation of exponentiation
in terms of the triadic relation mi (a) = m. His result, as stated here, also refers
to the sequence      y i (a) i∈N ;8 it is explained, albeit briey, in our Appendix C.
Theorem 4 ([13, pp. 3132]). The bi-implications
       bn = c ⇔            c=             b mn+1 (16 b (n + 1) mn+1 (2 b + 2) + 4) /
                                            mn+1 (16 (n + 1) mn+1 (2 b + 2))c
                                                                               
               ⇔           c=             b y n+1 8 b (n + 1) y n+1 (b + 1)+ 2 /
                                            y n+1 8 (n + 1) y n+1 (b + 1) c
               ⇔ (∃ x , y , z , r , s) z = c y + r & 1 + r + s = y                          &
                                       z = y n+1 (b x + 2)                                  &
                                       y = y n+1 (x)                                       &
                                       x = 8 (n + 1) y n+1 (b + 1)                           .
hold, where x, y, z, r, and s are uniquely determined. This gives us a Diophantine
representation of exponentiation, whichever way we manage to get a Diophantine
representation of either one of the triadic relations mi (a) = m, y i (a) = y .
     One slightly less slick, but nevertheless very elegant, reduction of exponenti-
ation to the sequence        y i (a) i∈N also deserves being mentioned:
Theorem 5 ([12, pp. 534535]). When b > 1 and n > 1, the bi-implication
                                     
         bn = c ⇐⇒ (∃ m , k , p , q ) k + n + 1 = y m b (n + 1)                          &
                                            m = 4 n (c + 1) + b + 2                      &
                                            (m2 − 1) p2 + 1 = q 2                        &
                                            m−1|p−n−1                                    &
                                                                                         
                                                                      
                                             p2 − 4 (k + n + 1 − p c)2 b c n > 0

holds (whence, trivially, the variable m can be eliminated).
8
    An early reduction of exponentiation to an integer quotient that involves, besides
    Diophantine functions, only the triadic relation y i (a) = y , appears in [16, p. 308].
Conclusions


A striking consequence of the univocal exponential representability of any r.e.
set was noted in [16, p. 300 and p. 310]. One can nd a concrete polynomial
H(a, x0 , x1 , . . . , xκ , y, w) with integral coecients such that:

1) to each a ∈ N, there corresponds at most one κ + 2 tuple hv 0 , v 1 , . . . , v κ , ui
                                                 u
    such that H(a, v 0 , v 1 , . . . , v κ , u, 2    ) > 0 holds;
2) to any monadic totally computable function C , there correspond κ + 3 tuples
    ha, v 0 , v 1 , . . . , v κ , ui of natural numbers such that
            H(a, v 0 , v 1 , . . . , v κ , u, 2u ) > 0 and max v 0 , v 1 , . . . , v κ , u > C(a) .

    To see this, refer to an explicit enumeration f 0 , f 1 , f 2 , . . . of all monadic
partially computable functions (see [7, p. 73 ]), so that both of


                      H = { ha1 , a2 i ∈ N2 | f a1 (a1 ) = a2 } ,
                       K = { a ∈ N | ha , xi ∈ H holds for some x }

are r.e. sets, the complement N \ K of the latter is not an r.e. set, and the former
can be represented in the univocal form shown at the beginning of Sect. 1, namely


f a1 (a1 ) = a2 ⇐⇒ (∃ x1 · · · ∃ xκ ∃ y ∃ w) 2y = w & D( a1 , a2 , x1 , . . . , xκ , y, w ) = 0 ,
                                                                                              


where D is a polynomial with integral coecients; then put


           H(a, x0 , x1 , . . . , xκ , y, w) =Def 1 − D2 ( a, x0 , x1 , . . . , xκ , y, w) ,
                                        y
so that H(a, x0 , x1 , . . . , xκ , y, 2    ) > 0 holds if and only if f a (a) = x0 , and hence
H satises 1).
    By way of contradiction, suppose that there is a monadic totally computable
function C∗ such that the inequalities v 0 6 C∗ (a), . . . , v κ 6 C∗ (a), and u 6 C∗ (a)
hold whenever a tuple ha, v 0 , v 1 , . . . , v κ , ui of natural numbers exists such that
H(a, v 0 , v 1 , . . . , v κ , u, 2u ) > 0 holds; that is, they hold when a pair ha , v 0 i ∈ H
exists (this happens, e.g., for the innitely many a's satisfying C∗ = f a ). In
particular, the said inequalities must hold when a ∈ K. But then this would
oer us a criterion for checking whether or not a ∈ K, by evaluating a bounded
                                                                      u
family of expressions of the form H(a, v0 , v1 , . . . , vκ , u, 2 ); however, this would
conict with the fact that N \ K is not r.e. We conclude that H satises 2).

    Summing up, we are in this situation: thanks to                      reductio ad absurdum,
we have found that the course of values of the concrete arithmetic expression
H(a, v0 , v1 , . . . , vκ , u, 2u ) exceeds zero at most once for each value a of a; it is
unconceivable, though, that one can put an eective bound on the search space
                                                          u
for positive values of H(a, v0 , v1 , . . . , vκ , u, 2       ).
    A proof that every r.e. set admits a nite-fold Diophantine polynomial rep-
resentation would yield analogous, equally striking consequences about `non-
eectivizable estimates'.
Acknowledgements


Discussions with Pietro Corvaja were very fruitful for the matters of this paper.




References


 1. D. Cantone and E. G. Omodeo. Can a single equation witness that every r.e. set
    admits a nite-fold Diophantine representation? In P. Felli and M. Montali, editors,
    Proceedings of the 33rd Italian Conference on Computational Logic, Bolzano, Italy,
    September 20-22, 2018., volume 2214 of CEUR Workshop Proceedings, pages 147
    152. CEUR-WS.org, 2018.
 2. D. Cantone and E. G. Omodeo. One equation to rule them all, revisited. 2019?
    In preparation.
 3. M. Davis. An explicit Diophantine denition of the exponential function. Commun.
    Pur. Appl. Math., XXIV(2):137145, 1971.
 4. M. Davis. Lecture Notes in Logic. Courant Institute of Mathematical Sciences,
    New York University, 1993.
 5. M. Davis, Yu. Matijasevi£, and J. Robinson. Hilbert's tenth problem. Diophantine
    equations: positive aspects of a negative solution. In Mathematical Developments
    Arising From Hilbert Problems, volume 28 of Proceedings of Symposia in Pure
    Mathematics, pages 323378, Providence, RI, 1976. American Mathematical Soci-
    ety. Reprinted in [20, p. 269.].
 6. M. Davis, H. Putnam, and J. Robinson. The decision problem for exponential
    Diophantine equations. Ann. of Math., Second Series, 74(3):425436, 1961.
 7. M. D. Davis, R. Sigal, and E. J. Weyuker. Computability, complexity, and languages
     Fundamentals of theoretical computer science. Computer Science ad scientic
    computing. Academic Press, 1994.
 8. J. P. Jones and Yu. V. Matijasevi£. Register machine proof of the theorem on ex-
    ponential Diophantine representation of enumerable sets. The Journal of Symbolic
    Logic, 49(3):818829, 1984.
 9. N. K. Kosovski. O Diofantovykh predstavleniyakh posledovatel'nosti resheni urav-
    neniya Pellya. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matem-
    aticheskogo Instituta im. V. A. Steklova AN SSSR (LOMI), 20:4959, 1971. (Rus-
    sian. Available in English translation as [10]).
10. N. K. Kosovski. Diophantine representation of the sequence of solutions of the
    Pell equation. J. of Soviet Mathematics, 1(1):2835, 1973. (Translated from [9]).
11. Ju. V. Matijasevi£. Enumerable sets are Diophantine. Soviet Mathematics. Dok-
    lady, 11(3):354358, 1970. (Translated from [15]).
12. Yu. Matijasevi£ and J. Robinson. Reduction of an arbitrary diophantine equation
    to one in 13 unknowns. Acta Arithmetica, XXVII:521553, 1975. Reprinted in [20,
    p. 235.].
13. Yu. V. Matiyasevich. Hilbert's tenth problem. The MIT Press, Cambridge (MA)
    and London, 1993.
14. Yu. Matiyasevich. Towards nite-fold Diophantine representations. Journal of
    Mathematical Sciences, 171(6):745752, Dec 2010.
15. Yu. V. Matiyasevich. Diofantovost' perechislimykh mnozhestv. Doklady Akademii
    Nauk SSSR, 191(2):279282, 1970. (Russian. Available in English translation as
    [11]; translation reprinted in [21, pp. 269273]).
16. Yu. V. Matiyasevich. Sushchestvovanie neèektiviziruemykh otsenok v teorii èkpo-
    nentsial'no diofantovykh uravneni. Zapiski Nauchnykh Seminarov Leningrad-
    skogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR (LOMI),
    40:7793, 1974. (Russian. Translated into English as Yu. V. Matiyasevich, Exis-
    tence of noneectivizable estimates in the theory of exponential Diophantine equa-
    tions, Journal of Soviet Mathematics, 8(3):299311, 1977).
17. Yu. V. Matiyasevich. Martin Davis and Hilbert's tenth problem. volume 10 of
    Outstanding Contributions to Logic, pages 3554. Springer, 2016.
18. J. Robinson. Existential denability in arithmetic. Transactions of the American
    Mathematical Society, 72(3):437449, 1952. Reprinted in [20, p. 47.].
19. J. Robinson. Diophantine decision problems. In W. J. LeVeque, editor, Studies in
    Number Theory, volume 6 of Studies in Mathematics, pages 76116. Mathematical
    Association of America, 1969.
20. J. Robinson. The collected works of Julia Robinson, volume 6 of Collected Works.
    American Mathematical Society, Providence, RI, 1996. ISBN 0-8218-0575-4. With
    an introduction by Constance Reid. Edited and with a foreword by Solomon Fe-
    ferman. xliv+338 pp.
21. G. E. Sacks, editor. Mathematical Logic in the 20th Century. Singapore University
    Press, Singapore; World Scientic Publishing Co., Inc., River Edge, NJ, 2003.


A      A quick account of the reduction, as proposed in [19],
       of exponentiation to any exponential-growth relation


Suppose that Q ⊂ N × N and S ⊂ N × N are such that


i)     Q(w, u) implies u > ww ,
ii)    w > 1 & u > w2 w implies Q(w, u) ;
iii)   S(p, q) implies p > 1 & q 6 pp ,
                                                                k
iv)    for each k > 0, there are p and q such that S(p, q) and p < q .


Then, as we will prove:

                                                   
            bn = c ⇐⇒ (∃ a , d , ` , r , v , s , t) (c − 1)2 + n = 0     ∨
                                                  (n > 1 & c + b = 0) ∨
                      
                          n > 1 & b > 1 & S(a, d) & d > `              &

                          `2 = (a2 − 1) r2 + 1 & r = (a − 1) s + n &             (@)
                          Q(b + n + 1 , v) & v = 2 a b − b2 − 1        &

                          a>b+n      &    v>c                          &
                                                                    
                          ` = (a − b) r + v t + c                        .

Lemma 2. The above bi-implication (@) holds if i), ii), iii), and iv) hold.
Proof. Assuming that n > 1 & b > 1, we must show that bn = c holds if and
                                                                                 2
only if: there are natural numbers a, d, `, r , and v = 2 a b − b − 1, such that the
                               2       2         2
conditions S(a, d), d > `, `  − (a − 1) r = 1, Q(b + n + 1, v) hold and, moreover,
n is the remainder of the integer division of r by a − 1 and c is the remainder of
the division of ` − (a − b) r by v .
     (`⇐='): By means of i), we get v > (b + n + 1)b+n+1 > bn ; by means of
                      a
iii), a > 1 and ` < a . Thus, since n > 1 implies r > 0, we get ` = xi (a) and
r = y i (a) for some i such that 0 < i < a; thereforetaking the congruence
y i (a) ≡ i (mod a − 1) into accounti ≡ n (mod a − 1), and hence i = n is the
                                                                n
remainder of the division of r by a−1. Since ` − (a − b) r ≡ b (mod v)thanks
                                              j                2
to the congruence xj (a) − (a − b) y j (a) ≡ b (mod 2 a b − b − 1) holding for all
j and, moreover, ` − (a − b) r ≡ c (mod v), c < v , bn < v , we conclude that
c = bn as desired.
     (`=⇒'): Notice that iii) and iv) imply that for every k there exists an innite
sequence
                             hp0 , q0 i , hp1 , q1 i , hp2 , q2 i , . . .
                                            k                                              9
in N × N such that S(pj , qj ), qj > pj , and pj+1 > pj hold for every j .                     Hence we
                                                                                 2n
can choose an a so large that: for some d, S(a, d) and d > a                          holds; a > n + b;
Q(b+n+1 , 2 a b−b2 −1) (to enforce this, by ii), it suces to pick an a such that
2 a b−b2 −1 > (b+n+1)2 (b+n+1) ) and, in consequence of i), 2 a b−b2 −1 > bn . To
satisfy all desired conditions, it will then suce to take ` = xn (a) and r = y n (a),
                                                        n                2
thanks to the congruence xn (a) − (a − b) y n (a) ≡ b (mod 2 a b − b − 1).

                                                                            10
     In order for Q to behave as wanted, it suces to put:

                                    
              Q(w, u) =Def (∃ x , y) u > w x                 &      x>1               &
                                                                          
                                            x2 − (w2 − 1) (w − 1)2 y 2 = 1 .

Lemma 3. As just dened, the Diophantine relation Q(w, u) satises i) & ii).
Proof. Suppose rst that Q(w, u) holds. From x > 1 it follows that w ∈/ {0, 1};
hence x = xn (w)   & (w − 1) y = y n (w) holds for some n > 0. Since y i (w) ≡
i (mod w − 1) holds for all i, we get n ≡ 0 (mod w − 1); therefore n > w − 1
                                 w
and, hence, u > w xw−1 (w) > w . This proves i).
    Suppose next that w > 1. By taking x = xw−1 (w) and y = y w−1 (w) /(w −1),
we easily check that Q(w, u) holds for every u > w xw−1 (w). Since xi (w) <
(2 w)i 6 w2 i holds for every i > 0, we get w xw−1 (w) < w w2 w−2 < w2 w ;
                                         2w
therefore, Q(w, u) holds for every u > w    . This proves ii).

 9
   To choose p0 , q0 so that S(p0 , q0 ) & q0 > pk0 , just rely on iv). Inductively, assuming
                                                        p
   S(pj , qj ) & qj > pkj , notice that pj 6= 0 & pj j > qj holds by iii), hence pj > k
                                                                                           pj
   follows; therefore, by choosing pj+1 and qj+1 so that S(pj+1 , qj+1 ) & qj+1 > pj+1        ,
                                                                            p
   we will enforce qj+1 > pkj+1 ; on the other hand, pj+1 6= 0 & pj+1         j+1
                                                                                  > qj+1 , and
   therefore pj+1 > pj .
10
   Notice that for w > 2 the inequality x > 1 amounts to the same as y > 0.
    From Lemma 3 and Thm 2, by taking the above implementation of Qwhere
we replace y by h + 1into account, we get straightforwardly:

Corollary 1. If S is a Diophantine relation satisfying iii) & iv), the following
rule provides a Diophantine representation of exponentiation:
                                       
    bn = c ⇐⇒ (∃ a , d , ` , s , x , h) (c − 1)2 + n = 0                              ∨
                                            (n > 1 & c + b = 0)                       ∨
                         
                             n > 1 & b > 1 & S(a, d) & d > `                          &
                                                      2
                                                                                      &
                                        
                             `2 = a2 − 1 (a − 1) s + n + 1

                             x2 = (b + n)3 (b + n + 2) (h + 1)2 + 1                   &

                             2 a b − b2 − 1 > (b + n + 1) x                           &

                             2 a b − b2 − 1 > c & a > b + n                           &
                                                                             
                                                                      
                             2 a b − b2 − 1 | ` −    a − b (a − 1) s + n − c   .

(Besides a, d, `, s, x, h, one needs one additional existential variable in the right-
hand side of this bi-implication in order to eliminate each inequality, plus one
more to eliminate the divisibility relator `|'. Thanks to the inequality a − b > 0,
we can also get rid of `, thus reducing the number of existential variables to 12.)



B     Davis's reduction of               bn = c to the relation r = y n (a)
The following crucial link between exponentiation and the sequence hy i (a)ii∈N
was pointed out in [3] and explained at length, again, in [4]:


                                                     
       b > 1 =⇒       bn = c ⇐⇒ (∃ t , a , ` , r , h )                r = y n (a) &
                                                          ` − (a − 1) r2 = 1 &
                                                           2      2

                                                               t>b        &   t>n &
                                           (t − 1) (t − 1) (h + 1) + 1 = a2 &
                                             2             2          2

                                                            c < 2 a b − b2 − 1 &
                                                                               
                                                                       2
                                      c ≡ ` − (a − b) r ( mod 2 a b − b − 1 )     .

                                  n
Specically, when b > 1 and b   = c, the constraints here appearing in the scope of
∃ can be satised in innitely many ways: for, corresponding to any t > n max b,
it suces to put a = xt−1 (t) in order to be able to determine the values of ` , r ,
and h uniquely (see Lemma 4 below).
      In light of the above biimplication, if we now provided a Diophantine repre-
                                                                                    n
sentation of the relation r = y n (a), we would readily get that the relation b         =c
is also Diophantine.


      Let us recall here the proof of the above-stated relationship between expo-
nentiation and the Pell equation. We begin with the proposition:

Lemma 4. If b > 1 and bn = c, then to each number of the form a = x(s+1) (t−1) (t)
with t > b max n there correspond uniquely values `, r, h such that the fol-
lowing conditions are met: r = y n (a), ` = xn (a), c < 2 a b − b2 − 1, c ≡
` − (a − b) r (mod 2 a b − b2 − 1), and a2 − (t2 − 1) (t − 1)2 (h + 1)2 = 1.
Proof. Observe that, since t > b > 1, the Pell equation x2 −(t2 −1) y 2 = 1 has the
usual innite sequence hhxi (t) , y i (t)iii∈N of solutions; therefore, it makes sense
to put a := x(s+1) (t−1) (t). In its turn a > 1 holds, because x(s+1) (t−1) (t) >
x1 (t) > 1; hence it makes sense to put r := y n (a) and ` := xn (a).
                              t−1
    Plainly, a > xt−1 (t) > t     > bn ; hence it is easy to see that the inequality
 n             2                11
b < 2 a b − b − 1 is satised when n > 0. The same inequality holds when
n = 0, as it follows from a > tt−1 > t > b > 1.
      The last two conditions in the claim simply state well-known congruences
that are satised (as recalled in Fig. 2) by the solutions of any Pell equation of
the special form being considered here. In particular,


                        c ≡ ` − (a − b) r ( mod 2 a b − b2 − 1 )

states that


                  bn ≡ xn (a) − (a − b) y n (a) ( mod 2 a b − b2 − 1 ).                 (◦)

           2
As for a − (t2 − 1) (t − 1)2 (h + 1)2 = 1, it merely expresses that y (s+1) (t−1) (t)
is a non-null multiple of t − 1; recall, in fact, that a = x(s+1) (t−1) (t) and
t − 1 > 0, and that the congruence y i (t) ≡ i (mod t − 1) holds in general, for
every i.

      We next come to the converse of Lemma 4:

Lemma 5. Suppose that b > 1 and that the conditions
                        c < 2 a b − b2 − 1,
                        c ≡ ` − (a − b) r ( mod 2 a b − b2 − 1 )
                        `2 − (a2 − 1) r2 = 1
                        a2 − (t2 − 1) (t − 1)2 (h + 1)2 = 1
                        t > b max n,

are satised by a, `, r, t, and h, where n is the value ensuring that r = y n (a).
Then bn = c holds.
11
     Here, as we will again do in the proof of Lemma 5, we are making use of the following
     fact (which gets easily proven even for a real number b): If n > 0, b > 1, and a > bn
     (with a, n ∈ N), then 2 a b − b2 − 1 > bn .
Proof. Since t > b > 1, the Pell equation x2 −(t2 −1) y 2 = 1 has the usual innite
                                                                2
                                                        − (t2 − 1) y 2 = 1 holds
sequence hhxi (t) , y i (t)iii∈N of solutions; thus, since a
for some y > 0, we have a = xj (t) for some j , where j > 0since a > tand
` = xn (a), r = y n (a) holds for a suitable n. Consequently 2 a b − b2 − 1 > 2;
moreover, by the well-known congruence (◦) recalled above, we have


                           c ≡ bn ( mod 2 a b − b2 − 1 ),

whence the sought equality will follow if we manage to prove that both sides
                                                  2
of this congruence are smaller than 2 a b − b         − 1 (as for c, this is an explicit
assumption). Since this is obvious when n = 0, we will assume n > 0.
                    n
    To see that b< 2 a b−b2 −1, we argue as follows. Clearly y j (t) = (t−1) (h+1)
holds, whence (t − 1) (h + 1) ≡ j (mod t − 1), i.e. t − 1 | j , follows. Since j 6= 0,
                                            j    t−1
we get j > t−1, and therefore a = xj (t) > t > t      > bn . The sought inequality
follows, which completes the proof.


Corollary 2. Put Q(w, h) := (w + 2)3 (w + 4) (h + 1)2 + 1 . Then,
                           
 b = c ⇐⇒ (∃ a , ` , r , h) (c − 1)2 + b + n = 0 ∨ (n > 1 & c + b = 0)
    n
                                                                                    ∨
                             
                              b > 1 & r = y n (a)                                   &

                                   `2 = (a2 − 1) r2 + 1 & Q(b + n − 2, h) = a2 &

                                   2 a b − b2 − 1 > c                               &
                                                                           
                                                                    2
                                   c ≡ ` − (a − b) r ( mod 2 a b − b − 1 )   .

Proof. Suppose rst that there are a, `, r, h satisfying the conditions in the scope
of `∃', and that b > 1. By putting t := b + n + 1, we obviously get t > b max n
        2
and a  − (t2 − 1) (t − 1)2 (h + 1)2 = 1, so that bn = c holds by Lemma 5.
                                n
   Conversely, suppose that b      = c holds, where b > 1. Put t := b + n + 1
and a := xt−1 (t). Then, by Lemma 4, unique values `, r, h exist satisfying all
conditions that appear in the third disjunct of the scope of `∃' in the claim.



C       Representing exponentiation as an integer quotient


In the ongoing, in order to prove that

                              $                                       %
                                  y n+1 8 b (n + 1) y n+1 (b + 1) + 2
             bn = c ⇐⇒ c =                                             ,
                                  y n+1 8 (n + 1) y n+1 (b + 1)
we will proceed to show, for b and n natural numbers, that

                                            y n+1 (b x + 2)
                           bn = limx→∞                      ;
                                               y n+1 (x)
this, in the light of the corollary which follows, will give us


                          bn = by n+1 (b x + 2) / y n+1 (x)c                     (*)

                                                                                  n
where x is a natural number sucently large to reduce the distance between b
and y n+1 (b x + 2)   / y n+1 (x) to an amount less than 1. We will carefully assess
how to take the value of x big enough. Our treatment adheres closely to [13,
pp. 3132].

   We begin by recalling, from fact 1 of Fig. 2:

Lemma 6. For a > 2 and i ∈ N, the following inequalities hold:
                            (2 a − 1)i 6 y i+1 (a) 6 (2 a)i .

Here the increase on the left is strict when i > 0; on the other side, when i > 1.
Corollary 3. For b, n, x ∈ N with x > 2,
                                 y n+1 (b x + 2)
                                                 > bn .
                                    y n+1 (x)

Proof. Thanks to Lemma 6, we have
                                                n          n
                  y n+1 (b x + 2)   (2 b x + 3)     (2 b x)   n
                                  >         n     >       n =b .
                     y n+1 (x)         (2 x)         (2 x)

   Assessment of a value of x which ts our needs (cf. [13, p. 32]):


                       
                       =
                                 1             for b = 0     and x > 2 ;
       y n+1 (b x + 2)           4n
                         <    (2 x−1)n      < 1 for b = 0 < n and x > 2 ;
          y n+1 (x)                16 n
                            n
                                          
                         6 b 1 + 2x             for b > 0 < n and x > 8 n .
                       

                                                                n
Thus (*) becomes true as soon as x > 8 (n + 1) (b + 1) ; we can, e.g., enforce
                                                                             n
it by putting x := 8 (n + 1) y n+1 (b + 1), thus getting the formulation of b = c
shown at the beginning of this appendix.