Two Cases of Deduction with Non-referring Descriptions

TL;DR

The paper addresses the challenge of formalizing non-denoting descriptions within a rigorous logical framework. It develops a partial higher-order type theory $TT^*$ with natural deduction in sequent style ($ND_{TT^*}$) and signed matches to manage non-denoting terms, intensional transitive verbs, and possible-worlds semantics. It then applies the framework to two NL-inspired cases: (i) intensional transitive reasoning with non-referring complements and (ii) Strawsonian existential presuppositions, deriving SPR1–SPR3 as formal rules. The approach offers a constructive, Montague- and Tichý-inspired account that preserves compositionality and provides a proof-theoretic treatment of gappy inferences, offering a new baseline for analyzing non-referring descriptions in formal semantics and NLP tasks.$TT^*$, $ND_{TT^*}$, $ND$, $\iota$, $SPR1$-$SPR3$.

Abstract

Formal reasoning with non-denoting terms, esp. non-referring descriptions such as "the King of France", is still an under-investigated area. The recent exception being a series of papers e.g. by Indrzejczak, Zawidzki and Krbis. The present paper offers an alternative to their approach since instead of free logic and sequent calculus, it's framed in partial type theory with natural deduction in sequent style. Using a Montague- and Tichý-style formalization of natural language, the paper successfully handles deduction with intensional transitives whose complements are non-referring descriptions, and derives Strawsonian rules for existential presuppositions of sentences with such descriptions.

Theorems & Definitions (16)

• Definition 1: Forms of constructions (and of terms of the language $\mathscr{L}_\mathsf{TT^*}$)
• Definition 2: Types $\tau^n$
• Definition 3: Structural rules
• Definition 4: Form rules
• Definition 5: Operational rules
• proof : Proof of (the instance of) (L.=.Desc-E)
• Theorem 1
• proof
• Theorem 2
• proof