A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic

TL;DR

This paper introduces a new approach to formalising definite descriptions using a binary quantifier within Nelson's paraconsistent logic, enabling constructive reasoning about both truth and falsehood while addressing classical issues like Russell's paradox.

Contribution

It develops an embedding and natural deduction system for a binary quantifier in Nelson's logic, enhancing the handling of definite descriptions with constructive falsehood and paraconsistent reasoning.

Findings

Provides an embedding from Nelson's logic into intuitionistic logic

Introduces a natural deduction system with Kripke semantics for the binary quantifier

Offers a novel resolution to Russell's paradox in free logic

Abstract

The method K\"urbis used to formalise definite descriptions with a binary quantifier I, such that I$x[F,G]$ indicates `the F is G', is examined and improved upon in this work. K\"urbis first looked at I in intuitionistic logic and its negative free form. It is well-known that intuitionistic reasoning approaches truth constructively. We also want to approach falsehood constructively, in Nelson's footsteps. Within the context of Nelson's paraconsistent logic N4 and its negative free variant, we examine I. We offer an embedding function from Nelson's (free) logic into intuitionistic (free) logic, as well as a natural deduction system for Nelson's (free) logic supplied with I and Kripke style semantics for it. Our method not only yields constructive falsehood, but also provides an alternate resolution to an issue pertaining to Russell's interpretation of definite descriptions. This comprehension might result in paradoxes. Free logic, which is often used to solve this issue, is insufficiently powerful to produce contradictions. Instead, we employ paraconsistent logic, which is made to function in the presence of contradicting data without devaluing the process of reasoning.