Definite Descriptions in Intuitionist Positive Free Logic

TL;DR

This paper develops inference rules for a binary quantifier to formalize definite descriptions in intuitionist positive free logic, ensuring desirable proof properties and comparing with traditional term-based approaches.

Contribution

It introduces a novel binary quantifier approach for definite descriptions within intuitionist free logic, with proven normal form properties.

Findings

The system has desirable proof-theoretic properties.

Deductions can be transformed into normal form.

Comparison with the term-forming operator approach.

Abstract

This paper presents rules of inference for a binary quantifier $I$ for the formalisation of sentences containing definite descriptions within intuitionist positive free logic. $I$ binds one variable and forms a formula from two formulas. $Ix[F, G]$ means `The $F$ is $G$'. The system is shown to have desirable proof-theoretic properties: it is proved that deductions in it can be brought into normal form. The discussion is rounded up by comparisons between the approach to the formalisation of definite descriptions recommended here and the more usual approach that uses a term-forming operator $\iota$, where $\iota xF$ means `the F'.