331 logic/hofstadter.p
Description
This article is from the Puzzles FAQ, by Chris Cole chris@questrel.questrel.com and Matthew Daly mwdaly@pobox.com with numerous contributions by others.
331 logic/hofstadter.p
In first-order logic, find a predicate P(x) which means "x is a power of 10."
logic/hofstadter.s
Well, one summer, I decided to tackle the problem. Not having any great
knowledge of number theory, I used a more brute force approach. Note
that for greater comprehensibility, I have broken the resulting formula
up into several stages, but it would not be difficult to put it
back together into one vast formula:
{e is prime:}
PRIME(e) :=
~Eb:Ec:((b+2)*(c+2) = e)
{if e is a prime, true iff a is a power of e:}
PPOWER(a,e) :=
Ab:Ac:((b*c = a) -> ((b = 1) or (Ed: (e*d) = b)))
{if e is a prime, and a is a power of e, true iff d is the
(log_e a)th digit (counting from the right, starting with 0)
in the base-e expansion of n:}
DIG(a,e,d,n) :=
(d < e) & Eb:Ec:((c < a) & (n = (b*e*a) + (d*a) + c))
{if e is prime, and a is a power of e, true iff n has exactly
(log_e a) digits in its base-e expansion (0 is counted as having 0
digits:}
LENGTH(e,a,n):=
(n < a) & Ab:((PPOWER(b,e) & (b < a)) -> (b <= n))
POWER_OF_TEN(x):=
Ee:(PRIME(e) & (e > x) &
En:Ea:(LENGTH(e,a,n) &
DIG(1,e,1,n) &
Ai:Aj:Au:( (PPOWER(u,e) & ((e*u) < a)
& DIG(u,e,i,n) & DIG(e*u,e,j,n))
-> j = (10 * i) ) &
Eu:(PPOWER(u,e) & (e*u = a) & DIG(u,e,x,n))
) )
The basic idea is that you are asserting that for some prime e greater
than x, we can find a number n which, when expressed in base-e notation,
will have 1 in its units place, 10 in its e's place, 100 in its (e^2)'s
place, and in general have the "digit" in each place be 10 times
greater than the one to its right, such that the leftmost digit is our x.
To translate into Hofstadter's notation, of course, we must use horse-shoes
instead of ->'s, big carets instead of &'s, letters a through e (followed
by however many ''s) exclusively, and so forth. (We must also replace <'s
and <= with appropriate expansions, and substitute in for our capitalized
formula abbreviations.) This is left as an exercise to the reader.
Kevin Wald
wald2@husc.harvard.edu
Continue to:
My Books
