A short introduction to intuitionistic logic (Q2703802)

This book gives an introdution to intuitionistic logic by emphasizing its connections with computer science. The subject is presented by proof-theoretic machinery: beginning with natural deduction, then continuing with sequent calculi and tableaux systems, which lead to automatic proof-search procedures. This basic line of argument is supported by the topics on programming interpretation by lambda-calculus (Curry-Howard isomorphism), relational, algebraic, and topological semantics (soundness and completeness), as well as some related technical issues (filtration, etc.). Though the book is comparatively short, the material as a whole covers quite a large part of the fundamental results on the subject due to the author's new compact proofs for them, including normalization of natural deductions, cut-elimination in sequent calculi, interpolation (and Beth definability) theorem, disjunction (and existential) property, negative translation of classical into intuitionistic logic (Glivenko's Theorem), and, in the propositional case, finite model property, decidability, coherence theorem (for applications to category theory), and so on. The book thus aims at providing a safe background for reading more advanced research literature in logic and computer science. The reader is assumed to be familiar with basic notions of first-order logic, general topology, and (Heyting) algebra.NEWLINENEWLINEIt is a pity that there are considerably many errors in the numbering of results and definitions, in particular when they are referred to afterwards. (Perhaps the proof-reading was insufficient.) This can bring about some confusion in following the arguments or proofs for a reader who studies the topics for the first time. It is also somewhat strange that there is a section (\S 11.1) which consists of its title only. For example, Theorem 5.2, which means the second theorem of Chapter 5, appears in \S 5.3, but in \S 13.3 it is incorrectly referred to as Theorem 5.3 (because it appears in \S 5.3?), while the actual Theorem 5.3, i.e., the third theorem of Chapter 5 appears in \S 5.4.