[FOM] paper announcement

[Jeremy Avigad]

Dear friends and colleagues,

I would like to announce a few papers that may be of interest to the FOM 
audience. The are all available on my web page,

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

under "Publications".

"Understanding proofs". This argues for a particular way of thinking 
about mathematical understanding, and surveys contemporary work in 
formal verification that bears on the topic.

"A decision procedure for linear 'big O' equations" (with Kevin 
Donnelly). We show that the validity of boolean combinations of linear 
"big O" equations (in various formulations) is decidable.

"A variant of the double-negation translation". This short note 
describes an interesting variant of the double-negation translation, and 
an application to functional interpretation. (These results were 
discovered independently by Streicher and Kohlenbach.)

"Combining decision procedures for the reals" (with Harvey Friedman). 
This includes decidability and undecidability results for theories 
obtained by combining the linear and multiplicative fragments of the 
reals (as an ordered field). We also propose a strategy for verifying 
common inferences involving real inequalities in the context of formal 
verification.

"Gödel and the metamathematical tradition". This consists of reflections 
on Gödel and his uneasy relationship with the Hilbert tradition. This 
was presented as a talk to the ASL Spring Meeting in Montreal last year.

"Computers in mathematical inquiry". This is a survey of philosophical 
issues related to the use of computers in mathematics. This article, 
together with "Understanding proofs", will appear in a collection of 
essays on the philosophy of mathematical practice, edited by Paolo Mancosu.

I have announced the last three of these papers in this forum before, 
but they have been revised since then.

Best wishes,

Jeremy Avigad
Associate Professor of Philosophy
Carnegie Mellon University