A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions

TL;DR

This paper introduces a new sequent calculus for a Russellian theory of definite descriptions that is cut-free, sound, complete, and treats descriptions as genuine terms, improving on traditional approaches.

Contribution

It provides a novel, cut-free sequent calculus for a Russellian theory of definite descriptions with constructive and completeness proofs.

Findings

Cut elimination theorem proved constructively

Completeness established via Henkin-style proof

Definite descriptions treated as genuine terms

Abstract

We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution.