TY - JOUR AU - Kürbis, Nils PY - 2019/06/30 Y2 - 2024/03/28 TI - A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation JF - Bulletin of the Section of Logic JA - B Sect Log VL - 48 IS - 2 SE - Research Article DO - 10.18778/0138-0680.48.2.01 UR - https://czasopisma.uni.lodz.pl/bulletin/article/view/5440 SP - 81-97 AB - <p>This paper presents a way of formalising definite descriptions with a binary quantifier ℩, where ℩<em>x</em>[<em>F</em>, <em>G</em>] is read as `The <em>F</em> is <em>G</em>'. Introduction and elimination rules for ℩&nbsp;in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ℩<em>x</em>[<em>F</em>, <em>G</em>] are given, and it is shown that deductions in the system can be brought into normal form.</p> ER -