Proof-Theory and Semantics for a Theory of Definite Descriptions

TL;DR

This paper develops a sequent calculus and dual domain semantics for a theory of definite descriptions using a binary quantifier, integrating scope distinctions and proving cut elimination, soundness, and completeness.

Contribution

It introduces a novel formal system with a binary quantifier for definite descriptions, differing from traditional term-forming approaches.

Findings

Proves cut elimination for the classical positive free logic system.

Shows the system is sound and complete for the semantics.

Highlights differences from and motivations for diverging from existing theories.

Abstract

This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier $I$. $I$ forms a formula from two formulas. $Ix[F, G]$ means `The $F$ is $G$'. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with $I$ and it is shown to be sound and complete for the semantics. The system has a number of novel features and is briefly compared to the usual approach of formalising `the $F$' by a term forming operator. It does not coincide with Hintikka's and Lambert's preferred theories, but the divergence is well-motivated and attractive.