Question — core type, lattice, Heyting derivatives

[CGR18] [Cia22] [Pun16] [Pun19] [TRA18]

A bundled Question W — a non-empty downward-closed family of information states over W (where an information state is a subset of W). This is mathematically a non-empty LowerSet (Set W); in linguistic terms it is the umbrella structure for question-flavored content: it subsumes Hamblin alternative sets (polar, which), partition-style questions (via Semantics/Mood/PartitionAsInquiry.lean), and the inquisitive propositions of [CGR18]. The name "Question" follows the decision-theoretic / discourse-semantic tradition (van Rooij, Westera) — neutral as to whether the consumer is doing inquisitive theorizing.

This Basic file carries the structural core: the type definition with its SetLike instance, the info/alt/isInformative/isInquisitive/ isDeclarative predicates, the declarative constructor, the algebraic operations (conj, inqDisj, top, bot) packaged into the CompleteDistribLattice instance, the basic info-on-lattice-operations API, the alt-as-maximal characterization, the existence of alternatives under finiteness, the Resolutions Theorem (DNF), the principal-ideal characterization of declaratives, the Heyting derivatives (compl_eq, proj, nonInfo, the division law), and the LEM-fails witness.

For Hamblin constructions (polar, which), see Core/Question/Hamblin.lean. For partial-answerhood and Roberts QUD-relevance predicates, see Core/Question/Relevance.lean. For the Setoid → Question embedding (used by POSWQ), see Semantics/Mood/PartitionAsInquiry.lean.

Mathlib alignment

• props : Set (Set W) — sets of subsets of W, mathlib-native
• contains_empty is logically equivalent to Nonempty props together with downward closure — we expose it as the field directly because it's the only constraint that matters once downward closure holds
• info returns Set W (mathlib-native), not W → Bool
• SetLike (Question W) (Set W) — auto-derives Membership, CoeSort, and the ext machinery. mem_props is the canonical simp normalization (q ∈ P.props → q ∈ P).
• CompleteDistribLattice (Question W) — registered via CompleteDistribLattice.ofMinimalAxioms from two pointwise inequalities, giving Frame, Coframe, HeytingAlgebra, and BiheytingAlgebra for free. Mirrors Filter's registration pattern.

Why a bundled structure rather than LowerSet (Set W)?

A downward-closed family of propositions on W is, abstractly, a LowerSet (Set W). We considered registering Question as a LowerSet synonym, but rejected it because the ⊥ elements disagree: LowerSet.⊥ = ∅ (no resolving propositions), while ours is {∅} (only the inconsistent state resolves). The non-emptiness constraint (contains_empty) is essential to inquisitive semantics and is lost in LowerSet. We use SetLike instead, which gives the membership/coercion API without forcing LowerSet's ⊥.

structure Question (W : Type u) : Type u

An inquisitive proposition in the sense of [CGR18]: a non-empty downward-closed family of information states over W. The states in props are the ones that resolve the issue raised by the sentence.

• props : Set (Set W)

  The set of propositions resolving the issue.

• contains_empty : ∅ ∈ self.props

  Contains the empty proposition (= the inconsistent information state). Equivalent to non-emptiness given downward closure.

• downward_closed (p : Set W) : p ∈ self.props → ∀ q ⊆ p, q ∈ self.props

  Downward closed: if p resolves the issue and q ⊆ p, then q also resolves it (any sufficient evidence is also sufficient when strengthened).

@[implicit_reducible]

instance Question.instSetLikeSet {W : Type u} : SetLike (Question W) (Set W)

SetLike instance: an Question W coerces to its underlying Set (Set W) of resolving propositions. Auto-derives Membership (q ∈ P means q ∈ P.props), CoeSort, and the standard ext machinery. Mirrors mathlib's pattern for Submonoid, Subgroup, LowerSet, etc.

Equations

• Question.instSetLikeSet = { coe := Question.props, coe_injective := ⋯ }

@[simp]

theorem Question.mem_props {W : Type u} {P : Question W} {q : Set W} : q ∈ P.props ↔ q ∈ P

Membership normalization: q ∈ P.props rewrites to q ∈ P. Mirrors mathlib's mem_carrier pattern (SetLike.Basic line 92).

@[simp]

theorem Question.coe_mk {W : Type u} (s : Set (Set W)) (h₁ : ∅ ∈ s) (h₂ : ∀ p ∈ s, ∀ q ⊆ p, q ∈ s) : ↑{ props := s, contains_empty := h₁, downward_closed := h₂ } = s

theorem Question.ext {W : Type u} {P Q : Question W} (h : ∀ (q : Set W), q ∈ P ↔ q ∈ Q) : P = Q

Two Questions are equal when their props agree.

theorem Question.ext_iff {W : Type u} {P Q : Question W} : P = Q ↔ ∀ (q : Set W), q ∈ P ↔ q ∈ Q

def Question.alt {W : Type u} (P : Question W) : Set (Set W)

The alternatives of an inquisitive content ([CGR18]): the maximal propositions in props. These are the "answers" — the strongest information states that resolve the issue.

Equations

• P.alt = {p : Set W | p ∈ P.props ∧ ∀ q ∈ P.props, p ⊆ q → p = q}

def Question.info {W : Type u} (P : Question W) : Set W

The informative content of an inquisitive content ([CGR18]): the union of all propositions in props. The information any utterance with this meaning provides — the actual world must lie in info P.

Equations

• P.info = ⋃₀ P.props

def Question.isInformative {W : Type u} (P : Question W) : Prop

A sentence is informative iff its informative content excludes at least one possible world.

Equations

• P.isInformative = (P.info ≠ Set.univ)

def Question.isInquisitive {W : Type u} (P : Question W) : Prop

A sentence is inquisitive iff resolving the issue it raises requires more than the information it provides — equivalently, iff info P itself is not in props (so no single proposition in props covers all of info P).

Equations

• P.isInquisitive = (P.info ∉ P.props)

def Question.isDeclarative {W : Type u} (P : Question W) : Prop

A sentence is declarative iff it is not inquisitive — equivalently, iff info P ∈ props. Algebraic characterization ([Pun19]): props is a principal ideal in the algebra of information states; see isDeclarative_iff_eq_declarative_info.

Equations

• P.isDeclarative = (P.info ∈ P.props)

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

Declarative and inquisitive are exact negations of each other.

Constructors

def Question.ofLowerSet {W : Type u} (s : Set (Set W)) (empty_mem : ∅ ∈ s) (lower : IsLowerSet s) : Question W

Smart constructor from a lower (downward-closed) family of information states containing ∅. Packages the two Question obligations in mathlib's IsLowerSet vocabulary, so a caller holding a persistence proof (IsLowerSet) and an empty-state witness builds the Question directly instead of re-deriving downward_closed inline.

Equations

• Question.ofLowerSet s empty_mem lower = { props := s, contains_empty := empty_mem, downward_closed := ⋯ }

@[simp]

theorem Question.props_ofLowerSet {W : Type u} (s : Set (Set W)) (empty_mem : ∅ ∈ s) (lower : IsLowerSet s) : (ofLowerSet s empty_mem lower).props = s

@[simp]

theorem Question.mem_ofLowerSet {W : Type u} {s : Set (Set W)} {empty_mem : ∅ ∈ s} {lower : IsLowerSet s} {q : Set W} : q ∈ ofLowerSet s empty_mem lower ↔ q ∈ s

def Question.declarative {W : Type u} (p : Set W) : Question W

The declarative content of a proposition p: the principal ideal {q | q ⊆ p}. Single alternative p; non-inquisitive; informative iff p ≠ univ.

Equations

• Question.declarative p = { props := {q : Set W | q ⊆ p}, contains_empty := ⋯, downward_closed := ⋯ }

Basic theorems on declarative

@[simp]

theorem Question.mem_declarative {W : Type u} {p q : Set W} : q ∈ declarative p ↔ q ⊆ p

@[simp]

theorem Question.info_declarative {W : Type u} (p : Set W) : (declarative p).info = p

theorem Question.isDeclarative_declarative {W : Type u} (p : Set W) : (declarative p).isDeclarative

theorem Question.not_isInquisitive_declarative {W : Type u} (p : Set W) : ¬(declarative p).isInquisitive

Algebraic operations ([Pun19] §2)

Following the support-clause definitions in [Pun19] §2: conjunction is ||α ∧ β|| = ||α|| ∩ ||β|| (state supports α ∧ β iff it supports both); inquisitive disjunction is ||α ⩒ β|| = ||α|| ∪ ||β|| (state supports α ⩒ β iff it supports either).

Implication → and negation ¬ arise as the Heyting ⇨ and ᶜ of the CompleteDistribLattice structure registered below; see the "Heyting derivatives" section for the structural identity Pᶜ = declarative (info P)ᶜ and the derivatives it grounds.

def Question.conj {W : Type u} (P Q : Question W) : Question W

Inquisitive conjunction P ∧ Q ([Pun19] §2 ∧ clause): props is the pointwise intersection. A state resolves P ∧ Q iff it resolves both P and Q.

Equations

• P.conj Q = { props := P.props ∩ Q.props, contains_empty := ⋯, downward_closed := ⋯ }

def Question.inqDisj {W : Type u} (P Q : Question W) : Question W

Inquisitive disjunction P ⩒ Q ([Pun19] §2 ⩒ clause): props is the pointwise union. A state resolves P ⩒ Q iff it resolves P or Q. Distinct from classical disjunction ∨, whose support clause involves splitting the state across two substates.

Equations

• P.inqDisj Q = { props := P.props ∪ Q.props, contains_empty := ⋯, downward_closed := ⋯ }

def Question.top {W : Type u} : Question W

The top inquisitive content: every set of worlds resolves the issue. The trivial inquiry that demands nothing.

Equations

• Question.top = { props := Set.univ, contains_empty := ⋯, downward_closed := ⋯ }

def Question.bot {W : Type u} : Question W

The bottom inquisitive content: only the inconsistent state (∅) resolves the issue. The unsatisfiable inquiry.

Equations

• Question.bot = { props := {∅}, contains_empty := ⋯, downward_closed := ⋯ }

Complete lattice structure

We package the algebraic operations into mathlib's order/lattice typeclasses: the entailment order P ≤ Q := P.props ⊆ Q.props makes Question W into a bounded distributive complete lattice with ⊓ = conj, ⊔ = inqDisj, ⊥ = bot, ⊤ = top, plus arbitrary suprema and infima.

sSup S is the union of all props fields (with ∅ adjoined so contains_empty holds vacuously when S = ∅); sInf S is the intersection (= univ, vacuously, when S = ∅, which gives ⊤). This gives access to the entire mathlib order/lattice API (inf_le_left, le_sup_right, inf_sup_right, iSup, iInf, sSup_le_iff, intervals, lattice homomorphisms, …).

Distributivity (binary) is free: it reduces to the standard set distributivity on the underlying Set (Set W), and falls out of the CompleteDistribLattice registration below (no separate DistribLattice instance needed).

def Question.sSupContent {W : Type u} (S : Set (Question W)) : Question W

The arbitrary supremum: a state resolves sSup S iff it resolves some P ∈ S (or is the empty state, which always resolves).

Equations

• Question.sSupContent S = { props := {q : Set W | q = ∅ ∨ ∃ P ∈ S, q ∈ P.props}, contains_empty := ⋯, downward_closed := ⋯ }

def Question.sInfContent {W : Type u} (S : Set (Question W)) : Question W

The arbitrary infimum: a state resolves sInf S iff it resolves every P ∈ S. (When S = ∅, this is Set.univ, recovering ⊤.)

Equations

• Question.sInfContent S = { props := {q : Set W | ∀ P ∈ S, q ∈ P.props}, contains_empty := ⋯, downward_closed := ⋯ }

@[implicit_reducible]

instance Question.instSupSet {W : Type u} : SupSet (Question W)

Equations

• Question.instSupSet = { sSup := Question.sSupContent }

@[implicit_reducible]

instance Question.instInfSet {W : Type u} : InfSet (Question W)

Equations

• Question.instInfSet = { sInf := Question.sInfContent }

@[implicit_reducible]

instance Question.instCompleteLattice {W : Type u} : CompleteLattice (Question W)

The complete lattice structure on Question W. Provides Lattice, BoundedOrder, SupSet, InfSet, plus iSup/iInf for the entire mathlib API.

Equations

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

Distributivity

Question W is a complete distributive lattice (in mathlib's sense: both a Frame and a Coframe). This subsumes finite distributivity, gives a HeytingAlgebra (and BiheytingAlgebra) structure for free, and follows from a single fact about the underlying Set (Set W): pointwise ∩ distributes over arbitrary ∪, and pointwise ∪ distributes over arbitrary ∩.

We register it via CompleteDistribLattice.ofMinimalAxioms, which needs only the two inequalities inf_sSup ≤ iSup_inf and iInf_sup ≤ sup_sInf.

@[implicit_reducible]

instance Question.instCompleteDistribLattice {W : Type u} : CompleteDistribLattice (Question W)

The CompleteDistribLattice structure: ⊓ distributes over ⨆ and ⊔ distributes over ⨅. Subsumes binary distributivity and auto-provides HeytingAlgebra, CoheytingAlgebra, and BiheytingAlgebra instances via ofMinimalAxioms.

Equations

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

theorem Question.le_def {W : Type u} {P Q : Question W} : P ≤ Q ↔ P.props ⊆ Q.props

theorem Question.inf_eq_conj {W : Type u} (P Q : Question W) : P ⊓ Q = P.conj Q

theorem Question.sup_eq_inqDisj {W : Type u} (P Q : Question W) : P ⊔ Q = P.inqDisj Q

theorem Question.sSup_eq {W : Type u} (S : Set (Question W)) : sSup S = sSupContent S

theorem Question.sInf_eq {W : Type u} (S : Set (Question W)) : sInf S = sInfContent S

theorem Question.top_eq {W : Type u} : ⊤ = top

theorem Question.bot_eq {W : Type u} : ⊥ = bot

@[simp]

theorem Question.mem_inf {W : Type u} {P Q : Question W} {q : Set W} : q ∈ P ⊓ Q ↔ q ∈ P ∧ q ∈ Q

@[simp]

theorem Question.mem_sup {W : Type u} {P Q : Question W} {q : Set W} : q ∈ P ⊔ Q ↔ q ∈ P ∨ q ∈ Q

@[simp]

theorem Question.mem_bot {W : Type u} {q : Set W} : q ∈ ⊥ ↔ q = ∅

@[simp]

theorem Question.mem_top {W : Type u} {q : Set W} : q ∈ ⊤

theorem Question.mem_iff_declarative_le {W : Type u} {X : Question W} {s : Set W} : s ∈ X ↔ declarative s ≤ X

A state lies in X iff its principal ideal entails X: declarative s is the smallest Question containing s.

theorem Question.mem_himp {W : Type u} {P Q : Question W} {s : Set W} : s ∈ P ⇨ Q ↔ ∀ r ⊆ s, r ∈ P → r ∈ Q

Heyting implication, pointwise: s resolves P ⇨ Q iff every substate of s that resolves P also resolves Q. The defining property of the Heyting arrow on inquisitive contents.

@[simp]

theorem Question.mem_sSup_props {W : Type u} {S : Set (Question W)} {q : Set W} : q ∈ (sSup S).props ↔ q = ∅ ∨ ∃ P ∈ S, q ∈ P.props

@[simp]

theorem Question.mem_sInf_props {W : Type u} {S : Set (Question W)} {q : Set W} : q ∈ (sInf S).props ↔ ∀ P ∈ S, q ∈ P.props

theorem Question.mem_iSup_iff {W : Type u} {ι : Sort u_1} {f : ι → Question W} {q : Set W} : q ∈ ⨆ (i : ι), f i ↔ q = ∅ ∨ ∃ (i : ι), q ∈ f i

Membership in an indexed iSup of inquisitive contents. The q = ∅ disjunct is structural: ∅ lies in every content's props.

theorem Question.mem_biSup_iff {W : Type u} {ι : Type u_1} {I : Set ι} {f : ι → Question W} {q : Set W} : q ∈ ⨆ i ∈ I, f i ↔ q = ∅ ∨ ∃ i ∈ I, q ∈ f i

Membership in a bounded indexed iSup. Used pervasively for Hamblin-style wh-question alternatives (which) and for any ⨆ i ∈ I, declarative (P i) construction.

@[implicit_reducible]

instance Question.instInhabited {W : Type u} : Inhabited (Question W)

Equations

• Question.instInhabited = { default := ⊤ }

Basic API for info on the lattice operations

info is a monotone map from (Question W, ≤) to (Set W, ⊆) and commutes with ⊔ (and ⊥/⊤). The story for ⊓ is one-sided: info distributes over union but only sub-distributes over intersection (the same asymmetry as ⋃₀ over Set operations).

theorem Question.info_mono {W : Type u} {P Q : Question W} (h : P ≤ Q) : P.info ⊆ Q.info

info is monotone in the entailment order: a stronger inquiry has no more informative content than a weaker one.

@[simp]

theorem Question.info_top {W : Type u} : ⊤.info = Set.univ

@[simp]

theorem Question.info_bot {W : Type u} : ⊥.info = ∅

@[simp]

theorem Question.info_sup {W : Type u} (P Q : Question W) : (P ⊔ Q).info = P.info ∪ Q.info

theorem Question.info_inf_subset {W : Type u} (P Q : Question W) : (P ⊓ Q).info ⊆ P.info ∩ Q.info

alt API and inquisitivity from alternatives

The alt (alternatives) selector picks out maximal propositions in P.props. Two basic facts: alternatives are propositions, and the union of alternatives is contained in info P (equality requires finite-W or other guarantees that maximals exist — [CGR18] discusses the limit case where no maximal element exists). The two-alternatives criterion gives a sufficient condition for inquisitivity that does not depend on finiteness.

theorem Question.mem_alt {W : Type u} {P : Question W} {p : Set W} : p ∈ P.alt ↔ p ∈ P.props ∧ ∀ q ∈ P.props, p ⊆ q → p = q

Unfolded membership in alt. Not the simp normal form — mem_alt_iff_maximal is preferred because it connects to mathlib's Maximal API. Use this lemma when destructuring is more convenient than going through Maximal.

theorem Question.alt_subset_props {W : Type u} (P : Question W) : P.alt ⊆ P.props

theorem Question.sUnion_alt_subset_info {W : Type u} (P : Question W) : ⋃₀ P.alt ⊆ P.info

@[simp]

theorem Question.mem_alt_iff_maximal {W : Type u} {P : Question W} {p : Set W} : p ∈ P.alt ↔ Maximal (fun (x : Set W) => x ∈ P.props) p

Simp normal form for alternatives: the alternatives of alt P are exactly the Maximal elements of P.props under the subset order. Bridges the linguistic alt-definition to mathlib's order-theoretic Maximal, so that mathlib's Maximal API (maximal_iff, Maximal.eq_of_ge, etc.) applies directly to inquisitive alternatives.

theorem Question.mem_alt_inf_iff {W : Type u} {P Q : Question W} {q : Set W} : q ∈ (P ⊓ Q).alt ↔ Maximal (fun (p : Set W) => p ∈ P.props ∧ p ∈ Q.props) q

Membership in alt (P ⊓ Q): the alternatives of the inquisitive conjunction are exactly the maximal elements of P.props ∩ Q.props. Direct corollary of mem_alt_iff_maximal and the pointwise definition of ⊓ on props.

theorem Question.mem_alt_sup_iff {W : Type u} {P Q : Question W} {q : Set W} : q ∈ (P ⊔ Q).alt ↔ Maximal (fun (p : Set W) => p ∈ P.props ∨ p ∈ Q.props) q

Membership in alt (P ⊔ Q): the alternatives of the inquisitive disjunction are exactly the maximal elements of P.props ∪ Q.props. Direct corollary of mem_alt_iff_maximal and the pointwise definition of ⊔ on props. The asymmetry with inf: inf's alts are sub-states satisfying both, sup's alts are super-states maximal across either.

theorem Question.mem_alt_sup_of_alt_left {W : Type u} {P Q : Question W} {p : Set W} (hP : p ∈ P.alt) (hQ : ∀ q ∈ Q.props, p ⊆ q → p = q) : p ∈ (P ⊔ Q).alt

An alt of P that is not contained in any strictly larger alt of Q survives in alt (P ⊔ Q). The convenient direction for constructing alts of an inquisitive disjunction.

theorem Question.mem_alt_sup_of_alt_right {W : Type u} {P Q : Question W} {q : Set W} (hQ : q ∈ Q.alt) (hP : ∀ p ∈ P.props, q ⊆ p → q = p) : q ∈ (P ⊔ Q).alt

An alt of Q that is not contained in any strictly larger alt of P survives in alt (P ⊔ Q). Mirror of mem_alt_sup_of_alt_left.

theorem Question.alt_sup_subset_union {W : Type u} (P Q : Question W) : (P ⊔ Q).alt ⊆ P.alt ∪ Q.alt

An alt of P ⊔ Q is necessarily an alt of one of the summands — when restricted to that summand's props.

@[simp]

theorem Question.declarative_inf {W : Type u} (A B : Set W) : declarative A ⊓ declarative B = declarative (A ∩ B)

The meet of two declaratives is the declarative of the intersection: ↓{A} ⊓ ↓{B} = ↓{A ∩ B}. State q resolves both declarative A and declarative B iff q ⊆ A ∩ B. Direct corollary of Set.subset_inter_iff.

@[simp]

theorem Question.alt_declarative {W : Type u} (p : Set W) : (declarative p).alt = {p}

A declarative p content has exactly one alternative — p itself, the unique maximal subset of p.

@[simp]

theorem Question.alt_top {W : Type u} : ⊤.alt = {Set.univ}

The unique alternative of ⊤ is Set.univ.

@[simp]

theorem Question.alt_bot {W : Type u} : ⊥.alt = {∅}

The unique alternative of ⊥ is ∅.

theorem Question.isInquisitive_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.isInquisitive

If P has two distinct alternatives, then P is inquisitive: no single proposition (in particular, not info P) can equal both.

Existence of alternatives under finiteness

When W is finite, P.props ⊆ Set W is finite, so every proposition extends to a maximal one. This gives the dual half of sUnion_alt_subset_info: info P ⊆ ⋃₀ alt P, hence equality.

Without finiteness, alternatives need not exist — a downward-closed family with no maximal element (e.g. {q ⊊ Set.univ | q.Finite} on infinite W) is a valid Question with alt P = ∅ even though info P ≠ ∅.

theorem Question.exists_alt_above {W : Type u} (P : Question W) (hP : P.props.Finite) {p : Set W} (hp : p ∈ P.props) : ∃ q ∈ P.alt, p ⊆ q

Existence of alternatives under finiteness: every proposition in P.props extends to a maximal one (i.e., to an alternative).

Hypothesis is the minimal one: P.props.Finite (not Finite W). The latter implies the former (since Set.instFinite gives Finite (Set W) and P.props ⊆ Set W), but P.props.Finite can hold even on infinite worlds (e.g., a content with finitely many alternatives over an infinite world space).

theorem Question.info_eq_sUnion_alt {W : Type u} (P : Question W) (hP : P.props.Finite) : P.info = ⋃₀ P.alt

Under finiteness of P.props, info P is exactly the union of alternatives: every world in some resolving proposition lies in some maximal resolving proposition.

The Resolutions Theorem (DNF for inquisitive content)

The deepest theorem about Question: under finiteness, every inquisitive content equals the inquisitive disjunction of the declaratives generated by its alternatives. This is the inquisitive-semantics analogue of disjunctive normal form, justifying the slogan "an inquisitive content is its alternatives" — once alternatives exist (finiteness), they fully determine the content.

This subsumes:

• Single-alternative case: P = declarative p iff alt P = {p} (the principal-ideal characterization for declaratives).
• The polar case: polar p = declarative p ⊔ declarative pᶜ (in Hamblin.lean) is literally ⨆ q ∈ {p, pᶜ}, declarative q.
• Setoid-derived inquiries: fromSetoid r resolves to the iSup over equivalence classes (each class is an alternative).

Without finiteness the theorem fails (alternatives may not exist), but the inequality ⨆ p ∈ alt P, declarative p ≤ P holds always.

theorem Question.iSup_declarative_alt_le {W : Type u} (P : Question W) : ⨆ p ∈ P.alt, declarative p ≤ P

The lower bound (always holds): the inquisitive disjunction of the declarative principal ideals of P's alternatives is contained in P itself.

theorem Question.eq_iSup_declarative_alt_of_exists_alt {W : Type u} (P : Question W) (hExt : ∀ p ∈ P.props, ∃ q ∈ P.alt, p ⊆ q) : P = ⨆ p ∈ P.alt, declarative p

Resolutions Theorem under "alternatives-cover" hypothesis: when every resolving proposition extends to an alternative, P equals the inquisitive disjunction of the declaratives generated by its alternatives. The hypothesis hExt is strictly weaker than P.props.Finite: atoms have props = {q | q ⊆ V} (potentially infinite if V infinite) but alt = {V}, so hExt discharges by q ⊆ V → q ⊆ V while finiteness fails.

This is Booth 2022's Compactness of Alternatives for atomic and decomposable bilateral inquisitive propositions, captured at the Question substrate level.

theorem Question.eq_iSup_declarative_alt {W : Type u} (P : Question W) (hP : P.props.Finite) : P = ⨆ p ∈ P.alt, declarative p

Resolutions Theorem: under finiteness of P.props, every inquisitive content is the inquisitive disjunction of the declaratives generated by its alternatives. Corollary of the "alternatives-cover" version: finiteness gives existence of a maximal extension via exists_alt_above.

Principal-ideal characterization of declaratives

[Pun19]: declarative propositions are, algebraically speaking, principal ideals in the algebra of information states. We make this characterization explicit: P is declarative iff P is the principal ideal generated by info P. We also prove the equivalent characterization via alternatives: P is declarative iff alt P = {info P}.

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

Principal-ideal characterization ([Pun19]): an inquisitive content is declarative iff it equals the principal ideal generated by its informative content.

theorem Question.isDeclarative_iff_alt_eq_singleton {W : Type u} (P : Question W) : P.isDeclarative ↔ P.alt = {P.info}

Alternative-set characterization: an inquisitive content is declarative iff its alternatives are exactly {info P} — i.e., iff its informative content is itself the unique maximal resolving state.

Heyting derivatives: complement, projection, division law

The CompleteDistribLattice structure registered above gives us a HeytingAlgebra for free, so Pᶜ (pseudo-complement) and P ⇨ Q (Heyting implication) come pre-installed with their universal properties. The structural fact that drives the inquisitive-specific theory is the explicit formula for Pᶜ:

`Pᶜ = declarative (info P)ᶜ`

i.e., complementing P is the same as complementing its informative content and taking the principal ideal. This single identity (compl_eq) lets us derive the standard inquisitive operators ([CGR18]; [Pun19]):

• the non-inquisitive projection !P = Pᶜᶜ = declarative (info P) (proj_eq_compl_compl),
• the non-informative projection ?P = P ⊔ Pᶜ,
• and the division law !P ⊓ ?P = P decomposing every content into its informative and inquisitive components (proj_inf_nonInfo).

The lattice is Heyting but not Boolean: LEM P ⊔ Pᶜ = ⊤ fails in general — see not_lem_inquisitive_content below.

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

Pseudo-complement formula: the Heyting complement Pᶜ is the declarative principal ideal of the complemented informative content. This is the structural identity that grounds all subsequent Heyting derivatives.

@[simp]

theorem Question.info_compl {W : Type u} (P : Question W) : Pᶜ.info = P.infoᶜ

info commutes with complement: even though the lattice of contents is only Heyting, the underlying informative content is a Boolean Set, and info respects complementation.

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

Non-inquisitive projection !P: the declarative content with the same informative content as P ([CGR18]). Removes any inquisitivity by collapsing all alternatives into a single principal ideal. Always declarative; equal to P iff P is declarative.

Used to define classical (non-inquisitive) operators in inquisitive semantics: classical disjunction is !(P ⩒ Q) = !P ⊔ !Q, etc.

Equations

• P.proj = Question.declarative P.info

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

!P = Pᶜᶜ: the non-inquisitive projection coincides with the Heyting double-complement ([CGR18]). Together with compl_eq, this means every inquisitive operator derivable from the Heyting structure is, at the level of info, a Boolean operator on Set W.

@[simp]

theorem Question.info_proj {W : Type u} (P : Question W) : P.proj.info = P.info

theorem Question.isDeclarative_proj {W : Type u} (P : Question W) : P.proj.isDeclarative

@[simp]

theorem Question.proj_proj {W : Type u} (P : Question W) : P.proj.proj = P.proj

proj is idempotent: projecting twice = projecting once.

theorem Question.proj_eq_self_iff {W : Type u} (P : Question W) : P.proj = P ↔ P.isDeclarative

Projection fixes declarative contents (!P = P iff P is declarative).

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

Non-informative projection ?P := P ⊔ Pᶜ ([CGR18]). The "inquisitive question" operator: takes any content and returns its non-informative counterpart with the same inquisitive structure.

Equations

• P.nonInfo = P ⊔ Pᶜ

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

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

Division law ([CGR18]): every inquisitive content decomposes uniquely as the meet of its non-inquisitive projection and its non-informative projection. This is the fundamental decomposition theorem of inquisitive semantics — it says the lattice "factors through" (info, alternatives).

LEM fails: the lattice is Heyting but not Boolean

A central feature of inquisitive semantics is that the standard logical laws of a Boolean algebra do not all hold. In particular, the law of excluded middle P ⊔ Pᶜ = ⊤ fails: an inquisitive content P and its pseudo-complement Pᶜ are both declarative, so their join is declarative too, while ⊤ is the trivially-resolved content (every state in props). The witness below uses the polar-question shape declarative {true} ⊔ declarative {true}ᶜ over Bool.

theorem Question.not_lem_inquisitive_content : ∃ (W : Type) (P : Question W), P ⊔ Pᶜ ≠ ⊤

LEM fails for inquisitive content: there exists W and P with P ⊔ Pᶜ ≠ ⊤. This is what makes the lattice Heyting rather than Boolean.

The Truth-Support Bridge: the declarative embedding

The classical algebra of propositions embeds into the inquisitive algebra via declarative — [Cia22]'s Truth-Support Bridge, by which a statement names the singleton-generated information type ↓{|α|} (§2.4.2, p. 21). The embedding is order-faithful (declarativeEmbedding) and preserves meets and ⊤ (declarativeHom : InfTopHom), but not joins: the join of two declaratives can be genuinely inquisitive (exists_isInquisitive_declarative_sup) — inquisitive content enters the algebra exactly at ⊔. The classical context-set picture of Discourse/CommonGround.lean (its scoped meet monoid and CommonGround.HasAssertion) is the declarative fragment of the inquisitive one along this embedding.

@[simp]

theorem Question.declarative_top {W : Type u} : declarative Set.univ = ⊤

theorem Question.declarative_le_declarative_iff {W : Type u} {A B : Set W} : declarative A ≤ declarative B ↔ A ⊆ B

theorem Question.declarative_injective {W : Type u} : Function.Injective declarative

def Question.declarativeEmbedding {W : Type u} : Set W ↪o Question W

declarative as an order embedding: the classical algebra of propositions sits order-faithfully inside the inquisitive algebra.

Equations

• Question.declarativeEmbedding = { toFun := Question.declarative, inj' := ⋯, map_rel_iff' := ⋯ }

def Question.declarativeHom {W : Type u} : InfTopHom (Set W) (Question W)

The Truth-Support Bridge, bundled: declarative preserves meets and ⊤. Deliberately not a lattice hom — see exists_declarative_sup_ne.

Equations

• Question.declarativeHom = { toFun := Question.declarative, map_inf' := ⋯, map_top' := ⋯ }

theorem Question.exists_isInquisitive_declarative_sup : ∃ (A : Set Bool) (B : Set Bool), (declarative A ⊔ declarative B).isInquisitive

Joins are where inquisitiveness enters: over Bool, the join of the declaratives ↓{{true}} and ↓{{false}} is the polar question "which truth value?" — its own informative content (univ) does not resolve it.

theorem Question.exists_declarative_sup_ne : ∃ (A : Set Bool) (B : Set Bool), declarative A ⊔ declarative B ≠ declarative (A ∪ B)

The Truth-Support Bridge does not commute with ⊔: declarative is an InfTopHom but not a lattice hom.

Question.Support instance

The cross-tradition s ⊨ Q interface (Question.Support) is satisfied by Question in the standard inquisitive way: an information state s : Set W supports / resolves the issue P iff s is one of the resolving propositions (s ∈ P.props). This is the inquisitive notion of support ([CGR18]).

@[implicit_reducible]

instance Question.instSupport {W : Type u} : Support (Set W) (Question W)

Inquisitive support: s ⊨ P iff the state s resolves the issue P.

Equations

• Question.instSupport = { supports := fun (s : Set W) (P : Question W) => s ∈ P }

theorem Question.supports_iff {W : Type u} (s : Set W) (P : Question W) : Support.supports s P ↔ s ∈ P