Publications
This list includes resarch articles, surveys, expository articles,
unpublished notes, and a translation. I have also done work in formally verified mathematics using the Isabelle proof assistant.
- A language for mathematical knowledge management
with Steven Kieffer and Harvey Friedman, Carnegie Mellon Technical Report CMU-PHIL-181, 2008
Paper: arXiv. Associated materials: html.
- The metamathematics of ergodic theory
to appear in the Annals of Pure and Applied Logic
Paper: pdf.
- Functional interpretation and inductive definitions
with Henry Towsner, submitted.
Paper: arXiv
- Local stability of ergodic averages
with Philipp Gerhardy and Henry Towsner, to appear in Transactions of the American Mathematical Society.
Paper: arXiv
- Response to questionnaire
in Vincent F. Hendricks and Hannes Leitgeb, editors, Philosophy of Mathematics: 5 questions, Automatic / VIP Press, 2007
Book site: html, Paper: pdf (letter), pdf (a4)
- A decision procedure for linear "big O" equations
with Kevin Donnelly, Journal of Automated Reasoning 38: 353-373, 2007
Abstract: html, Paper: journal, arXiv, Implementation: sml
- A variant of the double-negation translation
Carnegie Mellon Technical Report CMU-PHIL 179
Abstract: html, Paper: pdf
(letter), pdf (a4)
- Gödel and the metamathematical
tradition
to appear in a collection essays published in the ASL Lecture Notes in Logic series
Paper: pdf (letter), pdf
(a4).
- Understanding proofs
to appear in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press
Paper: pdf (letter), pdf
(a4).
- Computers in mathematical inquiry
to appear in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press
Paper: pdf (letter), pdf
(a4).
- Combining decision procedures for the reals
with Harvey Friedman, Logical Methods in Computer Science, 2(4:4):1-42, 2006
Paper: journal, 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: journal, arXiv
- Quantifier elimination for the reals with a predicate for the powers of two
with Yimu Yin, Theoretical Computer Science, 370:48-59, 2007
Paper: journal, 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
Paper: pdf (letter), pdf
(a4)
- Notes on a formalization of the prime number theorem
Carnegie Mellon Technical Report CMU-PHIL-163, 2004
Paper: pdf (letter), pdf
(a4)
- Philosophy of mathematics
in Constantin Boundas, editor, The Edinburgh Companion to Twentieth-Century
Philosophies, Edinburgh University Press, 2007, also published as The Columbia Companion to Twentieth-Century Philosophies, Columbia University Press, 2007
Paper: pdf (letter), pdf
(a4).
- Dedekind's
1871 version of ideal theory
translation, with an introduction; Carnegie
Mellon Technical Report CMU-PHIL-162, 2004
Paper: pdf (letter), pdf
(a4). The original version: pdf.
- Mathematical
method and proof
Synthese 153:105-159, 2006
Abstract: html, Paper: journal, pdf
(letter), pdf (a4)
- 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
Abstract: html, Paper: pdf
(letter), pdf (a4)
- Fundamental
notions of analysis in subsystems of second-order arithmetic
with Ksenija Simic, Annals of Pure and Applied Logic, 139:138-184,
2006
Abstract: html, Paper: pdf
(letter), pdf (a4), published
version
- Forcing in
proof theory
Bulletin of Symbolic Logic, 10:305-333, 2004
Abtract: html, Paper: pdf
(letter), pdf (a4). Published
version: html.
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.)
Abstract: html, Paper: portal
link, pdf
- Weak
theories of nonstandard arithmetic and analysis
in Stephen Simpson, editor, Reverse Mathematics 2001, A K Peters,
19-46, 2005
Abstract: html, Paper: dvi,
postscript, pdf
- Notes on Pi^1_1
conservativity, omega-submodels, and the collection schema
Carnegie Mellon Technical Report CMU-PHIL-125, 2001
Abtract: html, Paper: dvi,
postscript, pdf
- Number theory
and elementary arithmetic
Philosophia Mathematica, 11:257-284, 2003
Abtract: html, Paper: pdf.
- Saturated
models of universal theories
Annals of Pure and Applied Logic, 118:219-234, 2002
Abstract: html, Complaint: html,
Paper: dvi, postscript,
pdf
- Algebraic proofs
of cut elimination
Journal of Logic and Algebraic Programming, 49:15-30, 2001
Abstract: html, Paper: dvi, postscript,
pdf
- Update
procedures and the 1-consistency of arithmetic
Mathematical Logic Quarterly, 48:3-13, 2002
Abstract: html, Paper: dvi,
postscript, 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
Abtract: html, Paper: dvi, postscript,
pdf.
- An
ordinal analysis of admissible set theory using recursion on ordinal notations
Journal of Mathematical Logic, 2:91-112, 2002
Abstract: html, Paper: dvi,
postscript, pdf
- Transfer
principles in nonstandard intuitionistic arithmetic
with Jeffrey Helzner, Archive for Mathematical Logic, 41:581-602,
2002
Abstract: html, Paper: dvi,
postscript, 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
Abstract: html, Paper: dvi, postscript,
pdf
- Interpreting
classical theories in constructive ones
Journal of Symbolic Logic, 65:1785-1812, 2000
Abstract: html, Paper: dvi,
postscript, 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
Abstract: html, Paper: dvi, postscript,
pdf
- The
model-theoretic ordinal analysis of predicative theories
with Richard Sommer, Journal of Symbolic Logic, 64:327-349, 1999
Abstract: html, Paper: dvi,
postscript, pdf
- Gödel's
functional ("Dialectica") interpretation
with Solomon Feferman, in S. Buss ed., The Handbook of Proof Theory,
North-Holland, 337-405, 1999
Abtract: html, Paper: dvi,
postscript, pdf.
- Plausibly hard
combinatorial tautologies
in Beame and Buss eds., Proof Complexity and Feasible Arithmetics,
American Mathematical Society, 1-12, 1997
Abstract: html, Paper: dvi, postscript,
pdf
- A model-theoretic
approach to ordinal analysis
with Richard Sommer, Bulletin of Symbolic Logic, 3:17-52, 1997
Abstract: html, Paper: dvi,
postscript, pdf
- An
effective proof that open sets are Ramsey
Archive for Mathematical Logic, 37:235-240, 1998
Abstract: html, Paper: dvi, postscript,
pdf
- Predicative
functionals and an interpretation of ID^_<omega
Annals of Pure and Applied Logic, 92:1-34, 1998
Abstract: html, Paper: dvi, postscript,
pdf
- Formalizing
forcing arguments in subsystems of second-order arithmetic
Annals of Pure and Applied Logic, 82:165-191, 1996
Abstract: html, Paper: dvi,
postscript, pdf
- On the relationship
between ID^_<omega and ATR_0
Journal of Symbolic Logic, 61:768-779, 1996
Abstract: html, Paper: dvi,
postscript, pdf