This post provides an answer to the question: Can we somehow ‘lift’ proofs in a restricted language to interesting proofs in a richer language?
Contraction on a leash
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…
