Review of : Sheaves, Games, and Model Completions

Abstract

Sheaves, Games, and Model Completions by Silvio Ghilardi and Marek Zawadowski Published July 2002, by Kluwer, ISBN 1402006608. One of the most striking and useful results in the proof theory of intuitionistic logic in the 1990’s is undoubtedly Andy Pitts’ Theorem, which gives an interpretation of the second-order intuitionistic propositional calculus into ordinary intuitionistic propositional logic IPC: for every IPC-formula φ and for every propositional variable p there are formulas ∃pφ and ∀pφ, involving only variables occurring in φ except p, such that for any other IPC-formula ψ which does not contain p, one has the following equivalences: IPC  φ → ψ iff IPC  ∃pφ → ψ IPC  ψ → φ iff IPC  ψ → ∀pφ The book under review is an investigation into algebraic and model-theoretic aspects of this fact. The authors have written a number of joint papers, of which this book can be seen as the synthesis; however, there is also material that was not published before. Their starting point is a re-interpretation of Pitts’ Theorem.