[FOM] Koenigsmann's universal definition of Z in Q

[Grant Olney Passmore]

Re the quantifier complexity of known `IsAnInteger' predicates for carving
Z out of Q, my understanding is as follows:

 - Robinson's original predicate was A^2 E^7 A^6.
 - Poonen's definition has a quantifier prefix of A^2 E^7.
 - Koenigsmann has now constructed predicates with prefix A^418 and A
E^1109 (the former being his new purely universal definition, and the
latter being a simplification of Poonen's definition he gives as a
corollary in his Annals paper).

These stats on Koenigsmann's definitions aren't in the published version of
his paper; I learned these numbers from him directly.
He's also told me that he believes he can further reduce the number of
existential quantifiers in AE definition.

What amazing achievements!

Grant

On Sun, Jan 24, 2016 at 4:28 AM Mario Carneiro <di.gama at gmail.com> wrote:

> Perhaps this is a silly question, but... The theorem starts with a pair of
> existentials, so in principle we should have an *actual* concrete
> polynomial to look at here. Can the result be stated for any particular
> polynomial? Do we have any bounds on n or the height of g? Or is the method
> inherently nonconstructive?
>
> Mario
>
> On Fri, Jan 22, 2016 at 4:37 PM, Timothy Y. Chow <tchow at alum.mit.edu>
> wrote:
>
>> This is old news but I only learned about it today, and since it doesn't
>> seem to have been mentioned on FOM, I figured that some subscribers may not
>> have heard of it either.
>>
>> Jochen Koenigsman has proved:
>>
>> Theorem.  For some positive integer n, there exists a polynomial
>> g in Z[t; x_1, ..., x_n] such that, for any t in Q,
>>
>>    t is in Z  iff  forall x_1,...,x_n in Q: g(t; x_1, ..., x_n) != 0.
>>
>> In other words, Z is universally definable in Q.  This does not quite
>> resolve Hilbert's tenth problem over Q---for that, one wants to show that Z
>> is *existentially* definable in Q---but it comes close.
>>
>> Koenigsmann posted a preprint to the ArXiv back in 2010.  I found out
>> about it only today because I happened to see the published version:
>>
>> Jochen Koenigsmann, Defining Z in Q, Ann. Math. 183 (2016), 73-93.
>>
>> I quote a few paragraphs from Koenigsmann's paper:
>>
>> ---
>>
>> Like all previous definitions of Z in Q, we use elementary facts on
>> quadratic forms over R and Q_p, together with the Hasse-Minkowski
>> local-global principle for quadratic forms.  What is new in our approach is
>> the use of the Quadratic Reciprocity Law (e.g., in Propositions 10 or 16)
>> and, inspired by the model theory of local fields, the transformation of
>> some existential formulas into universal formulas (Step 4).  A technical
>> key trick is the existential definition of the Jacobson radical of certain
>> rings (Step 3) that makes implicit use of so-called `rigid elements' as
>> they occur, e.g., in [Koe95].
>>
>> Step 1: Diophantine definition of quaternionic semi-local rings a la
>> Poonen.  The first step modifies Poonen's proof ([Poo09a]), thus arriving
>> at a formula for Z in Q that, like the formula in his Theorem 4.1, has two
>> foralls followed by seven thereexists, but we managed to bring down the
>> degree of the polynomial involved from 9244 to 8.
>>
>> Step 2: Towards a uniform diophantine definition of all Z_(p)'s in Q.  We
>> will present a diophantine definition for the local rings Z_(p) = Z_p n Q
>> depending on the congruence of the prime p modulo 8 and involving p (and if
>> p=1 mod 8 an auxiliary prime q) as a parameter.
>>
>> Step 3: An existential definition for the Jacobson radical.  We will show
>> that, for some rings R occurring in Proposition 10, the Jacobson radical
>> J(R) can be defined by an existential formula.  This will also give rise to
>> new diophantine predicates in Q.
>>
>> Step 4: From existential to universal.
>>
>> ---
>>
>> Tim Chow
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160124/8d55bf70/attachment.html>