In Anupam’s recent post, he introduced the linear inferences switch and medial. By computational search it had been shown that all linear inferences with 6 or fewer variables are derivable from these two inferences. He also gave an 8 variable linear inference which is not derivable from switch and medial and posed the question of…
‘Simple’ proofs of cut-elimination II: intuitionistic logic
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…
