The contraction rule (c) (discussed also in this blog post) is a familiar obstacle to anyone aiming to use the sequent calculus to establish a property of the underlying logic. Simply stated the issue is that the premise of the rule is more complicated (contains more content) than its conclusion, and hence proof…
Of representations of mathematics
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…
