Journal article:

Samuel R. Buss, Pavel Pudlák.
"On the Computational Content of Intuitionistic Proofs."
Annals of Pure and Applied Logic 109 (2001) 49-64.

Download: postscript or PDF.

Introduction: The intuitionistic calculus was introduced to capture reasoning in constructive mathematics. As such it has much more constructive character than classical logic. This property of the intuitionistic calculus has been extensively studied, but mostly from the point of view of computability and little has been proved about computational complexity. The aim of this paper is to show that the constructive character of intuitionistic logic manifests itself not only on the level of computability but, in case of the propositional fragment, also on the level of   polynomial time computability.
Recent progress in proof complexity of propositional logic, which concerns various proof systems, suggest that the study of the complexity of intuitionistic propositional proofs may be a fruitful area. In particular for several classical calculi a so-called feasible interpolation theorem was proved \cite{Krajicek:interpol,Pudlak:interpol,PudlakSgall}.  Such theorems enable one to extract a boolean circuit from a proof; the size of the circuit is polynomial in the size of the proof. Indeed, feasible interpolation theorem was proved for the intuitionistic sequent calculus in \cite{Pudlak:ComplexityPropositional}.  The proof was based on the result of Buss and Mints \cite{BussMints:disjunctionexistence} which shows that the well-known disjunction property can be witnessed by polynomial algorithms in case of the propositional fragment of the intuitionistic calculus.
In this paper we further generalize the two results on the intuitionistic propositional calculus. The ultimate aim is to obtain a realizability theorem for intuitionistic propositional proofs based on polynomial time computations. We prove a result in this direction (Theorem 3), but we suspect that it is not the best possible result of this type. On the other hand, we show that boolean circuits cannot be replaced by a more restricted type of computation (section 5).
Our proof technique is extracted from \cite{BussMints:disjunctionexistence}. In this paper we make it more explicit (Theorem 1) and use the sequent calculus instead of the natural deduction system used in \cite{BussMints:disjunctionexistence}.   Goerdt~\cite{Goerdt:intuitionisticcomplexity} has also proved some related extensions of the  results in \cite{BussMints:disjunctionexistence}, but his main result is weaker than our Theorem 1.
In section 6 we prove some corresponding results for first order intuitionistic logic.

Back to Sam Buss's publications page.