A Cut-Free, Sound and Complete Russellian Theory of Definite Descriptions
Andrzej Indrzejczak, Nils Kürbis · Lecture notes in computer science · 2023
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.