A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation

Abstract

This paper presents a way of formalising definite descriptions with a binary quantifier $\iota$, where $\iota x[F,G]$ is read as `The $F$ is $G$'. Introduction and elimination rules for $\iota$ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form $\iota x[F,G]$ are given, and it is shown that deductions in the system can be brought into normal form.

Cited by in corpus (7)

• A Binary Quantifier for Definite Descriptions for Cut Free Free Logics
• Definite Descriptions in Intuitionist Positive Free Logic
• A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions
• Incomplete Descriptions and Qualified Definiteness
• Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators
• A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic
• Russell's Theory of Definite Descriptions in the Light of Structural Proof Theory