POSW with Inquiry Partition (POSWQ)

@cite{portner-2018} @cite{groenendijk-stokhof-1984} @cite{roberts-2012}

This file is our extension of @cite{portner-2018}'s POSW substrate to interrogative force, by way of a third component recording the open question. It is not the extension Portner himself works out. Portner's interrogative variant — PPOSW — replaces cs with a partition of cs, so the "informational" and "inquisitive" components are fused. We instead keep cs intact and add inquiry : Setoid W as a separate third coordinate; this preserves Portner's disjoint-target story (+, ⋆, ? each touch one component) and lets the inquiry partition compose orthogonally with cs-refinement and ≤-refinement.

The third-component idea is grounded in the dynamic-question tradition: @cite{groenendijk-stokhof-1984}'s partition theory takes the meaning of a question to be an equivalence relation on worlds; @cite{roberts-2012} maintains a QUD stack alongside the common ground; inquisitive semantics (Ciardelli et al. 2013) folds it into a single informative/inquisitive content. The Setoid representation makes the partition view directly available via mathlib's CompleteLattice (Setoid W).

The 3×3 Portner-style unification

layer	declarative	imperative	interrogative
sentence mood	assertion (+)	direction (⋆)	inquiry (?)
modal necessity	boxCs	boxLe	boxAns
verbal mood	.indicative	(no analogue)	.interrogative

The columns are the three POSW components (cs, le, inquiry); the rows are the operations on each component (refining update, quantification). Refinement of the inquiry partition (?-update), the modal boxAns, and the third column entries are this library's extensions; they do not appear in @cite{portner-2018}.

Mathlib alignment

• inquiry : Setoid W uses mathlib's CompleteLattice (Setoid W) instance directly: ⊓ for partition meet (jointly-finer), ≤ for refinement (finer ≤ coarser).
• The Setoid ≤ convention (r ≤ s ↔ ∀ x y, r x y → s x y) coincides with the POSW refinement preorder convention from Linglib/Core/Mood/POSW.lean §4: finer ≤ coarser, more discriminating ≤ less discriminating.
• extends POSW W mirrors Group extends Monoid: a POSWQ is a POSW (via the auto-generated POSWQ.toPOSW) plus extra structure.

Three-lattice unification (third corner)

The POSWQ ?-update is the third corner of the linglib lattice unification described in Mood/POSW.lean's "Lattice unification" docstring: each of cs, le, inquiry carries a mathlib lattice, and each of +, ⋆, ? is meet in its component's lattice. The inquiry corner uses Setoid.completeLattice α (mathlib), so the ?-update inherits not just inf but iInf over arbitrary index sets — reading off "asking the conjunction of a family of questions" as iInf is then a one-line consequence. The ?-update inherits inf_assoc, inf_idem, and inf_comm directly (inquire_inquire_self in §7 is a one-liner via inf_assoc + inf_idem).

Architectural note: Setoid vs. InquisitiveContent

We commit inquiry : Setoid W (partition-based questions). The state-of-the-art generalization is the algebraic / inquisitive- semantics frame of @cite{puncochar-2016} (lattice-of-logics characterization, with inquisitive logic as the strongest "G-logic"), @cite{puncochar-2019} (information models on substructural bases; declarative propositions as principal ideals), and @cite{ciardelli-groenendijk-roelofsen-2018} (the textbook), in which inquiry would be a downward-closed nonempty set of information states rather than a partition. That generalization handles non-partition inquiry — mention-some, intermediate-exhaustive, and conditional question phenomena — that Setoid W provably cannot represent (partition cells are disjoint and exhaustive).

We do not lift to InquisitiveContent W here. Following mathlib discipline, the lift should be triggered by a forcing phenomenon study, not built speculatively. The clearest forcing candidate is @cite{theiler-etal-2018}'s uniform semantics for declarative and interrogative complements, which derives mention-some and intermediate-exhaustive readings as theorems and shows that @cite{groenendijk-stokhof-1984}'s partition theory provably cannot. When that study is formalized in Phenomena/Attitudes/Studies/, the InquisitiveContent W type becomes load-bearing; until then, every existing POSWQ use case is partition-based and Setoid W is the right structure (mathlib already provides its CompleteLattice).

The lift, when it happens, should be a sibling structure (parallel to Setoid, with Setoid → InquisitiveContent as a faithful embedding) rather than a replacement — mirroring how mathlib keeps Set/Finset and Filter/Ultrafilter parallel rather than collapsing them.

structure Core.Mood.POSWQ (W : Type u) extends Core.Mood.POSW W : Type u

A POSW with an inquiry partition (POSWQ): the @cite{portner-2018} POSW substrate enriched with a third component recording the open question. The inquiry : Setoid W partitions worlds into "answers"; its ⊤ element is "no question". This three-coordinate extension is ours and is distinct from @cite{portner-2018}'s own PPOSW (which replaces cs with a partition rather than adding a third field).

• cs : W → Prop
• le : W → W → Prop
• le_refl (w : W) : self.cs w → self.le w w
• le_trans (w u v : W) : self.cs w → self.cs u → self.cs v → self.le w u → self.le u v → self.le w v
• inquiry : Setoid W

  The inquiry partition: inquiry.r w v means worlds w and v are indistinguishable answers to the open question.

§1. Constructors

def Core.Mood.POSWQ.ofPOSW {W : Type u} (c : POSW W) : POSWQ W

Lift a POSW to a POSWQ with no question under discussion (trivial inquiry partition: every world is in the same cell).

Equations

• Core.Mood.POSWQ.ofPOSW c = { toPOSW := c, inquiry := ⊤ }

@[simp]

theorem Core.Mood.POSWQ.ofPOSW_toPOSW {W : Type u} (c : POSW W) : (ofPOSW c).toPOSW = c

@[simp]

theorem Core.Mood.POSWQ.ofPOSW_inquiry {W : Type u} (c : POSW W) : (ofPOSW c).inquiry = ⊤

def Core.Mood.POSWQ.polarSetoid {W : Type u} (q : W → Prop) : Setoid W

The polar Setoid of a proposition q : W → Prop: two worlds are equivalent iff they agree on q. The smallest piece of partition structure a single proposition can contribute to an inquiry. The Setoid lattice's ⊤ is the trivial inquiry (q = ⊤), and meeting two polar Setoids gives the polar Setoid for the conjunction (up to logical equivalence).

Distinct from mathlib's Setoid.ker q, which uses = on propositions rather than ↔; we keep ↔ to make polarSetoid_r definitionally Iff.rfl.

Equations

• Core.Mood.POSWQ.polarSetoid q = { r := fun (w v : W) => q w ↔ q v, iseqv := ⋯ }

@[simp]

theorem Core.Mood.POSWQ.polarSetoid_r {W : Type u} (q : W → Prop) (w v : W) : (polarSetoid q) w v ↔ (q w ↔ q v)

@[simp]

theorem Core.Mood.POSWQ.polarSetoid_top {W : Type u} : (polarSetoid fun (x : W) => True) = ⊤

§2. The third update: ? (inquiry refinement)

def Core.Mood.POSWQ.inquire {W : Type u} (c : POSWQ W) (q : Setoid W) : POSWQ W

?-update (our extension; not in @cite{portner-2018}): refine the inquiry partition by meet with q. The partition-side analogue of +-update on cs and ⋆-update on le: it constrains the third POSW component without touching the other two.

The meet of two equivalence relations on W is "agree on both"; refining the inquiry by q shrinks each cell down to its intersection with q's cells (jointly-finer partition).

Equations

• c.inquire q = { toPOSW := c.toPOSW, inquiry := c.inquiry ⊓ q }

@[simp]

theorem Core.Mood.POSWQ.inquire_toPOSW {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).toPOSW = c.toPOSW

@[simp]

theorem Core.Mood.POSWQ.inquire_cs {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).cs = c.cs

@[simp]

theorem Core.Mood.POSWQ.inquire_le {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).le = c.le

theorem Core.Mood.POSWQ.inquire_inquiry {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).inquiry = c.inquiry ⊓ q

@[simp]

theorem Core.Mood.POSWQ.inquire_inquiry_eq_inf {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).inquiry = c.inquiry ⊓ q

?-update is meet in Setoid.completeLattice W. The inquiry-side analogue of POSW.plus_cs_eq_inf (meet in W → Prop) and POSW.star_le_eq_inf (meet in W → W → Prop). Definitional.

§3. The third modal: boxAns (informational answerhood)

def Core.Mood.POSWQ.boxAns {W : Type u} (c : POSWQ W) (p : W → Prop) : Prop

Informational answerhood (our extension): p is settled by the question at c iff p has a constant truth value within every cell of c.inquiry (restricted to the context set). The answerhood counterpart of @cite{portner-2018}'s boxCs (truth throughout cs) and boxLe (truth at every best world); the formulation is closest in spirit to @cite{groenendijk-stokhof-1984} answerhood.

Unlike boxCs and boxLe, boxAns is not upward-monotone in p: a strengthening of p can break the constant-truth property on a cell. The natural monotonicity for boxAns is anti-monotone in the inquiry partition (boxAns_anti below).

Equations

• c.boxAns p = ∀ (w v : W), c.cs w → c.cs v → c.inquiry w v → (p w ↔ p v)

§4. Disjointness of components

The +-, ⋆-, and ?-updates target disjoint components of the POSWQ. The first two leave inquiry alone (vacuously, since they're defined on the underlying POSW), and ?-update leaves both cs and le alone. The Portner unification thesis extends to three columns.

theorem Core.Mood.POSWQ.inquire_targets_disjoint_components {W : Type u} (c : POSWQ W) (q : Setoid W) : (c.inquire q).cs = c.cs ∧ (c.inquire q).le = c.le

§5. Refinement preorder

POSWQ W inherits a refinement preorder componentwise from POSW W's refinement preorder (Mood/POSW.lean §4) and the Setoid W lattice: c₁ ≤ c₂ iff c₁.toPOSW ≤ c₂.toPOSW and c₁.inquiry ≤ c₂.inquiry. Both directions agree on "finer ≤ coarser".

@[implicit_reducible]

instance Core.Mood.POSWQ.instPreorder {W : Type u} : Preorder (POSWQ W)

Equations

• Core.Mood.POSWQ.instPreorder = { le := fun (c₁ c₂ : Core.Mood.POSWQ W) => c₁.toPOSW ≤ c₂.toPOSW ∧ c₁.inquiry ≤ c₂.inquiry, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Core.Mood.POSWQ.le_iff {W : Type u} (c₁ c₂ : POSWQ W) : c₁ ≤ c₂ ↔ c₁.toPOSW ≤ c₂.toPOSW ∧ c₁.inquiry ≤ c₂.inquiry

theorem Core.Mood.POSWQ.inquire_le_self {W : Type u} (c : POSWQ W) (q : Setoid W) : c.inquire q ≤ c

?-update lands below the input: refining inquiry by meet with q can only constrain the POSWQ further. The third-component analogue of POSW.plus_le_self and POSW.star_le_self.

theorem Core.Mood.POSWQ.inquire_mono {W : Type u} {c₁ c₂ : POSWQ W} (h : c₁ ≤ c₂) (q : Setoid W) : c₁.inquire q ≤ c₂.inquire q

?-update is monotone in the underlying POSWQ.

theorem Core.Mood.POSWQ.boxAns_anti {W : Type u} (c₁ c₂ : POSWQ W) (h : c₁ ≤ c₂) (p : W → Prop) : c₂.boxAns p → c₁.boxAns p

Refining the POSWQ strengthens informational answerhood: if c₁ is more refined than c₂ and p is settled by the question at c₂, then p is settled at c₁ too. The answerhood counterpart of POSW.boxCs_anti.

§6. Closure properties of boxAns

boxAns p says "p is constant on each inquiry cell within cs". This class of propositions is closed under the standard logical operations — answers to a question can be combined like ordinary propositions.

theorem Core.Mood.POSWQ.boxAns_not {W : Type u} (c : POSWQ W) (p : W → Prop) : c.boxAns p → c.boxAns fun (w : W) => ¬p w

Negation preserves answerhood.

theorem Core.Mood.POSWQ.boxAns_and {W : Type u} (c : POSWQ W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w ∧ q w

Conjunction preserves answerhood.

theorem Core.Mood.POSWQ.boxAns_or {W : Type u} (c : POSWQ W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w ∨ q w

Disjunction preserves answerhood.

theorem Core.Mood.POSWQ.boxAns_imp {W : Type u} (c : POSWQ W) (p q : W → Prop) : c.boxAns p → c.boxAns q → c.boxAns fun (w : W) => p w → q w

Material implication preserves answerhood. Follows from the Boolean-algebra closure of constant-on-cell propositions.

§7. Three-component update disjointness

The three updates +, ⋆, ? touch disjoint POSWQ components, so they pairwise commute when lifted to act on POSWQ. The lifts are defined here because POSW.plus and POSW.star strip the inquiry field; POSWQ.plus and POSWQ.star are the inquiry-preserving counterparts.

def Core.Mood.POSWQ.plus {W : Type u} (c : POSWQ W) (p : W → Prop) : POSWQ W

POSWQ-side +-update: refine cs while preserving the inquiry partition. The inquiry-preserving lift of POSW.plus.

Equations

• c.plus p = { toPOSW := c.plus p, inquiry := c.inquiry }

def Core.Mood.POSWQ.star {W : Type u} (c : POSWQ W) (p : W → Prop) : POSWQ W

POSWQ-side ⋆-update: refine le while preserving the inquiry partition. The inquiry-preserving lift of POSW.star.

Equations

• c.star p = { toPOSW := c.star p, inquiry := c.inquiry }

@[simp]

theorem Core.Mood.POSWQ.plus_toPOSW {W : Type u} (c : POSWQ W) (p : W → Prop) : (c.plus p).toPOSW = c.plus p

@[simp]

theorem Core.Mood.POSWQ.plus_inquiry {W : Type u} (c : POSWQ W) (p : W → Prop) : (c.plus p).inquiry = c.inquiry

@[simp]

theorem Core.Mood.POSWQ.star_toPOSW {W : Type u} (c : POSWQ W) (p : W → Prop) : (c.star p).toPOSW = c.star p

@[simp]

theorem Core.Mood.POSWQ.star_inquiry {W : Type u} (c : POSWQ W) (p : W → Prop) : (c.star p).inquiry = c.inquiry

@[simp]

theorem Core.Mood.POSWQ.plus_star_comm {W : Type u} (c : POSWQ W) (p q : W → Prop) : (c.plus p).star q = (c.star q).plus p

+ and ⋆ commute on POSWQ: applying +-then-⋆ and ⋆-then-+ produces the same POSWQ. The components never interact.

@[simp]

theorem Core.Mood.POSWQ.plus_inquire_comm {W : Type u} (c : POSWQ W) (p : W → Prop) (s : Setoid W) : (c.plus p).inquire s = (c.inquire s).plus p

+ and ? commute on POSWQ: each touches a different component.

@[simp]

theorem Core.Mood.POSWQ.star_inquire_comm {W : Type u} (c : POSWQ W) (p : W → Prop) (s : Setoid W) : (c.star p).inquire s = (c.inquire s).star p

⋆ and ? commute on POSWQ: each touches a different component.

theorem Core.Mood.POSWQ.inquire_inquire_self {W : Type u} (c : POSWQ W) (s : Setoid W) : ((c.inquire s).inquire s).inquiry = (c.inquire s).inquiry

?-update is idempotent on the same partition: refining inquiry by s twice equals refining once. The Setoid-meet is idempotent in the CompleteLattice (Setoid W).

§8. Distinctness witness: boxAns ≠ boxCs ∘ projection

The third modal genuinely differs from boxCs. We exhibit a POSWQ where some p is settled by the question (boxAns p) but is not informationally necessary (¬ boxCs p). The witness is a non-trivial inquiry partition with two cells, where p is true on one cell and false on the other: it has a constant truth value per cell (so boxAns), but is not uniformly true on cs (so not boxCs).

def Core.Mood.POSWQ.sepPOSWQ : POSWQ Bool

Two-cell inquiry POSWQ: cs = ⊤ over Bool, le = ⊤, with inquiry the identity Setoid (each Bool in its own cell).

Equations

• One or more equations did not get rendered due to their size.

def Core.Mood.POSWQ.sepProp : Bool → Prop

Separation proposition: only false satisfies it.

Equations

• Core.Mood.POSWQ.sepProp w = (w = false)

theorem Core.Mood.POSWQ.boxAns_sepPOSWQ_sepProp : sepPOSWQ.boxAns sepProp

The separation proposition is settled by the question at sepPOSWQ: within each (singleton) cell, its truth value is constant.

theorem Core.Mood.POSWQ.not_boxCs_sepPOSWQ_sepProp : ¬sepPOSWQ.boxCs sepProp

The separation proposition is not informationally necessary at sepPOSWQ.toPOSW: true is in cs but does not satisfy p.

theorem Core.Mood.POSWQ.boxAns_not_reducible_to_boxCs : ∃ (c : POSWQ Bool) (p : Bool → Prop), c.boxAns p ∧ ¬c.boxCs p

boxAns and boxCs are not interderivable on the POSW substrate alone: there exists a POSWQ and a proposition where boxAns holds and boxCs fails. The inquiry component is doing genuine work.