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/Questions/Partition/Basic.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 predicates, the ofSet 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 Semantics/Questions/Hamblin.lean. For answerhood predicates, see Semantics/Questions/Resolution.lean; for question entailment, Semantics/Questions/Entailment.lean. For the Setoid → Question embedding (used by State), see Semantics/Questions/Partition/Basic.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).

@[instance_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}

theorem Question.mem_of_mem_alt {W : Type u} {P : Question W} {p : Set W} (h : p ∈ P.alt) : p ∈ P

An alternative is in particular a resolving state.

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)

theorem Question.info_mem_iff_not_isInquisitive {W : Type u} (P : Question W) : P.info ∈ P ↔ ¬P.isInquisitive

A content's own informative content resolves it iff it is not inquisitive — the condition declarative sentences satisfy; props is then a principal ideal ([Pun19]), see info_mem_iff_eq_ofSet_info.

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.ofSet {W : Type u} (p : Set W) : Question W

The content with the single alternative p: the principal ideal {q | q ⊆ p}, analogue of Filter.principal. Non-inquisitive — what a declarative sentence expresses; informative iff p ≠ univ.

Equations

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

Basic theorems on ofSet

@[simp]

theorem Question.mem_ofSet {W : Type u} {p q : Set W} : q ∈ ofSet p ↔ q ⊆ p

@[simp]

theorem Question.info_ofSet {W : Type u} (p : Set W) : (ofSet p).info = p

theorem Question.info_mem_ofSet {W : Type u} (p : Set W) : (ofSet p).info ∈ ofSet p

theorem Question.not_isInquisitive_ofSet {W : Type u} (p : Set W) : ¬(ofSet 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ᶜ = ofSet (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 := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_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.

@[instance_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

• Question.instCompleteDistribLattice = CompleteDistribLattice.ofMinimalAxioms ⋯

instance Question.instIsConcreteLESet {W : Type u} : IsConcreteLE (Question W) (Set W)

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_ofSet_le {W : Type u} {X : Question W} {s : Set W} : s ∈ X ↔ ofSet s ≤ X

A state lies in X iff its principal ideal entails X: ofSet 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 {W : Type u} {S : Set (Question W)} {q : Set W} : q ∈ sSup S ↔ q = ∅ ∨ ∃ P ∈ S, q ∈ P

@[simp]

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

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, ofSet (P i) construction.

@[instance_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

The info ⊣ ofSet adjunction

theorem Question.gc_info_ofSet {W : Type u} : GaloisConnection info ofSet

info is left adjoint to ofSet: a content's information lies inside p iff the content entails the principal content of p.

def Question.gi_info_ofSet {W : Type u} : GaloisInsertion info ofSet

The adjunction is an insertion: info (ofSet p) = p.

Equations

• Question.gi_info_ofSet = ⋯.toGaloisInsertion ⋯

theorem Question.info_iSup {W : Type u} {ι : Sort u_1} (f : ι → Question W) : (⨆ (i : ι), f i).info = ⋃ (i : ι), (f i).info

info turns joins into unions.

theorem Question.ofSet_iInf {W : Type u} {ι : Sort u_1} (p : ι → Set W) : ofSet (⋂ (i : ι), p i) = ⨅ (i : ι), ofSet (p i)

ofSet turns intersections into meets.

def Question.projClosure {W : Type u} : ClosureOperator (Question W)

The non-inquisitive projection proj = ofSet ∘ info as a closure operator.

Equations

• Question.projClosure = ⋯.closureOperator

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_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.ofSet_inf {W : Type u} (A B : Set W) : ofSet A ⊓ ofSet B = ofSet (A ∩ B)

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

@[simp]

theorem Question.alt_ofSet {W : Type u} (p : Set W) : (ofSet p).alt = {p}

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

theorem Question.self_mem_alt_ofSet {W : Type u} (p : Set W) : p ∈ (ofSet p).alt

p is the alternative of the content it generates.

@[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 = ofSet p iff alt P = {p} (the principal-ideal characterization for declaratives).
• The polar case: polar p = ofSet p ⊔ ofSet pᶜ (in Hamblin.lean) is literally ⨆ q ∈ {p, pᶜ}, ofSet 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, ofSet p ≤ P holds always.

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

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

theorem Question.eq_iSup_ofSet_alt_of_exists_alt {W : Type u} (P : Question W) (hExt : ∀ p ∈ P.props, ∃ q ∈ P.alt, p ⊆ q) : P = ⨆ p ∈ P.alt, ofSet 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_ofSet_alt {W : Type u} (P : Question W) (hP : P.props.Finite) : P = ⨆ p ∈ P.alt, ofSet 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]: ofSet 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.info_mem_iff_eq_ofSet_info {W : Type u} (P : Question W) : P.info ∈ P ↔ P = ofSet P.info

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

theorem Question.info_mem_iff_alt_eq_singleton {W : Type u} (P : Question W) : P.info ∈ P ↔ 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ᶜ = ofSet (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ᶜᶜ = ofSet (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ᶜ = ofSet P.infoᶜ

Pseudo-complement formula: the Heyting complement Pᶜ is the ofSet 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.ofSet 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.info_mem_proj {W : Type u} (P : Question W) : P.proj.info ∈ P.proj

@[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.info ∈ P

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 ofSet {true} ⊔ ofSet {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 ofSet — [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 (ofSetEmbedding) and preserves meets and ⊤ (ofSetHom : InfTopHom), but not joins: the join of two declaratives can be genuinely inquisitive (exists_isInquisitive_ofSet_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.ofSet_univ {W : Type u} : ofSet Set.univ = ⊤

theorem Question.ofSet_empty {W : Type u} : ofSet ∅ = ⊥

The principal content of ∅ is ⊥.

theorem Question.mem_iInf_iff {W : Type u} {ι : Sort u_1} {f : ι → Question W} {q : Set W} : q ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), q ∈ f i

theorem Question.mem_biInf_iff {W : Type u} {ι : Type u_1} {I : Set ι} {f : ι → Question W} {q : Set W} : q ∈ ⨅ i ∈ I, f i ↔ ∀ i ∈ I, q ∈ f i

theorem Question.coe_ofSet {W : Type u} (p : Set W) : ↑(ofSet p) = Set.Iic p

The coercion of ofSet p is the interval Set.Iic p.

theorem Question.ofSet_le_ofSet_iff {W : Type u} {A B : Set W} : ofSet A ≤ ofSet B ↔ A ⊆ B

theorem Question.ofSet_injective {W : Type u} : Function.Injective ofSet

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

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

Equations

• Question.ofSetEmbedding = { toFun := Question.ofSet, inj' := ⋯, map_rel_iff' := ⋯ }

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

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

Equations

• Question.ofSetHom = { toFun := Question.ofSet, map_inf' := ⋯, map_top' := ⋯ }

theorem Question.isInquisitive_ofSet_sup : (ofSet {true} ⊔ ofSet {false}).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.ofSet_sup_ne : ofSet {true} ⊔ ofSet {false} ≠ ofSet ({true} ∪ {false})

The Truth-Support Bridge does not commute with ⊔: ofSet 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]).

@[instance_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