# [FOM] review of two books on logic and foundations

Mon Dec 5 17:38:26 EST 2005

```I'd like to announce a review I have written of two books that deal with
logic and foundations in the early twentieth century: Calixto Badesa's
*The Birth of Model Theory* and Dennis Hesseling's *Gnomes in the Fog*.
The review, which will appear in the Mathematical Intelligencer, can be
found on my web page

under "Reviews."

While I am at it, I'd like to mention two other papers, still in
preprint form, that may be of interest to the FOM audience. Both can be
found on my web page, under "Research."

The first, "A formally verified proof of the prime number theorem,"
describes a formalization of the PNT using a mechanized proof assistant,
Isabelle. The formalization was joint work with Kevin Donnelly, David
Gray, and Paul Raff.

The second, "Quantifier elimination for the reals with a predicate for
the powers of two," is a syntactic proof of a result due to van den
Dries, namely, that the theory of the reals as an ordered field with a
predicate for the powers of two is decidable. This result is interesting
in that it subsumes two of the most important decidability results of
the last century: the decidability of real-closed fields, due to Tarski,
and the decidability of the additive theory of the integers, due to
Presburger. It turned out to be rather difficult to extract an explicit
quantifier-elimination procedure from van den Dries's proof; the best we
could do is an algorithm that runs in iterated-iterated-exponential time!

In an MS thesis that he is close to finishing, Yin has also determined a
novel equivalence between two q.e. tests which seem to be strictly
stronger than q.e. For fun, he has also extended the decidability
results to the reals with a predicate for the Fibonacci numbers, and
predicates for other sequences defined by appropriate recurrence
relations. I will add a link to my web page when he has posted it online.

Best wishes,