3 Diophantine problems
In the last section, we saw Tennenbaum's theorem, its relationship with the
incompleteness theorems and some subsequent refinements of it down to the
theory of bounded existential induction, IE1. Some minor
improvements were found by the present author by considering the
parameter-free induction scheme for bounded existential
formulas (MR1040385), but the theory IE1 represents
the approximate limit of results of this kind to date. On the other hand
Shepherdson (MR0161798) found nonstandard recursive models for
quantifier-free induction, and Berarducci and Otero have improved this
slightly to the case of normal open induction (MR1456104). Between
the theories IE1 and normal open induction there remains
substantial work to be done.
These considerations already put us in the realm of studying diophantine
sets, diophantine induction and diophantine definitions, and the issues relating to
Hilbert's 10th problem. Wilmers used the MRDP theorem to prove
his results about IE1. It seems that further progress in the
direction of Tennenbaum-type results will require new proofs or at least
a more detailed analysis of existing proofs of the the MRDP theorem.
Definition 3.1
We say that a theory T of arithmetic proves
the MRDP theorem (T⊢MRDP)
if for every Σ1 formula of the
language of arithmetic ϕ(x¯) there is an
∃1 formula ψ(x¯) in the same free variables
such that
T⊢∀x¯(ϕ(x¯)↔ψ(x¯)).
The definition just given does not make any predetermined choices
of equivalent formulas. (In this sense it is not about any first order axiom
scheme being provable.) The theory IΔ0+exp
does prove MRDP (Gaifman and Dimitracopoulos (MR648303)). On the other hand
IΔ0⊢MRDP is an important open problem
related to questions in complexity theory.
Theorem 3.2 (Kaye)
Suppose T is a theory of arithmetic extending
PA- and T⊢MRDP. Then every nonstandard
model of T is nonrecursive.
Proof
Let
A=n∈ℕ:ℕ⊧∃y α(n,y)
and
B=n∈ℕ:ℕ⊧∃z β(n,y)
be r.e. recursively inseparable sets,
where α,β are Δ0. We consider the formula
θ(w) which is
∀x,y,z<w ¬(α(x,y)∧β(x,z)).The formula θ(w) is Δ0 and true for all w∈ℕ.
If there is some nonstandard c∈M such that M⊧θ(c) then
C=n∈ℕ:M⊧∃y<c α(n,y)would be Δ0 definable, contains A (since c>ℕ)
and disjoint from B. So C would be nonrecursive, but, by
considering both the formula defining C and its negation and MRDP in M,
it is both ∃1- and ∀1-definable in M, hence
is recursive in the operations +,⋅,< of M. We conclude that
at least one of these operations must be nonrecursive.
If on the other hand, the standard cut is defined in M
by θ(w), i.e., ℕ=n∈ℕ:M⊧θ(n),
we take any nonstandard c∈M. Then a Σ1 predicate over naturals
∃xψ(n,x) is true for n∈ℕ iff
M⊧∃x<c (θ(x)∧ψ(n,x)). This is
a Δ0 formula, so by MRDP in M
it is both ∃1 and ∀1 definable in M so
we have shown that every Σ1 predicate is recursive
in the operations +,⋅,< of M, and hence
at least one of these operations must be nonrecursive.
The above result and its proof (which appeared first in
Kaye (MR1236464)) are interesting, not so much in the
result they prove, but in the way that they show that Tennenbaum-type theorems
can be proved by means other than overspill, especially by reducing the
problem in hand to questions about the standard model. These arguments seem to
split into cases: one case mirrors the overspill argument, but if overspill
fails then the standard cut is definable in the model in some way which also
leads to the required conclusion. Other similar examples will be given shortly.
An old question that has been open since the 1950s (originally raised
by Kreisel, I believe) is whether there is an algorithm for deciding
provability in the system of arithmetic formulated in the logic without
quantifiers. Shepherdson reformulated this question in terms of open induction, and it
remains one of the most interesting questions about open induction.
Question 3.3
Is the set ∀1-Th(IOpen) of
universal consequences of open induction recursive?
Another way of stating such a question is to ask if there is an
effective method to decide,
given a diophantine equation p(x¯)=q(x¯) where p,q
are polynomials with nonnegative integer coefficients, whether there is
some model of IOpen containing at least one solution of the equation.
Questions of this type are related
to Tennenbaum phenomena, for if T is a theory extending
PA- and ∀1-Th(T) is recursive
then by forcing with quantifier-free conditions (as in the proof of
Theorem above) we may build a recursive
model of ∀2-Th(T). This model is nonstandard
because the set of ∃1 sentences true in the model
can be read off recursively from the construction, but the
∃1 theory of the standard model ℕ
is not decidable by the MRDP theorem in ℕ. So Tennenbaum's
theorem for ∀2-Th(T) would imply the
undecidability of ∀1-Th(T).
Now, although it is in fact true that
IOpen=∀2-Th(IOpen),
the argument in the last paragraph doesn't seem to
help us, as Tennenbaum's theorem fails
for IOpen, by Shepherdson's work.
In fact, this isn't quite the end of the
story as we shall see in a moment, but let
us for the moment set our sights a little lower
and prove some weaker theorems of the same type.
The following result has not previously been published.
Theorem 3.4
The set
∀∃<-Th(PA-)
of consequences of PA- of the form
∀x¯∃y¯<p(x¯)θ(x¯,y¯)
with θ(x¯,y¯) quantifier-free is not recursive.
Proof
This is a model theoretic forcing argument with
∀< conditions, i.e., conditions of the form
∀y¯<p(x¯)θ(x¯,y¯)
with θ quantifier-free. (Note that up to
logical equivalence such formulas are closed under conjunctions.)
Our assumption that ∀∃<-Th(PA-) is recursive
means that we build a recursive model M of PA-
with a recursive sequence of conditions. For any tuple
w¯∈M of the constructed model, the set of
formulas ∃∀<-tp(w¯) of all
∃∀< formulas true of the tuple
w¯ is recursive since given such a formula
∃x¯∀y¯<p(x¯)θ(w¯,x¯,y¯)
we may decide its truth in M by searching simultaenously
either for a conjunct of a condition of the form
∀y¯<p(x¯)θ(w¯,u¯,y¯)
or for a proof that
PA-⊢∀u¯,v¯,w¯(λ(u¯,w¯)→¬∀y¯<p(v¯)θ(w¯,v¯,y¯))for some condition λ(u¯,w¯).
In particular, the model M is nonstandard as the set of
formulas ∃∀<-tp(0) for the
standard model ℕ is non-recursive.
Now take A,B r.e. and recursively inseparable.
By the MRDP theorem in ℕ we may assume
A=n∈ℕ:∃y¯ α(n,y¯)
and
B=n∈ℕ:∃z¯ β(n,z¯)
where α,β are quantifier-free. Now consider
∀x,y¯,z¯<c ¬(α(x,y¯)∧β(x,z¯)).
If there is no nonstandard c∈M satisfying this, then the
standard cut ℕ is ∀<-definable in M
and any r.e. set X⊆ℕ would be recursive,
since, by MRDP in ℕ, X is
n∈ℕ:∃w¯ ξ(n,w¯)
for some quantifier-free ξ, and hence
X=n∈ℕ:∃w¯ (⋀iθ(wi)∧ξ(n,w¯))where θ(x) is the ∀< formula
defining ℕ in M. The truth of this can be read off
∃∀<-tp(0).
On the other hand, if there is some nonstandard c∈M
such that
∀x,y¯,z¯<c ¬(α(x,y¯)∧β(x,z¯)).we consider C=n∈ℕ:∃y¯<c α(n,y¯)
which contains A and is disjoint from B by choice of C,
and is also recursive since the truth of
∃y¯<c α(n,y¯) can be read off
∃∀<-tp(c) for any particular n.
Theorem 3.5
The set ∀1-Th(IE1)
of ∀1 consequences of IE1 is not recursive.
As will be clear from the proof of Theorem ,
there is still scope for stronger results here. I have given
complex conditions by which induction axioms in a theory T
may be omitted but nevertheless ∀1-Th(T)
be proved nonrecursive by the methods discussed here (MR1218655).
Now I shall describe simpler conditions on the theory T for the same result
to hold; one still strong enough to prove Theorem .
To motivate the ideas, connsider first a
model M⊧IΔ0. The
theory IΔ0 is strong enough to define exponentiation
in a reasonably clean way but cannot prove the statement of the totality
of exponentiation, exp: ∀x∃y y=2x.
As already mentioned, IΔ0+exp proves the MRDP theorem.
The key application of MRDP in the arguments here is to the
formula
∀x,y,z<w ¬(α(x,y)∧β(x,z))where α,β are quantifier-free.
Let 20x=x and
2k+1x=22kx.
By the provability of MRDP in IΔ0+exp there is
some k∈ℕ (depending possibly on α,β) and
quantifier-free θ(u¯) such that IΔ0 proves
∀w(∃v(v=2kw)→((∀x,y,z<w ¬(α(x,y)∧β(x,z)))↔∃u¯ θ(u¯,w))).This is by a result for IΔ0+exp
similar to the well-known theorem of Parikh (MR0304152)
for IΔ0. Parikh's theorem says that
if IΔ0⊢∀x¯ ∃y¯ θ(x¯,y¯)
where θ(x¯,y¯) is Δ0
then the y¯ may be bounded by a polynomial in x¯,
IΔ0⊢∀x¯ ∃y¯<t(x¯) θ(x¯,y¯).
The same holds for IΔ0+exp except the term t(x¯)
must be a term involving exponentiation, and in fact
the axiom exp can be omitted in the conclusion. (This is
proved by a model-theoretic argument similar to the one for Parikh's
Theorem given for example in Models of Peano Arithmetic,
Exercise 6.5 (MR1236464).) The particular sentence of
interest in our case is
∀w(∀x,y,z<w ¬(α(x,y)∧β(x,z))→∃u¯ θ(u¯,w))which is provable in IΔ0+exp, showing the u¯
can be bounded by an exponential term in w.
The idea then is to consider the subset L of M
consisting of all w for which
M⊧∃v(v=2kw). In the case of
a nonstandard model of IΔ0, this L
will be a nonstandard initial segment, but the important feature
is that, by replacing ∃v(v=2kw)
by an appropriate Pell equation, we may take L to be
definable by an existential formula.
Definition 3.6
Let T be a theory in the usual language for
arithmetic. We say that T virtually proves MRDP
if whenever ϕ(w) is ∀< then there are
ψ(v¯,w) and θ(u¯,w), both quantifier-free,
such that
T⊢∃v¯ ψ(v¯,n)
for each n∈ℕ and
T⊢∀w(∃v¯ ψ(v¯,w)→(ϕ(w)↔∃u¯ θ(u¯,w))).
Theorem 3.7
(a) if T is consistent and virtually proves MRDP
then ∀1-Th(T) is nonrecursive. (b)
IE1 virtually proves MRDP.
Proof
(a) Let A,B be r.e. and recursively inseparable and defined
by
A=n∈ℕ:∃y¯ α(n,y¯)
and
B=n∈ℕ:∃z¯ β(n,z¯)
as before, and let ϕ(w) be ∀x,y¯,z¯<w ¬(α(x,y¯)∧β(x,z¯)). Take ψ(v¯,w) and θ(u¯,w) as in the definition
and build a recursive model M of ∀2-Th(T) in which
all ∃1-tp(c¯) are resursive, as before. Now choose
a nonstandard c∈M such that
M⊧∃u¯,v¯ (ψ(v¯,c)∧θ(u¯,c)).Observe that each c∈ℕ satisfies the above formula,
by properties of ψ and θ in the definition, so if there were no
nonstandard c∈M as above we would conclude that ℕ is
∃1-definable in M and so ∃1-Th(ℕ)
can be read off ∃1-tp(0), which is impossible.
Thus M⊧∀x,y¯,z¯<c ¬(α(x,y¯)∧β(x,z¯))
and the set
C=n∈ℕ:∃y¯<c α(x,y¯)is recursive and separates A,B.
(b) A Pell equation can be used in place of y=2x to prove
an analogous result to
∀w(∃v(v=2kw)→((∀x,y,z<w ¬(α(x,y)∧β(x,z)))↔(∃u¯ θ(u¯,w)))).for IE1 in place of IΔ0. See Kaye (MR1040385)
for details.