[CGR18]: Inquisitive Semantics

[frege-1918] [Hin62] [Sta78] [hamblin-1973] [Kar77b] [GS84] [Pun19]

Substrate-audit study file for [CGR18] Inquisitive Semantics (OUP, Oxford Surveys in Semantics and Pragmatics 6). The substrate of Semantics/Questions/ IS this paper's formalisation: every CGR Chapter-2 and Chapter-3 definition has a direct counterpart in Question. This file's job is to make the correspondence explicit, by (a) docstring-mapping each CGR definition to its substrate identifier and (b) re-proving the key CGR facts on the substrate so that the substrate is verifiably faithful to CGR.

Unique among Studies/ files: this is not a paper replication (building the paper's machinery from scratch and showing it agrees with the substrate) — it is a paper audit (confirming the substrate already implements the paper).

Substrate identification table

Chapter 2 — Basic notions

[CGR18]	substrate
Def 2.1 Information state s ⊆ W	Set W (mathlib)
Def 2.2 Enhancement t ⊆ s	set inclusion
Def 2.3 Issue (non-empty downward-closed set of states)	Question W
Def 2.4 Resolution s ∈ I	s ∈ I.props ≡ Support.supports s I
Def 2.5 Issues over a state ⋃I = s	info I = s
Def 2.6 Refinement I ⊆ J	(I : Question W) ≤ J
Def 2.7 Alternatives in an issue (max elts)	Question.alt
Fact 2.8 Multi-alts iff proper (finite case)	isInquisitive_of_two_alternatives (one direction; full equivalence under Q.props.Finite)
Def 2.9 Proposition (non-empty downward-closed)	Question W (same as Issue)
Def 2.10 Informative content info(P) := ⋃P	Question.info
Def 2.11 Issue embodied by P	P itself
Def 2.12 Truth w ∈ info(P)	w ∈ info P
Def 2.13 Support s ∈ P	Support.supports s P
Fact 2.14 Truth = singleton support	truth_iff_singleton_support
Def 2.15 Informative / Inquisitive	isInformative / isInquisitive
Def 2.16 Alternatives in a proposition	Question.alt
Fact 2.17 Inquisitive iff multi-alts (finite)	(specialisation of Fact 2.8)
Fact 2.18 Non-inquisitive ↔ info(P) ∈ P	isDeclarative_iff_not_isInquisitive (substrate uses isDeclarative for "non-inquisitive")
Fact 2.19 Non-inquisitive characterizations	isDeclarative_iff_eq_declarative_info
Def 2.20–2.22 Entailment P ⊨ Q ↔ P ⊆ Q	substrate's ≤ (le_def)
Fact 2.23 Entailment as support preservation	by le_def
Def 2.24 Tautology ⊤ := ℘(W), contradiction ⊥ := {∅}	top / bot
Fact 2.25 Partial order on propositions	inferInstance : CompleteLattice
Def 2.26 Context (= proposition)	Question W
Def 2.27 info(C) := ⋃C	Question.info
Def 2.28-2.32 Informed/inquisitive contexts	isInformative / isInquisitive
Def 2.30 Initial / absurd contexts	⊤ / ⊥
Def 2.35 Update C[P] := C ∩ P	C ⊓ P (substrate's inf)
Fact 2.36 Update reduces to standard on non-inquisitive	update_non_inquisitive_eq_intersection

Chapter 3 — Basic operations

[CGR18]	substrate
Fact 3.1 Meet ⋂Σ = {s \| s ∈ P ∀ P ∈ Σ}	sInf / sInfContent
Fact 3.2 Join ⋃Σ = {s \| s ∈ P ∃ P ∈ Σ}	sSup / sSupContent
Fact 3.3 Relative pseudo-complement P ⇒ Q	substrate's Heyting ⇨ (HeytingAlgebra instance)
Fact 3.4 Absolute pseudo-complement P*	substrate's Pᶜ
Fact 3.5 P* = ℘(¬info(P))	compl_eq
Def 3.8-3.9 Decision set D(P) := P ∪ P*	derived from inqDisj P Pᶜ
Def 3.13 Projection !P := ℘(info(P))	proj
Def 3.13 Projection ?P := P ∪ P*	nonInfo
Fact 3.14 Division P = !P ⊓ ?P	proj_inf_nonInfo
Fact 3.15 !P = P**, ?P = P ∪ P*	proj_eq_compl_compl

Chapter 5 — Questions

[CGR18]	substrate
§5.1 Polar ?Mab := Mab ∨ ¬Mab	Question.polar
§5.2 Alternative Mab ∨ Mac	declarative Mab ⊔ declarative Mac
§5.3 Open disjunctive ?(Mab ∨ Mac)	nonInfo (declarative Mab ⊔ declarative Mac)
§5.4.1 Mention-all wh ∀x?Pax	(substrate's [Kar77b] which modulo ?)
§5.4.2 Mention-some wh ∃xLax	Question.which (Hamblin disjunction)
§5.5.1 Conjoined Q ∧ Q'	Q ⊓ Q' (substrate's inf)
§5.5.2 Disjoined Q ∨ Q'	Q ⊔ Q' (substrate's sup)
§5.5.3 Conditional if A, Q ↦ A → Q	substrate's Heyting A ⇨ Q

What this file does NOT cover

• Ch 4 First-order syntax (the InqB logical language): the substrate is at the meaning side (Question W); the syntactic translation layer is not formalised here.
• Ch 6 Disjunction, clause typing, intonation: partial coverage in Semantics/Mood/ and the focus studies (Studies/Rooth1992.lean).
• Ch 7 Conditionals: the substrate exposes ⇨ via the HeytingAlgebra instance; [CGR18] Ch 7's full empirical analysis lives in Semantics/Conditionals/ and study files there.
• Ch 8 Inquisitive epistemic logic / know and wonder: see Semantics/Attitudes/ and Studies/TheilerRoelofsenAloni2018.lean.
• Ch 9 Comparison with alternative semantics, partition semantics, inquisitive indifference: covered piecemeal in Studies/{Hamblin1973_TODO, GroenendijkStokhof1984}.lean (alt and partition) and Semantics/Questions/ (as topical bridges).

§2.4.1 Truth and support

[CGR18] Fact 2.14: a proposition is true at a world iff it is supported by the singleton state. The substrate-level proof uses info and downward_closed.

theorem CiardelliGroenendijkRoelofsen2018.truth_iff_singleton_support {W : Type u} (P : Question W) (w : W) : w ∈ P.info ↔ {w} ∈ P

[CGR18] Fact 2.14 (Truth and support): P is true at w iff P is supported by {w}.

§2.4.2 Informative and inquisitive propositions

[CGR18] Fact 2.18: substrate has isDeclarative for "non-inquisitive". Re-state Fact 2.18's three disjuncts under substrate names.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_18_non_inquisitive_iff {W : Type u} (P : Question W) : ¬P.isInquisitive ↔ P.isDeclarative

[CGR18] Fact 2.18 (i): non-inquisitive iff info(P) ∈ P. The substrate's isDeclarative IS this condition by definition.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_18_non_informative_iff {W : Type u} (P : Question W) : ¬P.isInformative ↔ P.info = Set.univ

[CGR18] Fact 2.18 (ii): non-informative iff info(P) = W. The substrate's isInformative is "informative content excludes some world", so non-informative is the negation.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_18_tautology_iff {W : Type u} (P : Question W) : P = ⊤ ↔ Set.univ ∈ P

[CGR18] Fact 2.18 (iii): P is a tautology iff W ∈ P.

§2.4.2 Fact 2.19 — Non-inquisitive characterizations

[CGR18] Fact 2.19 lists four equivalent characterizations of non-inquisitivity. The substrate has the isDeclarative_iff_eq_declarative_info form (corresponding to characterization 2 in the chain). The other directions follow.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_19_eq_declarative_info {W : Type u} (P : Question W) : P.isDeclarative ↔ P = Question.declarative P.info

[CGR18] Fact 2.19 (1↔2): non-inquisitive iff P = ℘(info(P)) (the principal-ideal characterization). The substrate-level isDeclarative_iff_eq_declarative_info IS this.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_19_truth_conditional {W : Type u} (P : Question W) (h : P.isDeclarative) (s : Set W) : s ∈ P ↔ ∀ w ∈ s, w ∈ P.info

[CGR18] Fact 2.19 (4): non-inquisitive iff P is supported by s exactly when P is true at every world in s (truth-conditional support). Direct consequence of truth_iff_singleton_support + downward closure.

§2.5 Contexts and update

[CGR18] Def 2.35: update is C[P] := C ∩ P — the substrate's lattice meet ⊓. Fact 2.36: when both C and P are non-inquisitive (i.e., declaratives), the update reduces to the standard intersection on informative content.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_35_update_eq_inf {W : Type u} (C P : Question W) : (C ⊓ P).props = C.props ∩ P.props

[CGR18] Def 2.35: update IS the substrate meet operation. Tautology — substrate-⊓ was defined pointwise on props. Stated as a theorem to anchor the substrate's inf to CGR's [·] notation.

theorem CiardelliGroenendijkRoelofsen2018.CGR_2_36_update_non_inquisitive {W : Type u} (C P : Question W) (hC : C.isDeclarative) (hP : P.isDeclarative) : (C ⊓ P).isDeclarative ∧ (C ⊓ P).info = C.info ∩ P.info

[CGR18] Fact 2.36 (Update without inquisitiveness reproduces standard results): if both C and P are non-inquisitive, then their update is again non-inquisitive, with informative content equal to the standard intersection of the inputs' informative contents.

§3.1.2 Algebraic operations on inquisitive propositions

[CGR18] Facts 3.1, 3.2, 3.5 and the projection-related Facts 3.13–3.15. The substrate already provides these as sInf, sSup, compl_eq, proj, nonInfo, and their respective theorems. The bridge theorems below give the CGR formulations directly on the substrate's vocabulary.

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_1_meet {W : Type u} (S : Set (Question W)) (s : Set W) : s ∈ sInf S ↔ ∀ P ∈ S, s ∈ P

[CGR18] Fact 3.1 (Meet): arbitrary meet has support iff every member supports. Substrate-side: sInfContent is defined this way; restate to expose the CGR membership iff.

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_2_join {W : Type u} (S : Set (Question W)) (s : Set W) : s ∈ sSup S ↔ s = ∅ ∨ ∃ P ∈ S, s ∈ P

[CGR18] Fact 3.2 (Join): arbitrary join has support iff some member supports (or s = ∅). The substrate-side mem_sSup_props exposes the disjunctive structure. The CGR formulation special-cases the empty family to {∅} = ⊥; the substrate gets this from the s = ∅ clause.

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_5_pseudo_complement {W : Type u} (P : Question W) : Pᶜ = Question.declarative P.infoᶜ

[CGR18] Fact 3.5 (Absolute pseudo-complement, alternative characterization): P* = ℘(¬info(P)). The substrate's compl_eq IS this — Pᶜ = declarative (info P)ᶜ, and declarative q = ℘(q) (principal ideal).

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_13_proj_eq {W : Type u} (P : Question W) : P.proj = Question.declarative P.info

[CGR18] Def 3.13 (Projection operators): !P := ℘(info(P)) is the substrate's proj; ?P is nonInfo P := P ⊔ Pᶜ.

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_13_nonInfo_eq {W : Type u} (P : Question W) : P.nonInfo = P ⊔ Pᶜ

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_14_division {W : Type u} (P : Question W) : P = P.proj ⊓ P.nonInfo

[CGR18] Fact 3.14 (Division): every proposition decomposes uniquely as the meet of its non-inquisitive projection and its non-informative projection. Substrate's proj_inf_nonInfo.

theorem CiardelliGroenendijkRoelofsen2018.CGR_3_15_proj_eq_compl_compl {W : Type u} (P : Question W) : P.proj = Pᶜᶜ

[CGR18] Fact 3.15 (Projection operators in algebraic terms): !P = P**. Substrate's proj_eq_compl_compl.

§5.1 Polar questions

[CGR18] §5.1: the polar question ?Mab (Is Alice married to Bob?) is the inquisitive disjunction of the proposition Mab and its complement. The substrate primitive polar IS this construction.

theorem CiardelliGroenendijkRoelofsen2018.CGR_5_1_polar_eq {W : Type u} (p : Set W) : Question.polar p = Question.declarative p ⊔ Question.declarative pᶜ

[CGR18] §5.1: substrate identification of the polar question. The substrate's polar p expands to declarative p ⊔ declarative pᶜ, matching CGR's definition ?p := p ∨ ¬p since on declarative propositions ¬p reduces to declarative pᶜ.

§5.4 Wh-questions

[CGR18] §5.4.2: the mention-some wh-question ∃xLax (What is something Alice likes?) is the inquisitive disjunction (= Hamblin disjunction) of declaratives {|Lad| | d ∈ D}↓. The substrate primitive which D P IS this construction.

theorem CiardelliGroenendijkRoelofsen2018.CGR_5_4_2_which_resolution {W : Type u} {E : Type u_1} (D : Set E) (P : E → Set W) (s : Set W) : s ∈ Question.which D P ↔ s = ∅ ∨ ∃ e ∈ D, s ⊆ P e

[CGR18] §5.4.2 substrate identification: the mention-some wh-question denotation ∃xLax matches the substrate's which D L Hamblin disjunction. The ↓ notation in CGR is downward closure, which is automatic in the substrate (Question is a LowerSet).

§5.5 Question coordination

[CGR18] §5.5: question conjunction and disjunction are uniformly the lattice meet and join, exactly as they are for declaratives. The substrate's ⊓/⊔ IS this. The identification is automatic — there's no separate "question conjunction" operator.

theorem CiardelliGroenendijkRoelofsen2018.CGR_5_5_1_conj_eq_inf {W : Type u} (Q Q' : Question W) : Q ⊓ Q' = Q.conj Q'

[CGR18] §5.5.1: question conjunction reduces to substrate ⊓. The CGR claim is that the InqB translation of "Q and Q'" is μ ∧ μ' — same operator as for declaratives. The substrate's Question.conj = ⊓ IS this.

theorem CiardelliGroenendijkRoelofsen2018.CGR_5_5_2_disj_eq_sup {W : Type u} (Q Q' : Question W) : Q ⊔ Q' = Q.inqDisj Q'

[CGR18] §5.5.2: question disjunction reduces to substrate ⊔.

Closing observation

The substrate-side coverage of [CGR18] Chapters 2, 3, and 5 is essentially complete: every CGR primitive has a direct substrate counterpart with matching semantics. The only non-trivial added structure on the substrate side is the SetLike (Question W) (Set W) instance and the CompleteDistribLattice registration — both of which are mathlib-style ergonomic upgrades that don't change the underlying mathematics.

This audit is load-bearing: it documents that the substrate's Question W = LowerSet (Set W) design is the [CGR18] inquisitive proposition, with the same algebraic and order-theoretic structure. Future substrate refactors should preserve these identifications.