Journal article:
Samuel R. Buss.
"Bounded Arithmetic, Proof Complexity and Two Papers of
Parikh."
Annals of Pure and Applied Logic 96 (1999) 43-55.
Download article: postscript or PDF.
Abstract: This article surveys R. Parikh's work on feasibility, bounded arithmetic and the complexity of proofs. We discuss in depth two of Parikh's papers on these subjects and some of the subsequent progress in the areas of feasible arithmetic and lengths of proofs.
This article discusses two papers of Rohit Parikh on feasibility and
bounded arithmetic and on the complexity of proofs: the first is the 1971 paper
``Existence and Feasibility in Arithmetic''~\cite{Parikh:feasibility} and the second is
the 1973 paper ``Some Results on Length of Proofs''~\cite{Parikh:length}. Both papers were
seminal and influential and led to large research areas which are still active and
fruitful 25 years later. The first paper addressed the intuitive concept of feasibility,
discussed the infeasibility of exponentiation, and presented the original definition of
bounded arithmetic ($\IDelta_0$). The second paper solved a special case of a conjecture
of Kreisel's and additional problems in proof speed-up, and introduced important tools for
the analysis of the complexity of proofs in first-order logic and other formal systems.
We will discuss first the ``feasibility'' paper, in section 2. Section
3 takes up the ``length of proof'' paper, and section 4 concludes with a discussion of the
connections between these topics.