All publications with abstracts and download links
Books
- An Introduction to Proof Theory
- Sets, Logic, Computation
- Incompleteness and Computability
- Boxes and Diamonds
- forall x: Calgary
Papers by Subject
History of logic
- The genealogy of ‘∨’
- Carnap’s early metatheory: Scope and limits
- Heinrich Behmann’s 1921 lecture on the decision problem and the algebra of logic
- The development of mathematical logic from Russell to Tarski
- Kurt Gödel and computability theory
- The practice of finitism: Epsilon calculus and consistency proofs in Hilbert’s Program
- Hilbert’s “Verunglückter Beweis,” the first epsilon theorem, and consistency proofs
- Completeness before Post: Bernays, Hilbert, and the development of propositional logic
- Kurt Gödel, paper on the incompleteness theorems (1931)
Theory of proofs
- An Introduction to Proof Theory: Normalization, Cut-elimination, and Consistency Proofs
- Epsilon theorems in intermediate logics
- Cut elimination and normalization for generalized single and multi-conclusion sequent and natural deduction calculi
- Natural deduction for the Sheffer stroke and Peirce’s arrow (and any other truth-functional connective)
- Semantics and proof theory of the epsilon calculus
- The epsilon calculus and Herbrand complexity
- The epsilon calculus
- Generalizing theorems in real closed fields
- Note on generalizing theorems in algebraically closed fields
- Short proofs of tautologies using the schema of equivalence
- Algorithmic structuring of cut-free proofs
Philosophy of mathematics
- The significance of the Curry-Howard isomorphism
- Hilbert’s program then and now
- Gödel’s first incompleteness theorem and mathematical instrumentalism
- Critical study of Michael Potter’s Reason’s Nearest Kin
- Numbers and functions in Hilbert’s finitism
- Hilbert’s program
- Hilbert’s Finitism. Historical, Philosophical, and Metamathematical Perspectives
Gödel logics
- First-order Gödel logics
- Characterization of the axiomatizable prenex fragments of first-order Gödel logics
- Quantified propositional Gödel logic
- Hypersequents and the proof theory of intuitionistic fuzzy logic
- Compact propositional Gödel logics
- Incompleteness of an infinite-valued first-order Gödel logic and of some temporal logics of programs
Finite-valued Logic
Other Logic
- Cut-free completeness for modular hypersequent calculi for modal logics K, T, and D
- Non-analytic tableaux for Chellas’s conditional logic CK and Lewis’s logic of counterfactuals VC
- Effective Finite-Valued Approximations of General Propositional Logics
- Decidability of quantified propositional intuitionistic logic and S4 on trees of height and arity ≤ ω
- A complete first-order temporal logic of time with gaps
- Tableaux for reasoning about atomic updates