A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation
Logic in Computer Science
2021-08-12 v1 Logic
Abstract
This paper presents a way of formalising definite descriptions with a binary quantifier , where is read as `The is '. Introduction and elimination rules for in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form are given, and it is shown that deductions in the system can be brought into normal form.
Cite
@article{arxiv.2108.01976,
title = {A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation},
author = {Nils Kürbis},
journal= {arXiv preprint arXiv:2108.01976},
year = {2021}
}