Linear logic (Girard,1987) sprouts from the remarkable observation that a certain semantical decomposition of intuitionistic type constructors corresponds on a syntactical level to the banning of structural rules of weakening and contraction from the formulation of intuitionistic'logic as a sequent calculus, followed by their resurrection in modalized form. It then is a small, but important, step to apply this latter, purely formal, manipulation to sequent calculi also for classical logic, and marvel at the consequences.
Soon following its introduction, linear logic became the topic of a quickly growing number of research- and survey-papers, and inspired workers in proof theory, category theory, complexity theory, theoretical and not-so-theoretical computer science, all eager to explore the possible, impossible, the more, as well as the less, probable, implications and applications. As a result, in much less than a decade, the field has become so extensive, that, in the present context, we will not even try to give a comprehensive overview.
The optic of this thesis, then, is a fairly modest one: linear sequent calculus appears as a refinement of the known calculi for both intuitionistic and classical logic. It therefore can be considered a tool to investigate, as if through a microscope, behaviour and properties of intuitionistic and classical sequent derivations.
It is on a such proof theoretical study that we will embark.
Author(s): Harold Schellinx
Series: ILLC Dissertation Series DS-1994-01
Publisher: University of Amsterdam
Year: 1994
Language: English
Commentary: Scan & djvu by Envoy
Pages: 208
City: Amsterdam
Preface ......Page 7
Table of contents ......Page 9
Guide ......Page 13
1. Linear logic ......Page 17
1 Theme ......Page 21
2 Weakening and contraction ......Page 25
3 Deconstructing intuitionistic logic ......Page 29
Notes ......Page 33
2. Embeddings ......Page 36
1 Embedding IL into CLL ......Page 37
2 Modal logic ......Page 40
3 Embedding system F ......Page 43
4 Decomposing classical logic ......Page 46
Notes ......Page 49
3. Decorations ......Page 50
1 Plethoric translations I ......Page 51
2 ILU and (sub)Girardian decorations ......Page 54
3 Plethoric translations II ......Page 60
4 LKT and LKQ ......Page 66
5 Constructive classical logic ......Page 75
Notes ......Page 83
4. Decorating intuitionistic derivations ......Page 85
1 The lower decoration strategy I ......Page 86
2 Decorating ILU ......Page 98
3 Decoration and normalization ......Page 100
4 Decorating classical derivations ......Page 109
Notes ......Page 111
5. The exponential graph ......Page 112
1 Identity classes ......Page 113
2 Stripping derivations ......Page 114
3 The 'mono-stable' fragment of CLL2 ......Page 117
4 Strips and normalization ......Page 119
5 Plethoric translations III ......Page 124
6 The lower decoration strategy II ......Page 128
Notes ......Page 130
6. Constrictive morphisms ......Page 132
1 Decorating the identity ......Page 133
2 Correction cuts ......Page 139
3 Mapping IL to ILU ? ......Page 142
4 ? and CL to LKT, LKQ ......Page 149
7. Multicolour linear logic ......Page 152
1 R-CLL ......Page 153
2 A prelude to dilatation ......Page 156
Notes ......Page 158
1 Dilated linear logic ......Page 159
2 A characterization of 1+-dilatable derivations ......Page 166
3 Acyclic linear logic ......Page 170
References ......Page 173
Appendix A. Terminological conventions ......Page 178
Appendix B. Classical linear logic (CLL) ......Page 181
Appendix C. Classical logic (CL) ......Page 185
Appendix D. Intuitionistic logic (IL) ......Page 187
Appendix E. Multi-succedent IL (IL>) ......Page 190
Index ......Page 192
Acknowledgements ......Page 195
Beknopte weergave ......Page 197
Stellingen ......Page 201
Previous titles in the ILLC Dissertation Series ......Page 207
