[FOM] paper announcements
avigad at cmu.edu
Tue May 5 16:14:24 EDT 2009
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,
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
"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
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
"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.
"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.
More information about the FOM