Proof theory is the result of a short and tumultuous history, developed on the periphery of mainstream mathematics. Hence, its language is often idiosyncratic: sequent calculus, cut-elimination, subformula property, etc. This survey is designed to guide the novice reader and the itinerant mathematician along a smooth and consistent path, investigating the symbolic mechanisms of cut-elimination, and their algebraic transcription as coherence diagrams in categories with structure. This spiritual journey at the meeting point of linguistic and algebra is demanding at times, but also pleasantly rewarding: to date, no language (either formal or informal) has been studied by mathematicians as thoroughly as the language of proofs. We start the survey by a short introduction to proof theory (Chapter 1) followed by an informal explanation of the principles of denotational semantics (Chapter 2) which we understand as a representation theory for proofs – generating algebraic invariants modulo cut-elimination. After describing in full detail the cut-elimination procedure of linear logic (Chapter 3), we explain how to transcribe it into the language of categories with structure. We review three alternative formulations of ∗-autonomous category, or monoidal category with classical duality (Chapter 4). Then, after giving a 2-categorical account of lax and oplax monoidal adjunctions (Chapter 5) and recalling the notions of monoids and monads (Chapter 6) we relate four different categorical axiomatizations of propositional linear logic appearing in the literature (Chapter 7). We conclude the survey by describing two concrete models of linear logic, based on coherence spaces and sequential games (Chapter 8) and by discussing a series of future research directions (Chapter 9).
Search
Reviews
[Write a review of this article]
Find related articles from these CiteULike users
