Consider the following formulation of Gödel’s first incompleteness theorem. Theorem. Any complete, consistent theory that extends PA is not recursive. In other words, PA is essentially incomplete. Five years ago, I wondered whether such a recursively enumerable and essentially incomplete theory could be easily found in classical propositional logic, where formulas are built up from…
Continuity in System T
Continuity is one of the most important concepts in higher-order computability. Informally, a functional is continuous if we only require a finite part of its input to compute a finite part of its output. Though there are a number of ways of making this precise, at type level 2, that is, for functionals , continuity…
‘Simple’ proofs of cut-elimination: classical logic
In the last couple years, I have taught cut-elimination several times to research-level students (ESSLLI ’18, LSS ’18, and to PhD students at the University of Birmingham). Every time I am left squirming when I have to deal with the monster in the closet: . Most cut-elimination proofs do something like this: Main induction on…
Welcome to The Proof Theory Blog!
Welcome to The Proof Theory Blog! The purpose of this website is to give proof theorists a venue to communicate ideas, works-in-progress, gems, or simply observations that may be relevant to the proof theory community. The hope is that it can eventually evolve into a vibrant forum for proof theoretic discussions and collaboration. Proof theory…
