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

TL;DR

This paper introduces a binary quantifier for definite descriptions within intuitionist negative free logic, providing formal rules and normalization procedures to enhance logical representation and deduction.

Contribution

It formalizes a binary quantifier for definite descriptions and develops introduction, elimination, and normalization rules in intuitionist negative free logic.

Findings

Defined a binary quantifier $$ for definite descriptions

Formulated introduction and elimination rules for the quantifier

Established procedures for normalization of deductions

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.