Resource Logics: Proof-theoretical Investigations [PhD Thesis]

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.