[FOM] paper announcements

[Jeremy Avigad]

Dear friends and colleagues,

I would like to announce a few recent papers that may be of interest to 
some in the FOM community. Preprints can be found on my web page,

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

with links to the published versions of those that have already appeared.

To start with, Edward Dean, John Mumma, and I have just posted a revised 
version of our paper,

   "A formal system for Euclid's *Elements*,"
   to appear in the *Review of Symbolic Logic*

Proofs in the *Elements* are sometimes held to fall short of modern 
mathematical rigor because they require an "intuitive" appeal to the 
diagrams. We argue that, in fact, diagram use in the *Elements* is 
governed by a discernible logic, and we have tried to spell out the 
details. Our analysis characterizes Euclidean diagrammatic reasoning in 
logical terms, screening off cognitive and broader philosophical 
questions. I discuss some related issues in

   "Review of Marcus Giaquinto, *Visual thinking in mathematics:
   an epistemological study*"
   *Philosophia Mathematica*, 17:95-108, 2009

This appears on my web page under "Reviews."

On another topic, I have been interested in understanding 
nonconstructive aspects of ergodic theory and ergodic Ramsey theory in 
more constructive or explicit terms. Here the relevant papers are as 
follows:

   "Local stability of ergodic averages"
   with Philipp Gerhardy and Henry Towsner
   to appear in the *Transactions of the American Mathematical Society*

   "The metamathematics of ergodic theory"
   *Annals of Pure and Applied Logic*, 157:64-76, 2009

   "Functional interpretation and inductive definitions"
   with Henry Towsner
   to appear in the *Journal of Symbolic Logic*.

   "Metastability in the Furstenberg-Zimmer tower"
   with Henry Towsner
   submitted.

The first provides quantitative (and constructive) versions of the mean 
and pointwise ergodic theorems. The second is a survey. The third is a 
variant of the Dialectica interpretation that Towsner and I designed for 
the purpose of studying applications of the Furstenberg-Zimmer structure 
theorem to combinatorics. The fourth shows that a certain weakening of 
the structure theorem, still sufficient for the combinatorial 
application, requires only a small initial segment of the transfinite 
construction.

Another paper,

   "A language for mathematical knowledge management"
   with Steven Kieffer (first author) and Harvey Friedman,
   to appear in *Studies in Logic, Grammar and Rhetoric*

describes a syntactically-sugared version of set theory with definitions 
and partial functions, which provides a convenient way of expressing 
ordinary mathematical definitions. Kieffer's Carnegie Mellon MS thesis 
presents interesting statistics on the sizes and depths of definitions 
from elementary set theory and topology. Examples we have posted on my 
web page show that the formal language can be used to provide natural 
language output that is remarkably readable.

Finally,

   "The computational content of classical arithmetic"

is a survey which, in particular, discusses some variants of the 
Gödel-Gentzen double-negation translation, and their properties. The 
paper was written in honor of Grigori Mints' upcoming 70th birthday.

Best wishes,

Jeremy