The significance of the Curry-Howard isomorphism

In Gabriele M. Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics. Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin: De Gruyter. pp. 313-326 (2019)

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

DOI 10.1515/9783110657883-018

Embargoed until November 2020. Please email for offprint.

Book cover

Sets, Logic, Computation. An Open Introduction to Metalogic

Sets, Logic, Computation is an introductory textbook on metalogic. It covers naive set theory, first-order logic, sequent calculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. The audience is undergraduate students with some background in formal logic, e.g., what is covered by forall x.


Book cover

forall x: Calgary. An Introduction to Formal Logic

forall x: Calgary is a full-featured textbook on formal logic. It covers key notions of logic such as consequence and validity of arguments, the syntax of truth-functional propositional logic TFL and truth-table semantics, the syntax of first-order (predicate) logic FOL with identity (first-order interpretations), translating (formalizing) English in TFL and FOL, and Fitch-style natural deduction proof systems for both TFL and FOL. It also deals with some advanced topics such as truth-functional completeness. Exercises with solutions are available. It is provided in PDF (for screen reading, printing, and a special version for dyslexics) and in LaTeX source code.


Rumfitt on truth-grounds, negation, and vagueness

Philosophical Studies 175 (2018) 2079–2089

In The Boundary Stones of Thought (2015), Rumfitt defends classical logic against challenges from intuitionistic mathematics and vagueness, using a semantics of pre-topologies on possibilities, and a topological semantics on predicates, respectively. These semantics are suggestive but the characterizations of negation face difficulties that may undermine their usefulness in Rumfitt’s project.

DOI: 10.1007/s11098-018-1114-7


Semantics and Proof Theory of the Epsilon Calculus

In Logic and Its Applications. ICLA 2017, edited by Sujata Ghosh and Sanjiva Prasad, 27–47. LNCS 10119. Berlin, Heidelberg: Springer.

The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the 𝜀-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic interpretations. The problems facing the development of proof-theoretically well-behaved systems are outlined.

DOI 10.1007/978-3-662-54069-5_4

Natural Deduction for the Sheffer Stroke and Peirce’s Arrow (And Any Other Truth-Functional Connective)

Richard Zach, “Natural Deduction for the Sheffer Stroke and Peirce’s Arrow (and any Other Truth-Functional Connective),” Journal of Philosophical Logic 45(2) (2016), pp. 183–197.

Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke (NAND) and Peirce’s arrow (NOR). The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of the connectives in question.

DOI: 10.1007/s10992-015-9370-x

Preprint on arXiv (with errata)