Algebra of Proofs (eBook)

Front Cover 1
Algebra of Proofs 4
Copyright Page 5
Contents 10
Preface 8
Chapter 1. Introduction 14
1.1 Categorical preliminaries 17
1.2 Logical preliminaries 29
Chapter 2. Monoidal Categories 34
2.1 Definition 34
2.2 Examples 35
2.3 The category Fm(.) 36
2.4 The deductive system m.(.) 39
2.5 The semantics of Der(m.(.)) 39
2.6 The syntax of Fm(.) 41
Chapter 3. Symmetric Monoidal Categories 44
3.1 Definition 44
3.2 Examples 45
3.3 The category Fsm(.) 45
3.4 The deductive system sm.(.) 46
3.5 The semantics of Der(sm.(.)) 47
3.6 The syntax of Fsm(.) 48
Chapter 4. Cartesian Categories 53
4.1 Definition 53
4.2 Examples 53
4.3 The category Fc(X) 53
4.4 The deductive system c.(X) 56
4.5 The semantics of Der(c.(X)) 57
4.6 The syntax of Fc.(X) 60
Chapter 5. Bicartesian Categories 67
5.1 Definition 67
5.2 Examples 67
5.3 The category Fbc(X) 68
5.4 The deductive system bc.(X) 70
5.5 The semantics of Der(bc.(X)) 73
5.6 The syntax of Fbc(X) 76
Chapter 6. Distributive Bicartesian Categories 83
6.1 Definition 83
6.2 Examples 84
6.3 The category Fdbc(X) 84
6.4 The deductive system dbc.(X) 86
6.5 The semantics of Der(dbc.(X)) 87
6.6 The syntax of Fdbc(X) 91
Chapter 7. Monoidal Closed Categories 105
7.1 Definition 106
7.2 Examples 106
7.3 The category Fmcl(X) 107
7.4 The deductive system mcl.(X) 109
7.5 The semantics of Der(mcl.(X)) 110
7.6 The syntax of Fmcl(X) 113
Chapter 8. Symmetric Monoidal Closed Categories 120
8.1 Definition 120
8.2 Examples 120
8.3 The category Fsmcl(X) 121
8.4 The deductive system smcl.(X) 122
8.5 The semantics of Der(smcl.(X)) 122
8.6 The syntax of Fsmcl(X) 123
Chapter 9. Cartesian Closed Categories 141
9.1 Definition 141
9.2 Examples 142
9.3 The category Fccl(X) 142
9.4 The deductive system ccl.(X) 144
9.5 The semantics of Der(ccl.(X)) 145
9.6 The syntax of Fccl(X) 147
Chapter 10. Bicartesian Closed Categories 158
10.1 Definition 158
10.2 Examples 165
10.3 The category Fbccl(X) 165
10.4 The deductive system bccl.(X) 166
10.5 The semantics of Der(bccl.(X)) 170
10.6 The syntax of Fbccl(X) 171
Chapter 12. Monoidal Biclosed Categories 191
12.1 Definition 191
12.2 Examples 192
12.3 The category Fmbcl(X) 194
12.4 The deductive system mbcl.(X) 195
12.5 The semantics of Der(mbcl.(X)) 196
12.6 The syntax of Fmbcl(X) 196
Chapter 13. Quantifier-Complete Categories 202
13.1 Categorical preliminaries 204
13.2 The language L*(X) 215
13.3 The deductive system .*(X) 217
13.4 The semantics of Der(.*(X)) 219
13.5 The syntax of Fqc(At L*(X)) 224
Appendix A . The Labelled Deductive System b(X) 232
A.1 The class Lb(.X)) 232
A.2 The axioms of .(X) 232
A.3 The rules of inference of .(X) 233
A.4 The class Der(.(X)) 234
Appendix B . The Unlabelled Deductive System A(X) 237
B.1 The axioms of .(X) 237
B.2 The rules of inference of .(X) 237
B.3 The class Der(.(X)) 238
Appendix C. The Cut Elimination Algorithm 242
Appendix D. The Normalization Algorithm 257
Bibliography 291
Index of Symbols 298
Index of Subjects 304