A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation
share
This paper presents a way of formalising definite descriptions with a binary quantifier ι, where ι x[F, G] is read as `The F is G'. Introduction and elimination rules for ι in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ι x[F, G] are given, and it is shown that deductions in the system can be brought into normal form.
READ FULL TEXT