Andrei Sipoș

(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:…

(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…

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…

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…