Docs / Semantics / Questions / Number

Number in Hamblin sets

import Linglib.Semantics.Questions.Number · namespace Question

This file defines the Hamblin sets of wh phrases over a lattice of pluralities. A situation is identified with the plurality the nucleus holds of, so the member for x is Set.Ici x, and a phrase of number n ranges over the non-null individuals in Sauerland's domain of n, the atoms for a singular phrase and all of them otherwise; a strong plural phrase ranges over the non-atoms (whStrongPlural). Dayal's presupposition on such a Hamblin set holds exactly in the situations of the domain. Under competition in number a plural phrase is then felicitous exactly in the situations that are neither null nor atomic.

References

Dayal 1996, Locality in WH Quantification: Questions and Relative Clauses in Hindi
Dayal 2016, Questions formalized
Sauerland 2003, A new semantics for number formalized
Heim 1991, Artikel und Definitheit

Declarations

The domain of a strong plural wh phrase: the individuals neither null nor atomic.

def whStrongPlural L60–61

{E : Type u_1} [CompleteLattice E] :

Set E

whStrongPlural = {x : E | Number.nonAtomsOf (fun (x : E) => x ≠ ⊥) x}

Used by mem_whStrongPlural, isUpperSet_whStrongPlural

Used in AlonsoOvalleMoghiseh2025b, AlonsoOvalleRouillard2023

Ans-D is defined on the Hamblin set of a wh phrase exactly in the situations its domain contains.

theorem isExhaustivelyResolvable_whHamblin_iff L90–94

{E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Option Number) (w : E) :

IsExhaustivelyResolvable (whHamblin n) w ↔ w ∈ whDomain n

Built from ,

With two atoms, the plural question is felicitous exactly in the situations that are neither null nor atomic.

theorem whFelicitous_plural L135–139

{E : Type u_1} [CompleteLattice E] [IsAtomistic E] {a b : E} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) :

whFelicitous (some Number.plural) = {w : E | w ≠ ⊥ ∧ ¬IsAtom w}

Built from