Studying mathematics via logic implies one needs to choose a suitable logical language and represent part of mathematics therein. This post deals with the question whether such representations remain true to the original, or somehow distort it. I show that even the well-known representation of continuous functions leads to significant distortion.
Essential incompleteness in propositional logic
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…
