Publications

This list includes research articles, surveys, expository articles, unpublished notes, and a translation. Many of these papers are also listed, arranged by subject matter, under Research. See also listings on MathSciNet, Zentralblatt, DBLP, and Citeseer.

• Metastability in the Furstenberg-Zimmer tower
  with Henry Towsner, draft. Preprint: arXiv.
• The computational content of classical arithmetic
  to appear in a Festschrift for Grigori Mints. Preprint: arXiv.
• A formal system for Euclid's Elements
  with Edward Dean and John Mumma, Review of Symbolic Logic, 2:700-768, 2009. Paper: pdf. Preprint: arXiv. Axioms and test data: smt, tptp. Test diagram: pdf.
• A language for mathematical knowledge management
  with Steven Kieffer (first author) and Harvey Friedman, to appear in a special issue of Studies in Logic, Grammar and Rhetoric on computer reconstruction of the body of mathematics. Paper: arXiv. Associated materials: html.
• The metamathematics of ergodic theory
  Annals of Pure and Applied Logic, 157:64-76, 2009. Paper: doi. Preprint: pdf.
• Functional interpretation and inductive definitions
  with Henry Towsner, Journal of Symbolic Logic, 74:1100-1120, 2009. Paper: doi. Preprint: arXiv.
• Local stability of ergodic averages
  with Philipp Gerhardy and Henry Towsner, Transactions of the American Mathematical Society, 362:261-288, 2010. Paper: doi, pdf. Preprint: arXiv.
• Response to questionnaire
  in Vincent F. Hendricks and Hannes Leitgeb, editors, Philosophy of Mathematics: 5 questions, Automatic / VIP Press, 2007. Book site: html. Preprint: pdf.
• A decision procedure for linear "big O" equations
  with Kevin Donnelly, Journal of Automated Reasoning 38: 353-373, 2007. Paper: doi. Preprint: arXiv. Implementation: sml.
• A variant of the double-negation translation
  Carnegie Mellon Technical Report CMU-PHIL 179. Paper: pdf
• Gödel and the metamathematical tradition
  to appear Charles Parson et al. editors, Kurt Gödel: Essays for his Centennial, ASL Lecture Notes in Logic, Cambridge University Press. Preprint: pdf
• Computers in mathematical inquiry
  in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 302-316, 2008. Reprint: pdf. Preprint: pdf.
• Understanding proofs
  in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 317-353, 2008. Reprint: pdf. Preprint: pdf.
• Combining decision procedures for the reals
  with Harvey Friedman, Logical Methods in Computer Science, 2(4:4):1-42, 2006. Paper: doi, arXiv
  
• A formally verified proof of the prime number theorem
  with Kevin Donnelly, David Gray, and Paul Raff, ACM Transactions on Computational Logic, 9(1:2):1-23, 2007. Paper: doi. Preprint: arXiv. Project page and proof scripts: html.
• Quantifier elimination for the reals with a predicate for the powers of two
  with Yimu Yin, Theoretical Computer Science, 370:48-59, 2007. Paper: doi. Preprint: arXiv
  
• Methodology and metaphysics in the development of Dedekind's theory of ideals
  in José Ferreirós and Jeremy Gray, editors, The Architecture of Modern Mathematics, Oxford University Press, 159-186, 2006. Uncorrected proofs: pdf. Preprint: pdf.
• Notes on a formalization of the prime number theorem
  Carnegie Mellon Technical Report CMU-PHIL-163, 2004. Paper: pdf.
• Philosophy of mathematics
  in Constantin Boundas, editor, The Edinburgh Companion to Twentieth-Century Philosophies, Edinburgh University Press, 234-251, 2007, also published as The Columbia Companion to Twentieth-Century Philosophies, Columbia University Press, 2007. Preprint: pdf.
• Dedekind's 1871 version of ideal theory
  translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004. Paper: pdf. The original: pdf.
• Mathematical method and proof
  Synthese 153:105-159, 2006. Paper: doi. Preprint: pdf.
• Formalizing O notation in Isabelle/HOL
  with Kevin Donnelly, in David Basin and Michaël Rusinowitch, editors, Automated Reasoning: second international joint conference, IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, Springer, 357-371, 2004. Paper: doi. Preprint: pdf.
• Fundamental notions of analysis in subsystems of second-order arithmetic
  with Ksenija Simic, Annals of Pure and Applied Logic, 139:138-184, 2006. Paper: doi. Preprint: pdf.
• Forcing in proof theory
  Bulletin of Symbolic Logic, 10:305-333, 2004. Paper: doi, jstor, bsl. Preprint: pdf. Erratum: html.
• Eliminating definitions and Skolem functions in first-order logic
  ACM Transactions on Computational Logic, 4:402-415, 2003. (Conference version: Logic in Computer Science 2001, Springer, 139-146.)
  Paper: doi. Preprint: pdf.
• Weak theories of nonstandard arithmetic and analysis
  in Stephen Simpson, editor, Reverse Mathematics 2001, A K Peters, 19-46, 2005. Preprint: pdf.
• Notes on Pi^1_1 conservativity, omega-submodels, and the collection schema
  Carnegie Mellon Technical Report CMU-PHIL-125, 2001. Paper: pdf.
• Number theory and elementary arithmetic
  Philosophia Mathematica, 11:257-284, 2003
  Paper: doi. Reprint: pdf.
• Saturated models of universal theories
  Annals of Pure and Applied Logic, 118:219-234, 2002. Paper: doi. Preprint: pdf.
• Algebraic proofs of cut elimination
  Journal of Logic and Algebraic Programming, 49:15-30, 2001. Paper: doi. Preprint: pdf.
• Update procedures and the 1-consistency of arithmetic
  Mathematical Logic Quarterly, 48:3-13, 2002. Paper: doi. Preprint: pdf.
• The epsilon calculus
  with Richard Zach, in the Stanford Encyclopedia of Philosophy. Article: html.
• "Clarifying the nature of the infinite": the development of metamathematics and proof theory
  with Erich H. Reck, Carnegie Mellon Technical Report CMU-PHIL-120, 2001. Paper: pdf.
• An ordinal analysis of admissible set theory using recursion on ordinal notations
  Journal of Mathematical Logic, 2:91-112, 2002. Paper: doi. Preprint: pdf
• Transfer principles in nonstandard intuitionistic arithmetic
  with Jeffrey Helzner, Archive for Mathematical Logic, 41:581-602, 2002. Paper: doi. Preprint: pdf.
• Ordinal analysis without proofs
  in W. Sieg et al. eds., Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, ASL Publications, A K Peters, 1-36, 2002. Preprint: pdf.
• Interpreting classical theories in constructive ones
  Journal of Symbolic Logic, 65:1785-1812, 2000. Paper: jstor, euclid. Preprint: pdf.
• A realizability interpretation for classical arithmetic
  in Buss, Hájek, and Pudlák eds., Logic Colloquium '98, Lecture Notes in Logic 13, AK Peters, 57-90, 2000. Preprint: pdf
• The model-theoretic ordinal analysis of predicative theories
  with Richard Sommer, Journal of Symbolic Logic, 64:327-349, 1999. Paper: jstor, euclid. Preprint: pdf.
• Gödel's functional ("Dialectica") interpretation
  with Solomon Feferman, in S. Buss ed., The Handbook of Proof Theory, North-Holland, 337-405, 1999. Preprint: pdf.
• Plausibly hard combinatorial tautologies
  in Beame and Buss eds., Proof Complexity and Feasible Arithmetics, American Mathematical Society, 1-12, 1997. Preprint: pdf.
• A model-theoretic approach to ordinal analysis
  with Richard Sommer, Bulletin of Symbolic Logic, 3:17-52, 1997. Paper: jstor, euclid, bsl. Preprint: pdf.
• An effective proof that open sets are Ramsey
  Archive for Mathematical Logic, 37:235-240, 1998. Paper: doi. Preprint: pdf.
• Predicative functionals and an interpretation of ID^_<omega
  Annals of Pure and Applied Logic, 92:1-34, 1998. Paper: doi. Preprint: pdf.
• Formalizing forcing arguments in subsystems of second-order arithmetic
  Annals of Pure and Applied Logic, 82:165-191, 1996. Paper: doi. Preprint: pdf.
• On the relationship between ID^_<omega and ATR_0
  Journal of Symbolic Logic, 61:768-779, 1996. Paper: jstor, euclid. Preprint: pdf.