This relatively short book provides an introduction to the treatment of intuitionistic natural deduction using simply typed \(\lambda\)-calculus and outlines some more advanced topics. The definitions and proofs are given in detail at the beginning, but quickly become much more sketchy while notation is getting heavier. Many of the more original results are taken from the earlier work by the authors. Main attention is paid to propositional logic, predicate extensions are mostly only mentioned. Part 1 gives a general outline. Part 2 provides formulation of intuitionistic natural deduction enriched by \(\lambda\)-terms and the classical multiple succedent natural system with \(\lambda\mu\)-calculus. To incorporate sequent systems (especially antecedent rules), explicit substitutions are introduced. A strong normalization proof is sketched. Part 3 describes various models for these systems. Heyting algebras, bi-Cartesian closed categories and Kripke semantics are familiar. Games for intuitionistic logic are described and used later. Proofs of soundness and completeness are outlined. A related semantics for \(\lambda\mu\)-calculus as well as categorical continuations models (Hoffmann & Streicher) are presented.
Part 4 is devoted to proof search in intuitionistic propositional logic. A lot of attention is paid to the notion of a uniform proof, when a succedent formula is to be analyzed first. Due to absence of the disjunction property in the general case, this proof strategy is complete only for hereditary Harrop formulas. The authors state a modification which is complete for all formulas and for the multiple succedent intuitionistic Gentzen-style calculus, but it is much more complicated. One of the goals of Part 4 is to recover completeness of a resolution formulation of intuitionistic logic due to the reviewer from the completeness of classical resolution. One of the main tools is the notion of an intuitionistic \(\lambda\mu\nu\)-term. Essentially, a \(\lambda\mu\nu\)-term \(t\) is called intuitionistic if the classical Gentzen-style derivation corresponding to \(t\) is transformed into an intuitionistic derivation by the standard operation of pruning redundant formulas and inferences: all formulas in \(\Gamma\), \(\Delta\) are redundant in the axiom \(\varphi, \Gamma\vdash\varphi, \Delta\) and the whole right branch \(\Gamma\to\psi, \Delta\) is redundant in an &-inference \(\Gamma\mapsto\varphi, \Delta;\Gamma\mapsto \psi, \Delta/\Gamma\vdash\varphi\&\psi, \Delta\), if \(\psi\) is redundant in the right premise. By a classical resolution derivation the authors do not mean a familiar thing, but a Gentzen-style sequent derivation satisfying a complicated set of conditions. They prove that for any intuitionistically derivable HH formulas there exists such a derivation which is intuitionistic in their sense and gives rise (via a transformation defined by the reviewer) to an intuitionistic resolution proof in the sense of the reviewer. For arbitrary formulas the definition and proofs are more complicated. Parts 5, 6 are intended to provide an approach to the semantics of the bottom-up proof search for intuitionistic logic. An LJ reduction is defined to be a deduction from arbitrary initial sequents \(\Gamma_1\to\varphi_1,\dots\), \(\Gamma_n\to\varphi_n\) by rules of LJ (one-succedent intuitionistic Gentzen-style rules). Categorical interpretation of such a deduction \(d\) in a bi-Cartesian category \(\mathcal C\) is defined in the same way as for derivations. Initial sequents are assigned new variables \(\xi_1:\Gamma_1\to\varphi_1,\dots,\xi_k:\Gamma_n\to \varphi_n\) so that the whole reduction is interpreted in the polynomial category \({\mathcal C}(\xi_1,\dots,\xi_n)\). Combining this with other kinds of semantics (Kripke models derived from categories, games) results in new kinds of interpretations. It would be interesting to see whether they can throw some new light on the problems of proof search.