Question — singleton-alternative predicate #

@cite{bhatt-dayal-2020} @cite{roelofsen-farkas-2015}

A foundational predicate over Question W: an issue is singleton iff its alternative set is a singleton, i.e. there is exactly one maximal resolving proposition. This isolates the algebraic shape that drives several cross-linguistic question-particle analyses:

@cite{bhatt-dayal-2020}'s analysis of Hindi-Urdu kya: (eq. 23): the polar question particle presupposes that its sister denotes a question whose alternative set is a singleton (the "highlighted" cell, in the sense of @cite{roelofsen-farkas-2015}).
the parallel analysis of Mandarin nandao that @cite{bhatt-dayal-2020} fn. 11 cites as the model for kya:.

Declarative contents are exactly the singleton ones (under finiteness of props); the standard two-cell polar polar p (with both p and pᶜ as alternatives) is not singleton when p is non-trivial.

The "highlighted polar" terminology of @cite{roelofsen-farkas-2015} is a notational alias for declarative p in the inquisitive setting; we do not introduce a separate definition because the singleton alternative is the only feature that distinguishes it from the two-cell polar p, and that feature is IsSingleton (declarative p) itself.

Particle-specific bindings (kya:, nandao) live in their respective study files (Phenomena/Questions/Studies/) and use IsSingleton / SingletonQuestion directly.

`IsSingleton` predicate #

source

def Core.Question.IsSingleton {W : Type u} (P : Question W) :

Prop

An inquisitive content is singleton iff its alternative set contains exactly one element. The shape encoded by the singleton presupposition of @cite{bhatt-dayal-2020}'s eq. 23 (kya:) and the parallel nandao analysis cited in @cite{bhatt-dayal-2020} fn. 11.

Equations

P.IsSingleton = ∃ (p : Set W), P.alt = {p}

Instances For

source

theorem Core.Question.isSingleton_declarative {W : Type u} (p : Set W) :

(declarative p).IsSingleton

A declarative p content is singleton — its unique alternative is p itself. The base case for all singleton-presuppositional constructions.

source

@[simp]

theorem Core.Question.isSingleton_top {W : Type u} :

⊤.IsSingleton

source

@[simp]

theorem Core.Question.isSingleton_bot {W : Type u} :

⊥.IsSingleton

source

theorem Core.Question.isSingleton_iff_subsingleton_and_nonempty {W : Type u} (P : Question W) :

P.IsSingleton ↔ P.alt.Subsingleton ∧ P.alt.Nonempty

Subsingleton + nonempty characterization: an issue is singleton iff its alternative set is both Subsingleton and Nonempty in mathlib's sense. Bridges IsSingleton to mathlib's set API.

source

theorem Core.Question.IsSingleton.of_isDeclarative {W : Type u} {P : Question W} (h : P.isDeclarative) :

P.IsSingleton

A declarative content is singleton with witness info P: combines isDeclarative_iff_alt_eq_singleton with the definition of IsSingleton.

source

theorem Core.Question.not_isSingleton_of_two_alternatives {W : Type u} (P : Question W) {p₁ p₂ : Set W} (h₁ : p₁ ∈ P.alt) (h₂ : p₂ ∈ P.alt) (hne : p₁ ≠ p₂) :

¬P.IsSingleton

Two-distinct-alternatives obstruction: if P has two distinct alternatives, P is not singleton. The contrapositive: singleton issues admit at most one alternative. Drives the polar Q failure case below.

source

theorem Core.Question.not_isSingleton_polar_of_nontrivial {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) :

¬(polar p).IsSingleton

The two-cell polar question polar p (in the standard @cite{ciardelli-groenendijk-roelofsen-2018} / Hamblin sense) is not singleton when p is non-trivial — it has two distinct alternatives p and pᶜ. This is the structural reason the @cite{bhatt-dayal-2020} kya:-style "singleton presupposition" cannot be satisfied by a two-cell polar Q; it requires the one-cell highlighted polar of @cite{roelofsen-farkas-2015} (= declarative p).

`SingletonQuestion` subtype #

The mathlib-style packaging of "issue with singleton-alternative presupposition satisfied". Used by particle-specific study files (kya:, nandao) as the type of felicitous sister content.

source

def Core.Question.SingletonQuestion (W : Type u) :

Type u

The subtype of singleton issues — issues whose alternative set is a singleton. Used as the well-typed sister-content for singleton-presuppositional Q-particles (@cite{bhatt-dayal-2020}, kya: eq. 23 and parallel nandao analysis cited in fn. 11). The mathlib pattern for "predicate + partial function" pairs: rather than Option-valued partial interpretation, use a subtype.

Equations

Core.Question.SingletonQuestion W = { Q : Core.Question W // Q.IsSingleton }

Instances For

source

def Core.Question.SingletonQuestion.issue {W : Type u} (Q : SingletonQuestion W) :

Question W

The underlying issue of a SingletonQuestion — the truth-conditional content delivered when the singleton presupposition is satisfied. @cite{bhatt-dayal-2020} eq. 23: ⟦kya:⟧ returns its sister Q unchanged on felicitous inputs.

Equations