Fregean Description Theory in Proof-Theoretical Setting

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.