Algebra of proofs (Q788719)

The author studies the algebraic properties of the proof theory of intuitionistic first-order logic in a categorical setting. The conceptual basis of the book is the realization that the Lindenbaum-Tarski algebras of formulas may be viewed as categories and that the formal proofs of the associated deductive systems determine structured categories as their canonical algebras which are of the same type as the Lindenbaum-Tarski algebras of formulas of the underlying languages. Following the Introduction (Chapter I), there are twelve additional chapters, in which the author studies twelve theories of varied linguistic and deductive strength. The theories are divided into two main types: the monoidal type, in which theories based on the common algebraic properties of conjunction and disjunction are investigated, and the Cartesian type, in which conjunction and disjunction have their proper meanings. In every chapter the author follows the same scheme. He first constructs a category of a certain type as an algebraic model for the class of formal proofs being considered. Then he proves a completeness theorem to the effect that the arrows of the constructed category can be represented by formal proofs in a Gentzen-style sequent calculus with cut elimination. In the propositional cases the algorithmic character of the cut- elimination process is used to provide an effective description of the arrows of the category constructed and to develop decision procedures, in the form of Church-Rosser theorems, for the commutativity of the finite diagrams of these categories. In the last chapter, the author also shows how to accommodate quantifiers in the calculus of adjoints and describes the topos-theoretic setting required in order to develop the proof theory of intuitionistic first-order logic. The contents of the chapters are as follows: Chapter I: Introduction. The author provides the categorical and logical notions to be used in the rest of the book. Chapter II: Monoidal categories. The weakest structure on a category of logical interest is studied. This type of structure serves as a model for the proof-theoretic properties that are common to \(\bigwedge\) and \(\bigvee\), and to \(\top\) and \(\perp\), and that are independent of the symmetry of \(\bigwedge\) and \(\bigvee\). Chapter III: Symmetric monoidal categories. The effect of the symmetry of \(\bigwedge\) and \(\bigvee\) is considered. Chapter IV: Cartesian categories. The author studies the proof-theoretic properties that are particular to \(\bigwedge\) and \(\top\). Chapter V: Bi-Cartesian categories. The proof-theoretic properties of \(\bigwedge\), \(\bigvee\), \(\top\), \(\perp\) that are independent of distributivity are discussed. Chapter VI: Distributive bi-Cartesian categories. The effect of the distributivity of \(\bigwedge\) over \(\bigvee\) is investigated. Chapter VII: Monoidal closed categories. In this chapter the author begins the study of the categorical models of the proof theory of \(\Rightarrow\). Chapter VIII: Symmetric monoidal closed categories. The proof-theoretic properties that are particular to the symmetric operation \(\wedge \!\vee\) and to \(\Rightarrow\) are discussed. Chapter IX: Cartesian closed categories. The proof-theoretic properties of \(\top\), \(\bigwedge\), \(\Rightarrow\) are considered. Chapter X: Bi-Cartesian closed categories. The author deals with the categorical models for the proof theory of the full intuitionistic propositional calculus. Chapter XI: Residuate categories. The proof-theoretic properties of \(\wedge \!\vee\), \(\Rightarrow\), \(\Leftarrow\) that are independent of the symmetry of \(\wedge \!\vee\) are studied. Chapter XII: Monoidal biclosed categories. The proof-theoretic properties of I, \(\wedge \!\vee\), \(\Rightarrow\), \(\Leftarrow\) that are independent of the symmetry of \(\wedge \!\vee\) are considered. Chapter XIII: Quantifier-complete theories. The author completes his study of intuitionistic proof theories by giving a functorial description of quantifiers. The chosen functorial characterization of quantifiers is inspired by the view of universal and existential quantifiers as generalized conjunctions and disjunctions.