[FOM] review of two books on logic and foundations

[Jeremy Avigad]

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

   http://www.andrew.cmu.edu/user/avigad

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,

Jeremy Avigad
Associate Professor, Philosophy
Carnegie Mellon