A logical calculus for polynomial-time realizability
John Newsome Crossley, Gerald L. Mathai, R. A. G. Seely · 1994
A logical calculus, not unlike Gentzen's sequent calculus for intuitionist logic, is described which is sound for polynomial-time realizability as defined by Crossley and Remmel. The sequent calculus admits cut elimination, thus giving a decision procedure for the propositional fragment. 0 Introduction In [4], a restricted notion of realizability is introduced, a special case of which is polynomial-time realizability: this is like Kleene's original realizability, save for three features. First, closed atomic formulae are realized by realizers that give a measure of the resources required to establish the formula, unlike Kleene's system which only reflects the fact that the formula is provable. Second, open formulae are treated as the corresponding closed formulae with all free variables universally quantified simultaneously. (There is a difference between the quantifiers 8h¸; ji and 8¸8j.) And third, the realizers code polynomial-time ("p-time") functions, rather than arbitrary recurs...