The logic of information structures (Q1310268)

This book makes a strong point that information processing can be modelled best by intuitionistic logics since the essence of information processing is work in an open system subject to continual revision. It seems to the reviewer that the author makes a good point in this respect and that the theoretical developments presented here should make the intuitionistic approach technically superior to temporal logics. The book is written for researchers familiar with all aspects of intuitionistic logic. The book starts out with a definition of intuitionistic propositional logic (IPL) and some subsystems in a somewhat novel formulation intended to facilitate the systematic variation of structural inference rules. Kripke's and Grzegorczyk's model interpretations are discussed from the point of view of information processing. The basis for the variation of classical logic is the need in information to have a constructive negation, i.e., a provable negation \(\sim\) such that \(\sim A\) for a true formula \(A\) does not imply everything, and for control of the inference rules used. These preliminaries take up most of the first two chapters, the remainder of these chapters is taken up by some examples and by the examination of some ambiguities in previous interpretations of IPL. The technical part starts with chapter 3, where a series of subsystems of IPL and similar logics are introduced, and chapter 4, where the bases are laid for proofs of functional completeness of a given propositional logic to substructures. The technical part gets into high gear with chapter 5 dealing with an application of \textit{W. A. Howard}'s notion of `formulae- as-types construction' [To H. B. Curry: Essays on combinatory logic, lambda calculus and formalism, 479-490; Zbl 0469.03006)] to encoding of proofs, cut-elimination and normalization of terms, followed by the technical discussion (Chapter 6) of systems with constructive negation based on systems introduced by \textit{D. Nelson} [J. Symb. Logic 14, 16-26 (1949; Zbl 0033.243)]. The methods of chapter 4 applied to these systems (Chapter 6) lead to proofs of functional completeness if the notion of proof is augmented by a dual notion of refutation. The remaining two chapters deal with a development of \(\lambda\)-term semantics and with the interpretation of the several systems presented by monoid models based on addition of information and intersection of information pieces. The book ends with the desired proof that constructive negation \(\sim\) cannot be interpreted as inconsistency. All in all, a very successful Ph. D. thesis. \{The book is well produced and contains a valuable index; the reading of logical reduction proofs is sometimes made somewhat difficult by \TeX's unfortunate habit of using smaller and smaller types for complicated formulas\}.