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.