Algebra of Proofs
Published on 14. May 2014
311 pages
978-0-08-095497-4 (ISBN)
Description
Algebra of Proofs
More details
Series
Language
English
Place of publication
Burlington
Netherlands
ISBN-13
978-0-08-095497-4 (9780080954974)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Other editions
Additional editions
Lev D. Beklemishev
Provability, Computability and Reflection: Volume 88
Book
04/2000
Elsevier
€252.97
Article exhausted; check different version
Content
- Front Cover
- Algebra of Proofs
- Copyright Page
- Contents
- Preface
- Chapter 1. Introduction
- 1.1 Categorical preliminaries
- 1.2 Logical preliminaries
- Chapter 2. Monoidal Categories
- 2.1 Definition
- 2.2 Examples
- 2.3 The category Fm(?)
- 2.4 The deductive system m?(?)
- 2.5 The semantics of Der(m?(?))
- 2.6 The syntax of Fm(?)
- Chapter 3. Symmetric Monoidal Categories
- 3.1 Definition
- 3.2 Examples
- 3.3 The category Fsm(?)
- 3.4 The deductive system sm?(?)
- 3.5 The semantics of Der(sm?(?))
- 3.6 The syntax of Fsm(?)
- Chapter 4. Cartesian Categories
- 4.1 Definition
- 4.2 Examples
- 4.3 The category Fc(X)
- 4.4 The deductive system c?(X)
- 4.5 The semantics of Der(c?(X))
- 4.6 The syntax of Fc?(X)
- Chapter 5. Bicartesian Categories
- 5.1 Definition
- 5.2 Examples
- 5.3 The category Fbc(X)
- 5.4 The deductive system bc?(X)
- 5.5 The semantics of Der(bc?(X))
- 5.6 The syntax of Fbc(X)
- Chapter 6. Distributive Bicartesian Categories
- 6.1 Definition
- 6.2 Examples
- 6.3 The category Fdbc(X)
- 6.4 The deductive system dbc?(X)
- 6.5 The semantics of Der(dbc?(X))
- 6.6 The syntax of Fdbc(X)
- Chapter 7. Monoidal Closed Categories
- 7.1 Definition
- 7.2 Examples
- 7.3 The category Fmcl(X)
- 7.4 The deductive system mcl?(X)
- 7.5 The semantics of Der(mcl?(X))
- 7.6 The syntax of Fmcl(X)
- Chapter 8. Symmetric Monoidal Closed Categories
- 8.1 Definition
- 8.2 Examples
- 8.3 The category Fsmcl(X)
- 8.4 The deductive system smcl?(X)
- 8.5 The semantics of Der(smcl?(X))
- 8.6 The syntax of Fsmcl(X)
- Chapter 9. Cartesian Closed Categories
- 9.1 Definition
- 9.2 Examples
- 9.3 The category Fccl(X)
- 9.4 The deductive system ccl?(X)
- 9.5 The semantics of Der(ccl?(X))
- 9.6 The syntax of Fccl(X)
- Chapter 10. Bicartesian Closed Categories
- 10.1 Definition
- 10.2 Examples
- 10.3 The category Fbccl(X)
- 10.4 The deductive system bccl?(X)
- 10.5 The semantics of Der(bccl?(X))
- 10.6 The syntax of Fbccl(X)
- Chapter 12. Monoidal Biclosed Categories
- 12.1 Definition
- 12.2 Examples
- 12.3 The category Fmbcl(X)
- 12.4 The deductive system mbcl?(X)
- 12.5 The semantics of Der(mbcl?(X))
- 12.6 The syntax of Fmbcl(X)
- Chapter 13. Quantifier-Complete Categories
- 13.1 Categorical preliminaries
- 13.2 The language L*(X)
- 13.3 The deductive system ?*(X)
- 13.4 The semantics of Der(?*(X))
- 13.5 The syntax of Fqc(At L*(X))
- Appendix A . The Labelled Deductive System b(X)
- A.1 The class Lb(?X))
- A.2 The axioms of ?(X)
- A.3 The rules of inference of ?(X)
- A.4 The class Der(?(X))
- Appendix B . The Unlabelled Deductive System A(X)
- B.1 The axioms of ?(X)
- B.2 The rules of inference of ?(X)
- B.3 The class Der(?(X))
- Appendix C. The Cut Elimination Algorithm
- Appendix D. The Normalization Algorithm
- Bibliography
- Index of Symbols
- Index of Subjects
