(Parts I, II, III) After the developments recounted at the end of the previous post, proof mining lay dormant for a number of years; and it was during this period that it got its current name, as per the suggestion of Dana Scott. It was not just a renaming, but a refinement of the concept:…
Andrei Sipoș
What proof mining is about, Part III: The Heroic Age of Unwinding Proofs
(Parts I, II) “The 2456th Century was matter-oriented, as most Centuries were, so he had a right to expect a basic compatibility from the very beginning. It would have none of the utter confusion (for anyone born matter-oriented) of the energy vortices of the 300s, or the field dynamics of the 600s.” (Isaac Asimov, The…
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…
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…