Linear inferences are propositional tautologies of the form , where and are formulas with at most one occurrence of each propositional variable. These form a -complete set, but surprisingly little is known about their structure, despite their importance in structural proof theory (and beyond). In this post I will cover some of the background on…
What proof mining is about, Part II: Structures and metatheorems
As I said last time, it is time to raise the stakes and start dealing with sentences involving structures, which at first will be the structures of first-order logic. Let, then, be a first-order signature and be a family of -sentences. For the purposes of this post, we shall say, for any -structure , that…
Checking proofs with very low complexity
The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth . But exactly how much effort is required to check a proof, in terms of computational complexity?…
What proof mining is about, Part I
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…