Resource Logics: Proof-theoretical Investigations [PhD Thesis]

✍ Scribed by Dirk Roorda

• Publisher: University of Amsterdam
• Year: 1991
• Tongue: English
• Leaves: 141
• Category: Library

✦ Synopsis

The KEY TOPIC OF this THESIS is the Lambek calculus. It is a logic on the one hand, and a grammar on the other. The system is studied in different disciplines, having their own interests. The logician asks for completeness and soundness, or more basically, for semantics itself; if he has a hang towards proof theory, he investigates cut elimination and interpolation as well. The linguist is interested in parsing properties, expressive power, and models that are useful for (natural) language interpretation. The latter group of questions is less basic; some of them presuppose answers to the logical questions. But there is a converse direction: the linguist may redirect the eye of the logician into other aspects of the formal systems he deals with. For example, where a logician poses the question of decidability, the linguist would like to know the complexity, or any measure of feasibility that indicates how useful the proposed systems are for the purposes he has in mind. The awareness that resources are limited exists on the side of practical applications, while in theoretical settings those considerations are highly unwelcome. But the tide is turning. Nowadays there are logics that carry the epithet resource-conscious; among them linear logic is the most comprehensive one. Resources come in very different kinds: time, space, effort, proofs, expressions; common to them all is that they are matter-like: if you have two identical pieces of a resource, then you have more than if you had only one piece. This property cannot be ascribed to: truth, knowledge, information.

The EMPHASIS of THIS THESIS is proof-theoretical. This does not mean that other methods and concepts are completely out of the picture. On the contrary, in certain cases we shall use semantics heavily to obtain results that are stated proof-theoretically and ask questions familiar for the computer scientist. But most lines of argument are concerned with proofs and provability. The logical position does not exclude linguistic usefulness. At least two chapters, III and VI, are concerned with questions from the linguistic side.

✦ Table of Contents

Dirk Roorda. Resource Logics: Proof-theoretical Investigations (PhD Thesis, 1991) ......Page 1
Contents ......Page 4
Chapter 1. Introduction ......Page 7
2.1.1 Classical linear logic ......Page 18
2.2 Case analysis of cut applications ......Page 21
2.3 Primitive reductions ......Page 22
2.4.1 Reduction ......Page 26
2.4.2 Inductive proofs ......Page 27
2.5 Cut elimination and strong normalisation: the theorem ......Page 29
3.1 Introduction ......Page 30
3.2.1 The calculi LP and L ......Page 31
3.2.2 Proof nets ......Page 32
3.3.1 Completeness of proof nets w.r.t. LP ......Page 33
3.3.3 Balance ......Page 34
3.4.1 Decomposition ......Page 35
3.4.3 Result ......Page 36
3.5.1 Proof frames and proof structures ......Page 37
3.5.2 Preservation of semantics ......Page 38
3.5.3 Proof net conditions ......Page 39
3.6 Variants ......Page 41
3.7.1 Proof of theorem 5.3.4 ......Page 43
3.7.2 Proof of theorem 5.3.5 ......Page 44
3.7.3 Proof of theorem 5.3.6 ......Page 46
3.7.4 Proof of lemma 5.3.7 ......Page 49
4.1 Proof nets ......Page 51
4.2 Quantum graphs ......Page 52
4.3.1 Colouring quantum graphs ......Page 56
4.3.2 Examples ......Page 57
4.3.3 Correctness of the colouring algorithm ......Page 61
4.4 Theorem proving for Lambek calculus ......Page 63
5.2.1 Fragments ......Page 65
5.2.2 Material ......Page 66
5.3 Constructing interpolants ......Page 67
5.5 Interpolation for type II fragments ......Page 68
5.6.1 Orientation ......Page 71
5.6.2 Statements and proofs ......Page 73
5.6.3 The fragment (—o, •, +) ......Page 74
5.6.4 The fragment (—o, •) ......Page 75
5.6.5 The fragment (—o) ......Page 76
5.6.6 The fragment (—o, +) ......Page 81
5.7 Appendix: Towards the Lambek calculus ......Page 86
5.8 Some open questions ......Page 89
6.1 Introduction ......Page 90
6.2 Possible world models and semigroups ......Page 91
6.3 The first stage: from D to DL ......Page 92
6.3.1 Reasoning in D ......Page 93
6.3.2 Completeness of D ......Page 95
6.3.3 Interaction principles ......Page 97
6.3.4 Lambek calculus lays faithfully embedded in DL ......Page 100
6.3.5 Examples ......Page 101
6.3.6 Decidability for D and extensions ......Page 103
6.4.1 Limit of expressive power of DL ......Page 106
6.4.3 Functionality ......Page 107
6.4.4 Frame characterisation by normal extensions ......Page 108
6.5 Further directions ......Page 109
6.6.1 The proof of theorem 3.6.3, continued ......Page 110
6.6.2 Weak completeness of DD ......Page 114
Bibliography ......Page 123
Samenvatting in het Nederlands ......Page 126
Dankbetuiging ......Page 130
Curriculum Vitae ......Page 131
Index ......Page 132