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

TL;DR

The paper addresses formalizing definite descriptions within a Russellian framework by treating them as genuine terms using $\lambda$-abstraction and the $\imath$ operator, producing a reductionist yet expressive logic RL. It introduces a sequent calculus GRL for RL and proves its equivalence to a Hilbert-style system HRL, along with a constructive cut-elimination theorem and a Henkin-style completeness proof. Semantics are defined via lambda-atom satisfaction rather than an interpretation function, enabling DD to be managed through syntactic rules and a specialized satisfaction clause. The work yields a robust, cut-free, complete formal system for DD that supports proof-theoretic analysis, potential intuitionistic variants, and future extensions to modal or free-logics contexts.

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.

Figures (1)

• Figure 1: Calculus GRL

Theorems & Definitions (22)

• lemma 1
• proof
• theorem 1
• lemma 2: Right reduction
• proof
• lemma 3: Left reduction
• proof
• theorem 2
• proof
• lemma 4: The Substitution Lemma.