The complexity of the disjunction and existential properties in intuitionistic logic (Q1304542)

As immediate consequences of Gentzen's Hauptsatz, one has disjunction and existential properties of intuitionistic logic. (They are: if \(\lvdash A\vee B\) then \(\lvdash A\) or \(\lvdash B\), and if \(\lvdash\exists x C(x)\) then \(\lvdash C(t)\) for some term \(t\), respectively.) However, to find which disjunct or which term is beyond recursive means. [The authors remind us to think of the halting problem.] In this paper, the authors take up a somewhat different aspect: namely, given a proof of \(A\vee B\), or \(\exists x C(x)\), how efficiently\dots? The answer depends on the logic used. In propositional logic, polynomial time is enough to construct a proof of a disjunct. In predicate logic without function symbols, both properties can be shown in exponential times. But, with function symbols, super-exponential bounds are necessary. Optimality is shown by considering a fragment of arithmetic with a binary predicate for \(y= 2^x\) for the existential property, and for the disjunction property a Turing machine whose future states are hard to predict. This last construction is ingeneous, the reviewer thinks.