A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic: Natural Deduction and Normalisation

TY - JOUR

T1 - A Binary Quantifier for Definite Descriptions in Intuitionist Negative Free Logic

T2 - Natural Deduction and Normalisation

AU - Kürbis, Nils

PY - 2019/8/12

Y1 - 2019/8/12

N2 - 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.

AB - 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.

KW - Definite descriptions

KW - Natural deduction

KW - Negative intuitionist free logic

KW - Normalization

UR - http://www.scopus.com/inward/record.url?scp=85075992320&partnerID=8YFLogxK

U2 - 10.18778/0138-0680.48.2.01

DO - 10.18778/0138-0680.48.2.01

M3 - Article

SN - 0138-0680

VL - 48

SP - 81

EP - 97

JO - Bulletin of the Section of Logic

JF - Bulletin of the Section of Logic

IS - 2

ER -