A Binary Quantifier for Definite Descriptions for Cut Free Free Logics

TL;DR

This paper introduces sequent calculus rules for a binary quantifier to formalise definite descriptions within free logic, extending cut elimination proofs and comparing with other formalisation methods.

Contribution

It provides a novel set of rules for a binary quantifier in free logic and extends existing cut elimination proofs for this system.

Findings

Rules are suitable for positive free logic systems.

Extended proof of cut elimination for the new rules.

Brief comparison with term-forming operator approaches.

Abstract

This paper presents rules in sequent calculus for a binary quantifier $I$ to formalise definite descriptions: $Ix[F, G]$ means `The $F$ is $G$'. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of $I$. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a term forming operator. In the final section rules for $I$ for negative free and classical logic are also mentioned.