摘要：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.
其他摘要：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.
