We present a proof-theoretical analysis of the theory of definite descriptions which emerges from Frege’s approach and was formally developed by Kalish and Montague. This theory of definite descriptions is based on the assumption that all descriptions are treated as genuine terms. In particular, a special object is chosen as a designatum for all descriptions which fail to designate a unique object. Kalish and Montague provided a semantical treatment of such theory as well as complete axiomatic and natural deduction formalization. (...) In the paper we provide a sequent calculus formalization of this logic and prove cut elimination theorem in the constructive manner. (shrink)

In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.