Theiler, Roelofsen & Aloni (2018) — A Uniform Semantics for Declarative and Interrogative Complements #
@cite{theiler-etal-2018}
Journal of Semantics 35(3): 409–466, doi:10.1093/jos/ffy003.
This study formalizes Section 2 of the paper (semantic framework:
inquisitive sentence meanings) plus the forcing mention-some
example from Section 3.1, which justifies the existence of
Core/Question/Basic.lean as a sibling structure to
Setoid W.
What this file establishes #
Figure 2 examples (Section 2.1, p. 415): the polar interrogative
Did Amy leave?and the declarativeAmy left.constructed via thepolaranddeclarativeconstructors ofQuestion. We prove the four characteristic properties from the paper's prose discussion (Section 2.2):amyLeftis informative and non-inquisitive (declarative).didAmyLeaveis non-informative and inquisitive (polar question).
Mention-some forcing (Section 3.1, ex. (13)): the
Janna knows where one can buy an Italian newspaperscenario adapted from @cite{george-2011} requires alternatives that overlap (a world where two stores both sell Italian newspapers belongs to multiple alternatives). We construct a minimalmentionSomeinquisitive content and provementionSome_not_partition_derived: noSetoid Wproduces this content viafromSetoid.This is the forcing theorem for the architectural decision in the "Architectural note" docstring of
Core/Mood/POSWQ.lean(added 0.229.922) — it shows thatSetoid → Questionis a strictly weaker representation, and so the sibling-structure architecture is necessary rather than redundant.
Scope #
This file does not formalize the rest of the paper:
- Section 3 (false-answer-sensitive truthful resolutions, Definition 3
in §3.3) requires a richer
Eoperator over the inquisitive meaning, which we leave for a follow-up. - Sections 4–6 (verb meanings, predicates of relevance, constraints
on responsive verb meanings) require a full Fragment of attitude
verbs typed against
Question, also future work. - Appendices A–B (comparison with @cite{uegaki-2015} inverse reductive approach; formal proofs).
The point of this file is the existence theorem for the "more
expressive than partitions" claim, which is what the
Core/Question/Basic.lean/Core/Mood/PartitionAsInquiry.lean
pair was built to support.
Section 2.1: Figure 2 — Did Amy leave? / Amy left. #
Worlds: 0, 1 are worlds where Amy left; 2, 3 are worlds where
Amy didn't leave. Following @cite{theiler-etal-2018} Figure 2
(w₁, w₂ = Amy left, w₃, w₄ = Amy didn't leave).
Equations
Instances For
The proposition Amy left — true at worlds w₁, w₂ (= 0, 1).
Equations
Instances For
(6b) Amy left. — Figure 2(b).
Equations
Instances For
(6a) Did Amy leave? — Figure 2(a).
Equations
Instances For
Figure 2(b): Amy left is informative — its informative content excludes the worlds where Amy didn't leave.
Figure 2(b): Amy left is non-inquisitive — declaratives never raise an issue beyond what they assert.
Figure 2(a): Did Amy leave? is non-informative — its informative content covers all worlds (the speaker rules nothing out by asking).
Figure 2(a): Did Amy leave? is inquisitive — it has two
alternatives (amyLeft and amyLeftᶜ), neither of which alone
covers the universe.
Mention-some readings force overlapping alternatives #
The Janna/Rupert scenario from @cite{george-2011} (cited in @cite{theiler-etal-2018} ex. (13)): there are stores Newstopia, Paperworld, and Cellulose City; Newstopia and Paperworld sell Italian newspapers, Cellulose City does not. Janna knows where one can buy an Italian newspaper under a mention-some reading is true if Janna knows of any one such store. Critically, in worlds where multiple stores sell, those worlds belong to multiple alternatives (one per store) — the alternatives overlap.
The structural feature — non-disjoint alternatives — is what
@cite{theiler-etal-2018} §2 (Figure 5(b), the non-exhaustive Who
left?) and the broader inquisitive-semantics tradition (e.g.,
@cite{ciardelli-groenendijk-roelofsen-2018}) use to motivate the move
beyond partition theory. We model the irreducible structural feature
with three worlds and two overlapping alternatives. The forcing
theorem mentionSome_not_partition_derived shows that no Setoid on
these three worlds can generate this content via fromSetoid.
World universe for the mention-some example: three worlds.
Equations
Instances For
Alternative 1: Newstopia sells Italian newspapers — true in
worlds 0 and 1.
Equations
Instances For
Alternative 2: Paperworld sells Italian newspapers — true in
worlds 1 and 2. World 1 is where both stores sell, so it
sits in both alternatives — this is the structural feature that
a Setoid cannot represent.
Equations
Instances For
The mention-some inquisitive content for where one can buy an
Italian newspaper: a state resolves the issue iff every world in
it agrees on at least one of the two stores selling. The
alternatives are msNewstopia and msPaperworld, which overlap
at world 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Forcing theorem (the architectural justification for
Question). The mention-some content is not in the
image of fromSetoid for any Setoid on the three worlds.
Proof: msNewstopia = {0, 1} and msPaperworld = {1, 2} both lie
in mentionSome.props. If fromSetoid r = mentionSome, each must
be contained in some equivalence class of r. Since both contain
world 1, those classes coincide; so worlds 0, 1, and 2 all
lie in one class. Then {0, 2} is also in
(fromSetoid r).props = mentionSome.props, but {0, 2} is not a
subset of msNewstopia (missing 2) nor of msPaperworld
(missing 0) — contradiction.
This is the standard partition-theory limitation that motivates inquisitive semantics' move to non-disjoint alternatives (@cite{ciardelli-groenendijk-roelofsen-2018}; @cite{theiler-etal-2018} §2 Figure 5(b)).