power-free characterization of {10^n} [Re: Godel, Escher, Bach]

[Noam Elkies]

In article <78...@netnews.upenn.edu>
wee...@sagi.wistar.upenn.edu (Matthew P Wiener) writes:
:In article <D8wDLB...@mantis.co.uk>, tony@mantis (Tony Lezard) writes:
:>Although I forget the precise syntax of TNT, I remember cracking "x is
:>a power of 2" by expressing it as, roughly, "for all y, y divides x and
:>y is prime implies y is 2" (got it?),

Yes, but simpler still is "for all y[>0], 2*y+1 does not divide x".

:> but this approach can't work for
:>being a power of 10 (the obvious extension on the above (add "or 5" at
:>the end) allows eg. x=400). Did anyone out there manage to solve this one?
:
:(I didn't "solve" it, since I learned the answer long before GEB existed.)
:
:As far as I know, nothing short of coding sequences works for powers of 10.
:[...]

What I came up with when I read GEB was essentially
POWER_OF_10(x) := "for all y such that R(y), Q(y,10) implies Q(y,x)",
where R(D,u) := "there exist relatively prime m,n such that u=m^2-D*n^2",
and R(y) is a mild restriction needed to make sure that if m and n
are coprime then so are the coefficients of (m+n*sqrt(D))^k, for instance
R(y) := "y is congruent to 3 mod 4 and not divisible by 5". This is
more in line with Hofstadter's hint that one needs to use quite a bit
of number theory. It should also work for arbitrary values of 10. :-)

[Actually I don't think I ever worked out a complete proof that,
for appropriate R(y), POWER_OF_10 does characterize the powers of 10;
but I believe it should be a straightforward, albeit tedious,
application of standard ideas and methods.]

:OK, work with this to go one step further: how do you say "x is 10^n"?

I don't see how to do this using my above trick. One can
certainly adapt Matiyasevich's methods, though.

ObPuzzle: give a rigorous definition of what your statement that
"nothing short of coding sequences works" means. ;-)

--Noam D. Elkies (elk...@zariski.harvard.edu)
Department of Mathematics, Harvard University

[Matthew P Wiener]

In article <1992May26.2...@husc3.harvard.edu>, elkies@ramanujan (Noam Elkies) writes:
>:As far as I know, nothing short of coding sequences works for powers of 10.

>What I came up with when I read GEB was essentially

>POWER_OF_10(x) := "for all y such that R(y), Q(y,10) implies Q(y,x)",
>where R(D,u) := "there exist relatively prime m,n such that u=m^2-D*n^2",

Misprint: R(D,u) should be Q(D,u).

>and R(y) is a mild restriction needed to make sure that if m and n
>are coprime then so are the coefficients of (m+n*sqrt(D))^k, for instance
>R(y) := "y is congruent to 3 mod 4 and not divisible by 5". This is
>more in line with Hofstadter's hint that one needs to use quite a bit
>of number theory. It should also work for arbitrary values of 10. :-)

I expect that Hofstadter himself was thinking of the Goedel beta function,
which relies on the Chinese remainder theorem.

>:OK, work with this to go one step further: how do you say "x is 10^n"?

>I don't see how to do this using my above trick. One can certainly
>adapt Matiyasevich's methods, though.

Considering that Matiyasevich used Pellian methods to encode powers of
the golden ratio, this isn't surprising.

>ObPuzzle: give a rigorous definition of what your statement that
>"nothing short of coding sequences works" means. ;-)

Obviously I was wrong. The rigorous version would be something akin to
the Robinson-Davis-Putnam all-but-proof of M's theorem, where they had
reduced the problem to finding a single Diophantine "roughly exponential"
relation.
--
-Matthew P Wiener (wee...@sagi.wistar.upenn.edu)

[John C. Baez]

In article <1992May26.2...@husc3.harvard.edu> elk...@ramanujan.harvard.edu (Noam Elkies) writes:
>In article <78...@netnews.upenn.edu>
>wee...@sagi.wistar.upenn.edu (Matthew P Wiener) writes:
>:In article <D8wDLB...@mantis.co.uk>, tony@mantis (Tony Lezard) writes:
>:>Although I forget the precise syntax of TNT, I remember cracking "x is
>:>a power of 2" by expressing it as, roughly, "for all y, y divides x and
>:>y is prime implies y is 2" (got it?),
>
>Yes, but simpler still is "for all y[>0], 2*y+1 does not divide x".
>
>:> but this approach can't work for
>:>being a power of 10 (the obvious extension on the above (add "or 5" at
>:>the end) allows eg. x=400). Did anyone out there manage to solve this one?
>:
>:(I didn't "solve" it, since I learned the answer long before GEB existed.)
>:As far as I know, nothing short of coding sequences works for powers of 10.
>:[...]

>[Elkies shows how to do it....]

>ObPuzzle: give a rigorous definition of what your statement that
>"nothing short of coding sequences works" means. ;-)

Yikes!

This has always struck me as by far the stickiest point when it comes to
showing that all functions you think are computable are recursive (e.g.,
definable using expressions with bounded quantifiers). Once you have
codings for arbitrary n-tuples of numbers things get easy, but there is
a bottleneck, which in the treatments I've seen appears at about this
place, where one needs to be a bit sneaky. It's been a while since I've
thought about this. Is there any conventional wisdom among logicians
about this issue or is it regarded as not worth thinking about?

[Noam Elkies]

In article <79...@netnews.upenn.edu>

wee...@sagi.wistar.upenn.edu (Matthew P Wiener) writes:

:In article <1992May26.2...@husc3.harvard.edu>,
:elkies@ramanujan (Noam Elkies) writes:
:>POWER_OF_10(x) := "for all y such that R(y), Q(y,10) implies Q(y,x)",

:>where R(D,u) := "there exist relatively prime m,n such that u=m^2-D*n^2",
:
:Misprint: R(D,u) should be Q(D,u).

Right --- sorry about that.

:[...]
:>ObPuzzle: give a rigorous definition of what your statement that

:>"nothing short of coding sequences works" means. ;-)
:

:Obviously I was wrong. [...]

I didn't mean to needle you about that, but to suggest that it may be
hard if not impossible to even precisely *define* what it means to say
that a TNT formula does or does not rely on coding squences.

--Noam D. Elkies (elk...@zariski.harvard.edu)
Department of Mathematics, Harvard Univ.