Consider an ( + 1)-ary relation ℛ over the set N of natural numbers. Does there exist an arithmetical formula (0, . . . , , 1, . . . , ), not involving universal quantifiers, negation, or implication, such that the representation and univocity conditions, viz.,
are met by each tuple ⃗ = ⟨0, . . . , ⟩ ∈ N+1 ?
A priori, the answer may depend on the richness of the language of arithmetic: Even if solely addition and multiplication operators (along with the equality relator and with positive integer constants) are adopted as primitive symbols of the arithmetical signature, the graph ℛ of any primitive recursive function is representable; but can representability be reconciled with univocity without calling into play one extra operator designating either the dyadic operation ⟨ , ⟩ ↦→ or just the monadic function ↦→ associated with a fixed integer > 1? As a preparatory step toward a hoped-for positive answer to this question, one may consider replacing the exponentiation operator by a dyadic relator designating an exponential-growth relation (a notion made explicit by Julia Bowman Robinson in 1952).
We will discuss the said univocity, aka ‘single-fold-ness’, issue—rfist raised by Yuri V. Matiyasevich in 1974—, framing it in historical context.
MS Classification 2020: 03D25, 11D25
The notions of being listable, exponential Diophantine, and polynomial Diophantine were
proved, in the decade 1960/1970, to capture the same family of relations on the set N of natural
numbers (see [
∃ 1 · · · ∃ ′(0, . . . , , 1, . . . , ) = ′′(0, . . . , , 1, . . . , ) holds for all 0, . . . in N . If also exponentiation—with variables in the exponent—is allowed to occur in ′ and ′′, then is said to be exponential Diophantine.
A function from N to N is termed likewise if its graph, namely the relation {⟨1, . . . , , 0⟩ : (1, . . . , ) = 0} is Diophantine or, resp., exponential Diophantine.
A valid biimplication of the form just shown is called a Diophantine representation (resp.,
an exponential Diophantine representation) of . Any listable relation admits an exponential
Diophantine representation, as was first proved in [
∃ ∃ ∃ ⃗ [ (⃗, ⃗, ) = 0 & J( , ) ] ,
where is a polynomial (multivariate, with coeficients in Z), hence devoid of exponentiation,
while exponentiation is superseded by any fixed exponential-growth relation (a notion
that Julia Robinson proposed in [
∃ ∃ ∃ ⃗ [ (⃗, ⃗, ) = 0 & 2 = ] , where is a polynomial, while ensuring single-fold-ness, henceforth dubbed univocity, that is: there is at most one solution to the constraint (⃗, ⃗, ) = 0 & 2 = , for any ⃗.
Now and then our focus will zoom in on finite-fold specifications, which are the ones admitting at most a finite number of solutions for each tuple ⃗ of actual parameters.
Examples of exponential-growth relations are:
E1 = {︀ ⟨ , 2⟩ : ∈ N ∖ {0, 1} }︀
and E2 = {︀ ⟨ , 2 ⟩ : ∈ N ∖ {0, 1} }︀ ,
1Bold symbols often diferentiate, henceforth, actual from formal parameters; to wit, values from variables.
2Here and below, ⃗ and ⃗ shorten 0, . . . , and 1, . . . , , respectively.
3Or even to the more elegant format ⃗ ∈ ⇐⇒ ∃ ∃ ⃗ [ (⃗, ⃗) = 4 + ] , see also [7, pp. 137–138].
where is the Fibonacci progression defined by the recurrence 0 = 0 , 1 = 1 , and +2 =
+ +1 for ∈ N . The relation E1 suggests the feasibility of an amalgamation—nowhere
described in the literature, as far as the authors know—between the cited results of [
Polynomial Diophantine univocity—or, at worse, finitefold-ness—is the true challenge; this
is why we also seek a relation that can play, in this respect, a role analogous to E2: a relation
M which in addition to satisfying exponential growth, as well as any other requirements that
might emerge from the amalgamated theorem (a potential such requirement is tagged (‡) in
Sec. 7) admits a finite-fold, hopefully univocal, polynomial specification. After a suggestion
provided by [
————————
The paper is organized as follows. Sec.2 illustrates, through a gallery of short examples, which kind of relations on N can be represented univocally by means of Diophantine polynomials without resorting to overly sophisticated tools. It is contended that when univocity does not come for free, it can be built into such a representation by insertion of clauses that insist on the minimality of the values to be assigned to the “unknowns” 1, . . . , ; minimality can be enforced by means of bounded universal quantifiers, but can these quantifiers be recast just in terms of addition, multiplication, and existential quantification? Sec. 3 shows that a number-theoretic construct somehow related to bounded universal quantification does, in fact, admit a univocal exponential Diophantine representation: the construct we are referring to is the function (, , ) = ∏︀
=1( + · ), and clues about its kinship to bounded universal quantification are deferred to a later section. Sec. 4 digresses into presenting a special format, known as the Davis normal form, which can be used to represent the graph of any primitive recursive function. This is, in essence, a technique for specifying any listable relation in a manner that seemingly deviates from a Diophantine representation, as it involves one bounded universal quantifier. Sec. 4 also recaps a variant of the Davis normal form, enforcing univocity, derived by Yu. Matiyasevich from his momentous finding that every listable relation is Diophantine. All prerequisites are ripe enabling us to produce, in Sec. 5, a univocal exponential representation of any Diophantine—hence of any listable—relation , through reduction of the bounded universal quantifier to the said construct (, , ). At this point one of Matiyasevich’s variants, embodying univocity, of the DPR theorem has been reached; in Sec. 6 we recall a more refined one, in which exponentiation is relegated, within a representation of , into a single literal of the form 2 = . Two questions are then raised in Sec. 7: Could a suitable condition M (, ) supersede this literal in the general representation scheme? And also: Can we manage to place a finite-fold Diophantine relation M (, ) in this role? The truly original part of this paper is Sec. 8, where we review the entire catalog of our candidate M ’s.
Let us start with motivating examples of univocal (polynomial first, then exponential) Diophantine specifications of various relations over N . Before doing so, we observe that Diophantine relations can safely be nested one inside another; moreover, we can unconditionally admit the conjunction connective ‘&’ in the specification language, in view of the equivalence ︀[ ∃ ⃗ ′(⃗, ⃗) = ′′(⃗, ⃗)]︀ & [︀ ∃ ⃗ ′(⃗, ⃗) = ′′(⃗, ⃗)]︀ ⇐⇒ ∃ ⃗ ∃ ⃗ [︀ ′(⃗, ⃗)2 + ′′(⃗, ⃗)2 + ′(⃗, ⃗)2 + ′′(⃗, ⃗)2 = 2 · (︀ ′(⃗, ⃗) · ′′(⃗, ⃗) + ′(⃗, ⃗) · ′′(⃗, ⃗))︀] . While these broadenings of the specification language do not afect univocity, the disjunction connective can be brought into play but should be handled with care: simple-minded use of the rewriting rule ′ = ′′ ∨ ′ = ′′ ⇝ ′ · ′ + ′′ · ′′ = ′ · ′′ + ′′ · ′ might, in fact, endanger univocity. E.g., restating = 0 ∨ ∃ = + 1 as ∃ · = · ( + 1) would not work, because could take any value in N when = 0 ; this violation of univocity can easily be cured, though: we can overload the first disjunct with the requirement = 0 before eliminating the propositional connectives, thus getting ∃ ( + ) · = ( + ) · ( + 1) .
Using ‘:=’ to mean “stands for”, we now provide the specifications of some basic relations among which divisibility, ‘|’, coprimality, ‘⊥’, and the graphs of integer quotient ‘÷ ’ and remainder operation ‘ % ’: ∈ ∅ := = + 1 ; ∈{0, . . . , ℓ} := ⋁︀⩽ℓ = ; ⩽ := ∃ + = ; < := + 1 ⩽ ; ̸= := 2 · · < 2 + 2 ; = □ := ∃ 2 = ; ̸= □ := ∃ (2 < & ⩽ 2 + 2 · ) ; 1 max 2 = := ∈ {1, 2} & 1 ⩽ & 2 ⩽ ; ÷ = := ∃ (︀ · + = & < )︀ ; % = := ∃ (︀ · + = & < )︀ ; ⊥ := ∃ 1 ∃ 2 ∃ 1 ∃ 2 (︀ 1 · + 1 · = 2 · + 2 · + 1 )︀ ; ∤ := ∃ ∃ (︀ · + + 1 = & + 1 < )︀ ; | := ∃ · = ; ≡ mod := | ± ( − ) .
Among these, the specifications lacking univocity are the ones of ‘ |’ (insofar as · = holds for any when = = 0), of ‘mod’ (unless one imposes ̸= 0), and of ‘⊥’. To fix them, put: ⊥ := ∃ ∃ (︀ 2 2 + 1 = 22 + 2 · · & < )︀ ; | := ( + ) · ( % ) = 0 .
The former states that the equation ± = 1 has a solution (necessarily unique) such that < ; the definiens of the latter is plainly rewritable in primitive symbols, retaining univocity.
Generally speaking, univocity can be enforced in an existential definition that lacks it by insisting on the minimality of the values assigned to the existential variables, but this brings into play bounded universal quantifiers; 4 and it is far from obvious (see Sec. 5 below) how these can be disempowered into arithmetical constructs. As 4Bounded quantifiers can be introduced as usual; in particular: ∃ ⩽ := ∃ ( ⩽ & ). ∀ ⩽ := ∀ ( ⩽ =⇒ ) and an illustration of this point, consider the following Diophantine specification (alternative to the one proposed above) of the property of not being a perfect square: ̸= □
The theory of Pell equations (see, e.g., [11, Sec. 3.4]) ensures the correctness of this characterization; however, the number of solving triples is infinite for each non-square number and it is daredevil to introduce univocity by reformulating the definiens as ∃ ∃ ∃ [︀ 2 = · ( + 1)2 + 1 & = + 1 & ∀ ′ < ∀ ′ < (︀ ′2 ̸= · (′ + 1)2 + 1)︀ ]︀ .
Suppose now that an exponentiation operator is adopted as a primitive arithmetical construct, along with a symbol designating the integer value 2 . Then addition and multiplication can be the following univocal exponential Diophantine specifications make evident: viewed as derived constructs and no other constant is essential (since = 1 + · · · + 1), as = 0 := = 1
:= · = := + = := i.e., + = := ∃ ∃ (︀ = = 2 & 2 = ︀) ; ∃ ∃ ∃ (︀ 2 = = 2 & 2 ∃ ∃ (︀ 2 = & 2 ∃ ∃ ∃ (︀ 2 = & 2 = & = ︀) ;
= & 2 ∃ ∃ ∃ ∃ ∃ (︀ 2 = & 2 = & 2 = & = )︀ ; = & · = )︀ , = & 2 = & 2 = & = )︀ .
It is an easy task to figure out from the above table the following fact, that states more explicitly—and enhances with univocity—what is observed in [1, p. 427]: Lemma 1. Any exponential Diophantine specification ∃ 1 · · · ∃ (0, . . . , , 1, . . . , ), whose matrix is devoid of quantifiers and only involves the logical connectives =, & , ∨ , can be recast as
∃ 1 · · · ∃ ∃ 0 · · · ∃ ℓ [︀ 0 = 2 & & ⩽ = ]︀ , where 0, . . . , , 0, . . . , , 0, . . . , are variables drawn from the {0, . . . , , 1, . . . , , 0, . . . , ℓ}, and where , , are distinct signs for each .
If the source specification is univocal, so is the “flattened” one resulting from this recasting. set ⊣
Very early on [4, pp.446–447], J. Robinson noted that binomial coeficient and factorial function are existentially definable in terms of exponentiation. The following univocal specifications are reminiscent of hers, but we rely, as for the factorial, on the modernized variant provided in [11, pp. 145–146]. The well-known binomial theorem justifies the first specification recalled here: ︀( ℓ)︀ = := ∃ [︀ = (︀ ( + 1)ℓ ÷ )︀ % & = 2ℓ + 1]︀ ; ! = := = (︀ (2 ))︀ ÷ ︂( (2 ) )︂] ︂[
.
Constructs more general than ! are the falling factorial ∏︀<( − ) with ⩾ , and the related raising factorial ∏︀
=1( + ) . Concerning an even more general construct, we have: Lemma 2 (Originating from [12, Lemma 2.2]—Enhanced, here, with univocity). Given , , , , the relationship
∏︀=1( + · ) = holds if and only if there exist—and are uniquely determined—, , , , , such that [︁ · = + 1 & = · ( + · ) + 1 & · = + · & [︀ · ! (︀ + )︀] % = &
︀[ ( + + 1 = & = 0) ∨ ( = + & + + 1 = )]︀ ]︁.
Proof. The first disjunct, regarding the case = 0 ∨ = 0, does not deserve explanation; the second refines the existential specification of ∏︀
=1( + ) , ∃ ∃ ∃ = ( + ) + 1 & = + & ︂[ ! ︂( ︂( + )︂] % = , ︂) proved in [11, pp. 147–149] for the case > 0 & > 0 . That specification leaves and under-determined; we are now ensuring univocity by indicating that if one tried to assign a smaller value to , then either the value of itself or the corresponding value of would turn out to be negative. ⊣
In Sec. 4, we will exploit three computable functions admitting univocal exponential specifications; they are an injection from N2 onto N and its associated projections (see [13, Sec. 3.8]): ( , ) = := () = () = := := ∃ 2 (2 + 1) = + 1 .
2 (2 + 1) = + 1 ; 2 | + 1 & 2+1 ∤ + 1 ; These definitions yield, for all , , ∈ N , that:
( , ) = < ′ & < ′ =⇒ ⇐⇒ () = & () = ,
( , ) < (′ , ) & ( , ) < ( , ′) .
Intuitively speaking, a set R ⊆
N+1 is listable if there is an efective procedure for making a list (with repetition allowed) of the elements of R . Computability theory provides the notion of recursively enumerable (r.e.) set as a formal counterpart—satisfactory, by the Church–Turing thesis—of this intuitive notion. Here is one among various equivalent ways of characterizing it: primitive recursive functions 0, . . . , from N to N such that Characterization 1. An ( + 1)-ary relation R on N is called r.e. if either R = ∅ or there are R =
{⟨0(), . . . , ()⟩ : ∈ N} .
As this definition suggests, we mainly refer to monadic functions henceforth; hence we can rely on an ad hoc characterization of primitive recursiveness, that we borrow from [13, Sec. 4.9]: Characterization 2. Put n() = 0 and s() = + 1 for each ∈ N. Primitive recursive functions are all and only those functions from N to N that either belong to the initial endowment n( ) , s( ) , and ( ) , ( ) (see above, end of Sec. 3), or are obtainable from that endowment through repeated use of the following three operations: 1. composing ( ) and ( ) into the function ∘ that sends every to (︀ ())︀ ; 2. pairing ( ) and ( ) into the function ⊗ that sends every to (︀ (), ())︀ (see p. 6); 3. obtaining by recursion from ( ) and ( ) the function ℎ() := ⎧ 0 ⎪ ⎨ (︀ −2 1 )︀ ⎪⎩ (︀ ℎ (︀ )︀ 2 if = 0 , if ∈ { 1, 3, 5, 7, . . . } , if ∈ { 2, 4, 6, 8, . . . } .
We then have: Theorem 1. The graph ℱ (a , ) ⇐⇒ (a) = of any primitive recursive function from N into N can be specified by means of an arithmetical formula within which all universal quantifiers are bounded and negation does not occur (nor does implication; usage of the conjunction and disjunction connectives & , ∨ is subject to no restraints, also existential quantification can be used with no restraints, because we are assuming as a primitive sign ∃ as well as ∀).
Proof. The graphs of the initial functions n( ) , s( ) , ( ), and ( ) can be specified, respectively, by a + = a , a + 1 = , ∃ ∃ ︀( Pow(, ) & · (2 + 1) = a + 1 )︀ , and ∃ ∃ ︀( Pow(, ) & · (2 + 1) = a + 1 )︀ , where Pow (a, ) is a formula describing the graph of 2a—this function gets the value 1 when a = 0 and gets the value 2 · 2 when a = + 1 . By exploiting the Chinese remainder theorem in the manner explained in [5, pp. 79–80],5 we get the specification Pow (a, ) := ∃ ∃ [︁ 1 = % (︀ 1 + )︀ & = % (︀ 1 + (a + 1) · )︀ & ∀ ⩽ a ︁( % (︀ 1 + ( + 2) · )︀ = 2 · [︀ % (︀ 1 + ( + 1) · )︀] ︁)]︁ .
As for the mechanisms enabling the immediate construction of primitive recursive functions out of ( ) and ( ) that are supposed to satisfy the induction hypothesis, we so specify the graph of ∘ : ∃ ︀( (a) = & () = )︀ , graph of ⊗ : ⎧ ⎨ ∃ ∃ ∃ ⎩ [︁ (a) = & (a) = &
Pow(, ) & · ( + + 1) = + 1]︁ , 5A corollary, originating from Gödel (1931), of the Chinese remainder theorem says: Consider integers 0, . . . , such that 0 ⩽ < holds for each , and put = 1 + ! · · ( + 1) . Then 0 = % 0, . . . , = % hold together for a sole < ∏︀⩽ . and then conclude by so specifying the outcome of recursion: ∃ ∃ ∃ [︁ 0 = % (︀ 1 + )︀ & = % (︀ 1 + (a + 1) · )︀ & = a ÷ 2 & ∀ ⩽ ︁( () = % (︀ 1 + (2 · + 2) · )︀ &
︀( % (︀ 1 + ( + 2) · )︀ = % (︀ 1 + (2 · + 3) · )︀ )︁]︁ .
Needless to say, here the Chinese remainder theorem is at work again.
In light of the elicitation Char. 1 of listability, Thm. 1 can easily be generalized into: Theorem 2. Every listable (property or) relation on N can be specified by means of an arithmetical formula wherein all universal quantifiers are bounded and neither negation nor implication occurs. such that:
In [5, pp. 93–96], a syntactic manipulation algorithm is described that transforms any arithmetical formula
endowed with the features stated in Thm. 1 (and in Thm. 2), and whose free variabes are 0, 1, . . . , , into a Diophantine polynomial (ℎ, , 0, . . . , , 1, . . . , ) (0, . . . , ) ⇐⇒
∃ ℎ ∀ ⩽ ℎ ∃ 1 ⩽ ℎ · · · ∃ ⩽ ℎ [︀ (ℎ, , 0, . . . , , 1, . . . , ) = 0 ].
This special format is called Davis normal form, because it was first brought to light (originally
lacking bounds on the inner existential quantifiers) in [ 14, Part III]. We will now report on a
perfectioning of this format, that Yuri Matiyasevich put forward after establishing that the a
priori distinct notions of r.e. set and Diophantine set amount to one another (cf. [
Ancillary to that, let us introduce the Cantor functions cℓ, with ℓ ∈ N ∖ {0} : ⊣ c1(1) := 1 ,
︂( c+2(1, . . . , +2) := c+1 1, . . . , , (+1 + +2)2 + 3 · +1 + +2 )︂ 2 .
It thus turns out that each cℓ is a monotone injection of Nℓ onto N . Yu. Matiyasevich stated: 0, . . . , and 0, 1, . . . , , respectively):6 Lemma 3 ([15, pp. 303–304]). To each Diophantine polynomial (0, . . . , , 1, . . . , ), there correspond Diophantine polynomials (ℎ, , 0, . . . , , 0, 1, . . . , ) ⩾ 0 and (0, . . . , , ℎ) ⩾ 0 such that the following biimplications hold (where ⃗ and ⃗ shorten ∃ 1 · · · ∃ (⃗, 1, . . . , ) = 0 ⇐⇒ ⇐⇒ ⇐⇒ ∃ ℎ ∀ ⩽ ℎ ∃ ⃗ (ℎ, , ⃗, ⃗) = 0 ∃! ℎ ∀ ⩽ ℎ ∃ ⃗ (ℎ, , ⃗, ⃗) = 0 ∃ ℎ ∀ ⩽ ℎ ∃! ⃗ (ℎ, , ⃗, ⃗) = 0 ⇐⇒
∃ ℎ ∀ ⩽ ℎ ∃ 0 ⩽ (⃗, ℎ) ∃ 1 ⩽ (⃗, ℎ) · · · ∃ ⩽ (⃗, ℎ) (ℎ, , ⃗, ⃗) = 0 . Proof. We will define (ℎ, , ⃗, 0, 1, . . . , ) so that = 0 enforces univocally (also with respect to the new existential variables, ℎ and 0) the condition c (1, . . . , ) = & [︀( < ℎ & (⃗, 1, . . . , ) ̸= 0)︀ ∨ (︀ = ℎ & (⃗, 1, . . . , ) = 0)︀] . 6The sign ‘∃!’ (read: “there exists a sole”) can be introduced as usual: ∃! := ∃ ∀ ( ⇐⇒ = ).
For this purpose, we put7 := 22 · (︀ − c (1, . . . , )︀) 2+
︀[ (ℎ − ) · 2(⃗, 1, . . . , ) − 0 − 1]︀ 2 · [︀ (ℎ − )2 + 2(⃗, 1, . . . , ) + 0]︀ .
It is then clear that the variables ℎ, 1, . . . , , and 0 on the right-hand side of the claimed biimplications designate, respectively: the first such that the -tuple ⟨^1, . . . , ^ ⟩ for which c (^1, . . . , ^ ) = holds solves the equation (⃗, 1, . . . , ) = 0 (in the unknowns 1, . . . , ); for each ⩽ ℎ, the -tuple ⟨,1, . . . , , ⟩ such that c (,1, . . . , , ) = ; the accordance between positivity of ℎ − and non-nullity of (⃗, ,1, . . . , , ). When the left-hand side of each claimed biimplication is satisfied by specific ’s, we can hence determine— and they are unique—a value for ℎ and, corresponding to each , values , ’s that do to the case of the right-hand side; conversely, if ℎ satisfies the right-hand side for given ’s, then the corresponding ℎ,1, . . . , ℎ, are such that (⃗, ℎ,1, . . . , ℎ, ) = 0 . To end, we must address the issue of setting a suitable bound (⃗, ℎ) on the variables . Since no , with > 0 can exceed ℎ, we will enforce (⃗, ℎ) ⩾ ℎ; to also take into proper account the values ,0 , we put (⃗, ℎ) := ℎ · (︀ 1 + ̃︀(⃗, ℎ))︀ , where ̃︀(⃗, ℎ) results from the polynomial 2(⃗, ℎ, . . . , ℎ) through replacement of each one of its coeficients, , by the absolute value || . ⊣
The proof that the family of exponential Diophantine relations is closed under bounded universal
quantification can be developed in many diferent ways (see [ 16, Chap.6]). Here we resume part
of the development (Lemmas 4 e 5) from the recent monograph [
Lemma 4. (Cf. [11, p.154]). To each Diophantine polynomial (ℎ , , 1 , . . . , , 1 , . . . , ) there correspond Diophantine polynomials (ℎ , , 1 , . . . , ) such that the following hold: • (ℎ , , 1 , . . . , ) > ℎ max ; • (ℎ , , 1 , . . . , ) ⩾ | (ℎ , , 1 , . . . , , 1 , . . . , )| when ⩽ ℎ and 1 , . . . , ⩽ .
Proof. (Just a clue). The trick is similar to the one used at the end of the proof of Lemma 3. ⊣ Lemma 5 (From [11, pp. 150–153]). If and are as in Lemma 4 then, given ℎ, , 1, . . . , , ∀ ⩽ ℎ ∃ 1 ⩽ · · · ∃ ⩽ (ℎ , , 1 , . . . , , 1 , . . . , ) = 0 will hold if and only if there exist , , 1 , . . . , such that (1) = (ℎ , , 1 , . . . , ) ! ; (2) 1 + ( + 1) = ∏︀⩽ℎ ︀( 1 + ( + 1) )︀ ; (3) (ℎ , , 1 , . . . , , 1 , . . . , ) ≡ 0 mod 1 + ( + 1) ; 7The factor 22 abundantly sufices to elide the denominator of the polynomial c . (4) 1 + ( + 1) ⃒⃒⃒ ∏︀⩽( − ) , for = 1, . . . , .
Lemma 6. Out of any given Diophantine polynomial (1, . . . , , 1, . . . , ) , one can construct three polynomials, (ℎ, , 1, . . . , , 0, 1, . . . , ) , (1, . . . , , ℎ) , and (ℎ, , 1, . . . , ), each producing values in N when its variables range over N, such that ∃ 1 · · · ∃ (1, . . . , , 1, . . . , ) = 0 holds if and only if there exist uniquely determined ℎ , , , , 0 , . . . , , 0 , . . . , , 0 , . . . , , and satisfying the following exponential Diophantine conditions: ⊣ (1) = (1, . . . , , ℎ) & = (ℎ , , 1 , . . . , ) ! ; (2) = 1 + ( + 1) & = ∏︀ℎ=+11 (︀ 1 + )︀ ; (3) | (ℎ , , 1 , . . . , , 0 , 1 , . . . , ) ; (4) + = & ⃒⃒⃒ ∏︀⩽ ︀( + ︀) , for = 0, 1, . . . , ;
[︁ ]︁ (5) ⋁︀⩽ ︀( & < = + )︀ & + + 1 = & & =+1 = 0 .
Proof. From —assuming without loss of generality that > 0—we obtain and as in Lemma 3, then we get from as in Lemma 4 (there is but one extra variable, 0). Now we can apply Lemma 5, with = (1, . . . , , ℎ), and this accounts for the conditions (1)–(4). By means of the , we are requiring that ⩾ ; this is a legitimate request, in the light of the proof of Lemma 5, whose congruence ( , , 1 , . . . , , 0 , 1 , . . . , ) ≡ 0 mod is rewritten as a divisibility constraint between natural numbers here, by taking the fact (ℎ , , 1 , . . . , , 0 , 1 , . . . , ) ⩾ 0 into account; moreover, within that proof we had represented each − , in the form − with 0 ⩽ ⩽ , here we are representing it in the form + with 0 ⩽ ⩽ .
As Lemma 3 suggests, in order to make the specification (1)–(4) univocal, it is enough to bring into play new unknowns 0, . . . , subject to the constraint (5). That is, we are choosing as representative of the infinitely many ( + 1)-tuples ⟨0, . . . , ⟩ suitable to encode the list of tuples ⟨0,, . . . , ℎ,⟩ ( = 0, . . . , ) as described within the proof of Lemma 5, the one whose components cannot be lowered by the amount without at least one among them becoming smaller than . ⊣
Knowing that each listable has a representation ∃ ⃗ (⃗ , ⃗) = 0 , we can view Lemma 6 as
enriching the DPR theorem [
Denote by ⟨()⟩∈N the endless, strictly ascending, sequence consisting of all non-negative integer solutions to the Pell equation8 (2 − 1) 2 + 1 = □ with ∈ N ∖ {0, 1} ; 8Once more, ‘ = □ ’ means that must be a perfect square.
Moreover, if ⩾ 1 & ⩾ 3 ( + 1)( + 1) , then = ⇐⇒ = +1( + 1) ÷ +1() . Proof. Concerning the first claim, the proof can be traced back to [ 4, Lemmas 9 and 10] (see also [3, Lemma 3]). Concerning the second claim, see [15, p. 308].
Through the first claim of Lemma 7, Martin Davis got a very neat and general restatement of the DPR theorem, where a single literal involving an exponential-growth relation J( , ) supersedes exponentiation. Together with J( , ) , Davis’ technique exploits a Diophantine relation D ( , , ) on N, such that9 • ∀ ∀ ∃ D (, , ) , • ∀ ∀ ∀ ∀ ︀[ > & D (, , ) =⇒ > ]︀ and along with the Diophantine relation
E (, , , , ℓ) :=
∃ ∃ ∃ [︀ (︀ = = = = 0 & = + 1)︀ ∨ It can be shown that & ⩽ = ⇐⇒ (∃ , 0, . . . , , ℓ0, . . . , ℓ) & ⩽ D(, , ) & > & ︀( 2 − (2 2 − ℓ ⩽ < ℓ & = ÷ ℓ 1) 2 = 1 & = 0 &
︀] .
︂[ E (, , , , ℓ) & ℓ = () , √︁ also put ():=
(2 − 1) 2 () + 1. Then: Lemma 7. The following law determines uniquely the values of , : ︀( ( ⩾ 1 ∨ = 0) & > )︀ =⇒ ⎢ ⎢ ⎣ () ⩽ < () & = ÷ () whence () can be eliminated thanks to the following: Lemma 8 (Cf. [18, Lemma A.2]). Suppose that > 1, > , and () > ℓ . Then, ℓ = () ⇐⇒
∃ ℓ2 − (2 − 1) (︀ + ( − 1) )︀ 2 = 1 .
︂[
Q(, ) := (∃ , ) ⩾ & > 1 & 2 − (2 − 1) ( − 1)2 2 = 1 . 9For definiteness, one could take D(, , ) := Q( + + 2, ) , where Q(, ) is as in [7, p. 155], namely: Ultimately, one gets the following proposition, whose proof we omit: & ⩽ [︁
D(, , ) & > & > & E (, , , , ℓ) & ℓ < & ℓ2 = (2 − 1) [︀ + ( − 1) ]︀ 2 + 1 ]︁ ]︂ .
Lemma 9. If J( , ) is an exponential-growth relation and each , , is either a variable or a non-negative integer constant, then we have
& ⩽ = ⇐⇒ (∃ , , 0, . . . , , ℓ0, . . . , ℓ, 0, . . . , ) J( , ) &
Therefore, in view of Lemma 1: Theorem 4 (Davis, 1963). Each listable subset of a Cartesian power N+1 admits a specification of the form ∃ ∃ ∃ ⃗ [︀ (⃗, ⃗, , ) = 0 & J( , ) ]︀ , where is a Diophantine polynomial and J is any exponential-growth relation.
In one respect, this achieves more than Thm. 3; in fact, here we have a generic exponentialgrowth relation in place of exponentiation. But, regrettably, univocity is not ensured.
Matiyasevich made a leap towards a reconciliation between Thm. 3 and Thm. 4 in [15, pp. 308– 309]. In his theorem, reported below, the specific relation 2 = occurs instead of a generic J( , ) ; and in its proof (which we omit) the second claim of Lemma 7 plays a decisive role: Theorem 5 (Exponentiation, from dyadic to monadic). A univocal exponential Diophantine specification of any relation & =1 = (where , , are as said above) is: ℒ2 := 2 = , ℒ3, := [( = 0 & = 1 ) ∨ ( > 0 & = 0 )] & = = = ℎ = 0 , ℒ4, := = ÷ ℎ , ℒ5, := 2 − ︀( ( + 1)2 − 1︀) 2 = 1 & 2 − ︀( 2 − 1︀) ℎ2 = 1 , ℒ6, := ≡ + 1 mod ( ) & ℎ ≡ + 1 mod ( − 1) , ℒ7, := < & ℎ < .
Consequently, every listable subset of a Cartesian power N+1 admits a univocal representation ∃ ∃ ∃ ⃗ [︀ (0 , . . . , , ⃗, , ) = 0 & 2 = ]︀ , where is a Diophantine polynomial.
We are after a generalized variant of Thm. 5 which has, in place of its
ℒ1 & 2 = & & =1 [( = 0 & ℒ3, ) ∨ ( > 0 & ℒ4, & ℒ5, & ℒ6, & ℒ7, )] , a suitable formula ( ⃗ , ⃗ , , ) = 0 & M ( , ) , where is a Diophantine polynomial in the parameters ⃗ and • M is a dyadic relation subject to particular requirements—probably stronger than exponential-growth. Moreover, • a concrete such M should be exhibited that admits a finite-fold —hopefully univocal—
Diophantine polynomial specification.
The achievement of these two goals would answer positively an issue raised in [
As regards which requirement should be imposed on M , [9, p. 749] suggests the following
(without explaining, though, why this would be adequate to ensure that the relation 2 = —and
therefore any listable set—has a finite Diophantine specification if M ( , ) has one):
⃦⃦ Integers > 1 , ⩾ 0 , ⩾ 0 , > 0 exist such that to each ∈ N ∖ {0}
⃦⃦ there correspond , such that: M ( , ) , < , and > hold.
As for a concrete choice of M , the most promising candidate at the time when [
In [19], Martin Davis argued that Hilbert’s 10th problem would turn out to be algorithmically
unsolvable if his quaternary quartic just recalled could be shown to admit only one solution in
N (an expectation, btw, that came to an end in the early 1970s). In [
Number associated with the respective Pell equations 2 + 1 = □ turned out to admit only a finite number of solutions in Z, then every listable set—first and foremost the set of all triples ⟨, , ⟩ ∈ N3 such that = —would admit a finite-fold polynomial Diophantine representation.
If the equation associated with has a finite overall number of solutions, then the following dyadic relation M over N admits a polynomial Diophantine representation: ∈ {2, 7} : ∈ {3, 11, 19, 43} :
M(, ) := M(, ) := ∃ ℓ > 4 [︁ = ̃︀2ℓ () & | & ⩾ 2ℓ+1 ]︁ , ∃ ℓ > 5 [︁ = ̃︀22 ℓ+1 () & | & ⩾ 22 ℓ+2 ]︁ , where ⟨̃︀()⟩∈N is the endless, strictly ascending, sequence consisting of all solutions in N to the said equation 2 + 1 = □ . Independently of representability, each M turns out to satisfy Julia Robinson’s exponential growth criteria and Matiyasevich’s condition (‡) seen above.
It is very hard to guess whether the number of solutions to any of the six quartics shown above is finite or infinite. For quite a while the authors hoped that Matiyasevich’s surmise that each r.e. set admits a single-fold polynomial Diophantine representation could be established by just proving that the sole solution to the quartic 2 · (︀ 2 + 2 2)︀ 2 − (︀ 2 + 2 2)︀ 2 = 1 in N is ⟨¯, ¯, ¯, ¯⟩ = ⟨1, 0, 1, 0⟩ ; but a couple of days after [20] was published on arXiv, Evan O’Dorney (University of Notre Dame) and Bogdan Grechuk (University of Leicester) sent us kind communications that they had found two, respectively three, non-trivial solutions to this equation. Their first solution is the components of the third solution are numbers of roughly 180 decimal digits each.
It must be mentioned that Apoloniusz Tyszka radically disbelieves Matiyasevich’s finite-fold representability conjecture10 which has been, throughout, (and firmly remains) our polar star.
One of the questions Yu. Matiyasevich raised, at the outset of his seminal paper [
Suppose a proof is available that each (1, . . . , ) = in some indexed family of equations has at most one solution in N . Can we extract from it an efective bound C ensuring, when 1 = 1 , . . . , = is such solution, that 1, . . . , ⩽ C ?
As we have recalled and explained among the conclusions of [
Matiyasevich also discussed in [22] (see [7, pp. 151–152] for a quick account) intriguing consequences that establishing the finite-fold Diophantine representability of any r.e. set would entail about the Diophantine characterization of the probability of selecting by chance a program that terminates on every input.
This paper is a companion of [
The authors gratefully acknowledge partial support from project “STORAGE–Università degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, from INdAM–GNCS 2019 and 2020 research funds, and from ICSC–Centro Nazionale di Ricerca in High-Performance Computing, Big Data and Quantum Computing.
The authors are indebted with Pietro Corvaja (University of Udine) and Pietro Campochiaro
(Scuola Superiore di Catania) for helpful discussions, and to the anonymous referees for many
useful suggestions.
[15] Yu. V. Matiyasevich, Existence of nonefectivizable estimates in the theory of exponential
diophantine equations, Journal of Soviet Mathematics 8 (1977) 299–311. (Translated from [
II 30 (1968) 766–773. [20] D. Cantone, L. Cuzziol, E. G. Omodeo, Six equations in search of a finite-fold-ness proof, 2023.
arXiv:2303.02208.
[21] A. Tyszka, A hypothetical way to compute an upper bound for the heights of solutions of a
Diophantine equation with a finite number of solutions, in: M. Ganzha, L. A. Maciaszek, M. Paprzycki
(Eds.), 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015,
Lódz, Poland, September 13-16, 2015, volume 5 of Annals of Computer Science and Information
Systems, IEEE, 2015, pp. 709–716. URL: https://doi.org/10.15439/2015F41. doi:10.15439/2015F41.
[22] Yu. Matiyasevich. Diophantine flavor of Kolmogorov complexity. Transactions of the Institute
for Informatics and Automation problems of NAS RA. Collected reports of participants of JAF-23
(June 2–5, 2004). pages 111–122. Yerevan, 2006.
[23] Ju. V. Matijasevič, Enumerable sets are Diophantine, Soviet Mathematics. Doklady 11 (1970)
354–358. (Translated from [
World Scientific Publishing Co., Inc., River Edge, NJ, 2003. [25] 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 Feferman. xliv+338 pp. [26] E. G. Omodeo, A. Policriti (Eds.), Martin Davis on Computability, Computational Logic, and
Mathematical Foundations, volume 10 of Outstanding Contributions to Logic, Springer, 2016. [27] M. Davis, Computability and Unsolvability, McGraw-Hill, New York, 1958. Reprinted with an additional appendix, Dover 1983.