Cut-elimination for intuitionistic logic has particular significance to proof theorists due to the constructive nature of the logic. Cut-free proofs give rise to significant computational information, including interpolants of implications and, in the case of predicate logic, witnesses of existentials. Moreover, the process of cut-elimination can itself be viewed as a computational process thanks to…
What proof mining is about, Part IV: Kohlenbach & friends
(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:…
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…
The computational content of Nonstandard Analysis
We discuss the computational content of Nonstandard Analysis based on recent proof-theoretic developments.