Proof-Theory and Semantics for a Theory of Definite Descriptions

DOI10.1007/978-3-030-86059-2_6arXiv2108.03944MaRDI QIDQ6374825

Nils Kürbis

Publication date: 9 August 2021

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.

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: Proof-Theory and Semantics for a Theory of Definite Descriptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6374825)