This post explains how methods from ordinal analysis can be used to prove results in reverse mathematics. It may be surprising that this is possible, given that the traditional aims of the two areas are somewhat different: reverse mathematics proves implications between different statements about infinite sets, while ordinal analysis eliminates the infinite from proofs…
Lifting proofs: from Specker sequences to nets
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.