Definite descriptions are ubiquitous in natural languages. Phrases like "the capital of France" or "the youngest sister of Jack" usually do not lead to any problems in communication. However, we can easily run into troubles when we try to provide a satisfactory logical analysis of their behavior. In fact, proper definite decriptions having a unique designatum, are rather not problematic, in contrast to those which fail to designate, called improper (or unfulfilled) definite descriptions. The famous Russellian "the present King of France", is of this kind but even innocent-looking "the son of Jack" may be problematic in case Jack has no son, or more than one.

History of logical and philosophical investigations devoted to the explanation of definite descriptions is fascinating and illuminating. Famous logicians like Frege, Russell, Hilbert, Bernays, Carnap, Quine, Rosser and Hintikka - to mention only a few scholars from the earliest stage of investigation - were strongly engaged in this enterprise. We can find numerous brilliant analyses and even complete formal theories of this apparently simple linguistic phenomenon. Yet, despite the efforts, it can be hardly agreed that a fully satisfactory and commonly accepted theory was provided.

On the other hand, a proof-theoretic apparatus was not yet applied in this field and we would like to explore this possibility. In particular, we will show that the application of techniques taken from modern structural proof theory may shed a new light on the good and bad sides of different approaches to definite descriptions. No prerequisites are assumed. The tutorial will be structured in the following way:

I. Survey of the most important and interesting theories of definite descriptions
In the context of classical logic we will focus on the well known reductionist approach of Russell and the chosen object theory of Frege and its formalization provided by Kalish and Montague. Then we describe some of the theories developed in the framework of free logic by Lambert, Scott, van Fraasen and others. We finish the presentation with three different theories developed on the ground of modal logic by Thomason and Garson, Goldblatt, Fitting and Mendelsohn..

II. Presentation of some elements of proof theory required for further study
We introduce a suitable version of generic sequent calculus, discuss some of its properties, the problem of cut elimination and extension by extra rules. Finally we provide a sequent calculus equivalent to Kalish and Montague version of Fregean theory and prove cut elimination theorem for it.

III. Sequent calculus for modal system based on free logic which is equivalent to Thomason and Garson's theory
We prove cut elimination theorem for this sysrem and discuss some possible extensions of it taken from free logic hierarchy. We provide also a system for Goldblatt's theory and explain why cut rule is not eliminable for it. Finally we consider an open problem of providing a sequent calculus for Fitting and Mendelsohn's theory.

Bibliography