This is the first post in a series designed to introduce a working logician to the field of proof mining (for when you’ll want to know more than this hopefully gentle introduction will provide, the standard reference is the monograph of Kohlenbach). It will mainly focus on its motivations and logico-mathematical content, with historical information…
From cut elimination to reverse mathematics
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…
