Questions as inquisitive contents

A Question W is a non-empty downward-closed family of information states over W, the states that resolve an inquisitive proposition ([CGR18], [Cia22]). Hamblin sets (Hamblin.lean) and partition questions (Partition/Inquisitive.lean) embed into it. Ordered by inclusion, questions form a complete distributive lattice ([Pun19]) whose meet is conjunction and whose join is inquisitive disjunction; it is Heyting but not Boolean.

Main definitions

• Question.alt, Question.info: the alternatives, the maximal resolving states, and the informative content.
• Question.IsInformative, Question.IsInquisitive.
• Question.ofSet p: the declarative of p, the principal ideal below p.
• Question.query P: the non-informative projection ?P.
• Question.relativeTo Q C: Q relative to a context ([Rob12]).
• Question.IsNormal, Question.FG: questions generated by their alternatives, and by finitely many states.

Main statements

• Question.gc_info_ofSet, Question.infoHom: info is left adjoint to ofSet and a complete lattice homomorphism.
• Question.IsNormal.eq_iSup_ofSet_alt: the resolutions theorem, a normal question is the join of the declaratives of its alternatives.
• Question.fg_iff_finite_alt_and_isNormal: finite generation is finitely many alternatives plus normality.
• Question.compl_eq, Question.compl_compl_inf_query: the pseudo-complement is the declarative of the complemented informative content, and every content is the meet of its non-inquisitive and non-informative projections.
• Question.ofSet_sup_compl_ne_top, Question.ofSet_sup_ofSet_ne: excluded middle fails, and ofSet does not preserve joins.

Implementation notes

Question W is a bundled structure with a SetLike instance rather than a LowerSet (Set W) because the bottom elements differ: the bottom question is {∅}, resolved only by the inconsistent state, while the bottom lower set is empty. Generators are stated against lowerClosure on the coercion (isNormal_iff_coe_eq_lowerClosure). The distributive lattice is registered through CompleteDistribLattice.ofMinimalAxioms.

References

• [Cia22]
• [CGR18]
• [Pun16]
• [Pun19]
• [Rob12]
• [TRA18]

structure Question (W : Type u) : Type u

A question is a non-empty downward-closed family of information states over W, the states that resolve it.

• 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

  A state included in a resolving state resolves the question.

@[instance_reducible]

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

A question coerces to its set of resolving states.

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

@[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 a question are its maximal resolving states.

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 a question is the union of its resolving states.

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.

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

A world lies in the informative content of a question iff its singleton resolves the question, so truth at a world is support by the singleton state.

theorem Question.subset_info_of_mem {W : Type u} {P : Question W} {q : Set W} (h : q ∈ P) : q ⊆ P.info

A resolving state lies within the informative content.

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

theorem Question.isLowerSet {W : Type u} (P : Question W) : IsLowerSet ↑P

The resolving states of a question form a lower set, the inverse of ofLowerSet.

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

The declarative of p is resolved by the states included in p, the principal ideal below p, as Filter.principal is the principal filter.

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

The lattice of questions

Ordered by inclusion of resolving states, questions form a complete distributive lattice ([Pun19]): a state resolves P ⊓ Q iff it resolves both, and the inquisitive disjunction P ⊔ Q iff it resolves either; every state resolves ⊤ and only ∅ resolves ⊥. A join adjoins ∅, so that the join of the empty family is ⊥. Implication and negation are the Heyting ⇨ and ᶜ.

@[instance_reducible]

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

Equations

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

@[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 ∈ ⊤

@[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.le_def {W : Type u} {P Q : Question W} : P ≤ Q ↔ P.props ⊆ Q.props

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

@[instance_reducible]

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

Meets distribute over joins and joins over meets, since intersection and union of the underlying families of states do.

Equations

• Question.instCompleteDistribLattice = CompleteDistribLattice.ofMinimalAxioms ⋯

The non-informative projection

The non-informative projection ?P keeps the issue of P and trivializes its informative content by admitting the states within its complement ([CGR18]). The non-inquisitive projection !P is the double complement Pᶜᶜ (compl_compl_eq).

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

The non-informative projection ?P adds to P the states within the complement of its informative content.

Equations

• P.query = P ⊔ Question.ofSet P.infoᶜ

@[simp]

theorem Question.mem_query {W : Type u} {P : Question W} {q : Set W} : q ∈ P.query ↔ q ∈ P ∨ q ⊆ P.infoᶜ

@[simp]

theorem Question.info_query {W : Type u} (P : Question W) : P.query.info = Set.univ

theorem Question.query_eq_self_of_info_eq_univ {W : Type u} {P : Question W} (h : P.info = Set.univ) : P.query = P

A non-informative content is its own non-informative projection.

@[simp]

theorem Question.query_query {W : Type u} (P : Question W) : P.query.query = P.query

theorem Question.isInquisitive_query {W : Type u} {P : Question W} (h₁ : P.info ≠ Set.univ) (h₂ : P.info ≠ ∅) : P.query.IsInquisitive

?P raises a genuine issue unless P is a tautology or a contradiction.

theorem Question.disjoint_iff {W : Type u} {P Q : Question W} : Disjoint P Q ↔ ∀ q ∈ P, q ∈ Q → q = ∅

Two contents are disjoint iff the inconsistent state is the only state they share.

theorem Question.eq_top_iff_univ_mem {W : Type u} {P : Question W} : P = ⊤ ↔ Set.univ ∈ P

A content is the tautology iff it contains the universal state ([CGR18]).

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

A state resolves P ⇨ Q iff every substate resolving P resolves Q.

def Question.relativeTo {W : Type u} (Q : Question W) (C : Set W) : Question W

The question Q relative to a context C is resolved by the states that resolve Q once cut down to C; it is the Heyting implication ofSet C ⇨ Q.

Equations

• Q.relativeTo C = Question.ofSet C ⇨ Q

@[simp]

theorem Question.mem_relativeTo {W : Type u} {Q : Question W} {C s : Set W} : s ∈ Q.relativeTo C ↔ C ∩ s ∈ Q

@[simp]

theorem Question.relativeTo_univ {W : Type u} (Q : Question W) : Q.relativeTo Set.univ = Q

theorem Question.le_relativeTo {W : Type u} (Q : Question W) (C : Set W) : Q ≤ Q.relativeTo C

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

A state resolves an indexed join iff it is empty or resolves some member.

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, ⊆) commuting with ⊔, ⊓, ⊥ and ⊤, and indeed with arbitrary joins and meets: it is a complete lattice homomorphism (infoHom). Meets need no inquisitiveness assumption, since singleton states witness the informative content.

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

@[simp]

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

info commutes with the meet: singleton states witness the reverse inclusion, so no non-inquisitiveness assumption is needed (strengthening the declarative case of [CGR18]'s update fact).

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 a Galois insertion, since 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.

theorem Question.info_sInf {W : Type u} (S : Set (Question W)) : (sInf S).info = ⋂ P ∈ S, P.info

info turns arbitrary meets into intersections: a world is in the informative content of every member exactly when its singleton supports each of them.

theorem Question.info_iInf {W : Type u} {ι : Sort u_1} (f : ι → Question W) : (⨅ (i : ι), f i).info = ⋂ (i : ι), (f i).info

info turns meets into intersections.

def Question.infoHom {W : Type u} : CompleteLatticeHom (Question W) (Set W)

info as a complete lattice homomorphism into the classical propositions.

Equations

• Question.infoHom = { toFun := Question.info, map_sInf' := ⋯, map_sSup' := ⋯ }

@[simp]

theorem Question.infoHom_apply {W : Type u} (P : Question W) : infoHom P = P.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

The alternatives are the Maximal resolving states.

theorem Question.alt_isAntichain {W : Type u} (P : Question W) : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) P.alt

The alternatives of P form an antichain under ⊆: no alternative is properly contained in another.

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.

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

Normal questions

A question is normal when its alternatives generate it: every resolving state is included in an alternative, so that the resolving states are the lower closure of the alternatives ([Cia22]). An antichain generating a question is then its set of alternatives, and a question has such a basis exactly when it is normal. Finitely many resolving states suffice (isNormal_of_finite), declaratives are normal, and so is the inquisitive disjunction of two normal questions; but normality fails in general: on an infinite W the finite states form a question with no alternatives at all, although its informative content is all of W.

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

When there are finitely many resolving states, every resolving state extends to an alternative. The hypothesis bounds the resolving states, not W.

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

A question is normal when every resolving state is included in an alternative.

Equations

• P.IsNormal = ∀ s ∈ P, ∃ a ∈ P.alt, s ⊆ a

theorem Question.isNormal_of_finite {W : Type u} {P : Question W} (hP : P.props.Finite) : P.IsNormal

A question with finitely many resolving states is normal.

theorem Question.isNormal_iff_coe_eq_lowerClosure {W : Type u} {P : Question W} : P.IsNormal ↔ ↑P = ↑(lowerClosure P.alt)

A question is normal iff its resolving states are the lower closure of its alternatives.

theorem Question.IsNormal.coe_eq_lowerClosure {W : Type u} {P : Question W} : P.IsNormal → ↑P = ↑(lowerClosure P.alt)

Alias of the forward direction of Question.isNormal_iff_coe_eq_lowerClosure.

---

A question is normal iff its resolving states are the lower closure of its alternatives.

theorem Question.alt_eq_of_coe_eq_lowerClosure {W : Type u} {P : Question W} {T : Set (Set W)} (hT : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) T) (h : ↑P = ↑(lowerClosure T)) : P.alt = T

An antichain generating P is its set of alternatives: the alternatives of a normal question are its unique basis ([Cia22]).

theorem Question.isNormal_of_coe_eq_lowerClosure {W : Type u} {P : Question W} {T : Set (Set W)} (hT : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) T) (h : ↑P = ↑(lowerClosure T)) : P.IsNormal

A question generated by an antichain is normal, so that a question has a basis exactly when it is normal ([Cia22]).

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

The informative content of a normal question is the union of its alternatives.

theorem Question.IsNormal.alt_nonempty {W : Type u} {P : Question W} (hP : P.IsNormal) : P.alt.Nonempty

A normal question has an alternative, the one above ∅.

theorem Question.isNormal_ofSet {W : Type u} (p : Set W) : (ofSet p).IsNormal

A declarative is normal: its one alternative covers it.

theorem Question.IsNormal.sup {W : Type u} {P Q : Question W} (hP : P.IsNormal) (hQ : Q.IsNormal) : (P ⊔ Q).IsNormal

The inquisitive disjunction of normal questions is normal.

Questions generated by a family of states

The join ⨆ a ∈ S, ofSet a of the declaratives of a family S is the question S generates: a state resolves it iff it is included in a member of S, or is ∅, the one state resolving the join ⊥ of the empty family. Every Hamblin construction has this form (which, polar, fromSetoid), and an antichain generating a question is its set of alternatives, so their alternatives are computed once here. A finite family generates a normal question whose alternatives are among its members, and the meet of two generated questions is generated by the pairwise intersections, so finitely generated questions are closed under the connectives.

theorem Question.coe_biSup_ofSet {W : Type u} {S : Set (Set W)} (hS : S.Nonempty) : ↑(⨆ a ∈ S, ofSet a) = ↑(lowerClosure S)

A nonempty family generates the join of its declaratives.

theorem Question.biSup_ofSet_le_iff {W : Type u} {S : Set (Set W)} {Q : Question W} : ⨆ a ∈ S, ofSet a ≤ Q ↔ ∀ a ∈ S, a ∈ Q

The join of the declaratives of a family entails exactly the questions every member resolves.

theorem Question.alt_biSup_ofSet {W : Type u} {S : Set (Set W)} (hS : S.Nonempty) (hA : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) S) : (⨆ a ∈ S, ofSet a).alt = S

The alternatives of the join of the declaratives of a nonempty antichain are its members.

theorem Question.alt_ofSet_sup_ofSet {W : Type u} {A B : Set W} (hAB : ¬A ⊆ B) (hBA : ¬B ⊆ A) : (ofSet A ⊔ ofSet B).alt = {A, B}

The alternatives of the join of two incomparable declaratives are the two sets.

theorem Question.mem_biSup_ofSet {W : Type u} {S : Set (Set W)} {q : Set W} : q ∈ ⨆ a ∈ S, ofSet a ↔ q = ∅ ∨ ∃ a ∈ S, q ⊆ a

A state resolves the join of the declaratives of a family iff it is ∅ or lies in a member.

theorem Question.alt_biSup_ofSet_subset {W : Type u} (S : Set (Set W)) : (⨆ a ∈ S, ofSet a).alt ⊆ insert ∅ S

The alternatives of the join of the declaratives of a family lie in the family, or are ∅ when the family is empty.

theorem Question.isNormal_biSup_ofSet {W : Type u} {S : Set (Set W)} (hS : S.Finite) : (⨆ a ∈ S, ofSet a).IsNormal

The declaratives of a finite family generate a normal question.

theorem Question.biSup_ofSet_inf_biSup_ofSet {W : Type u} (S T : Set (Set W)) : (⨆ a ∈ S, ofSet a) ⊓ ⨆ b ∈ T, ofSet b = ⨆ c ∈ Set.image2 (fun (x1 x2 : Set W) => x1 ∩ x2) S T, ofSet c

The meet of the questions two families generate is generated by their pairwise intersections.

The resolutions theorem

A normal question is the join of the declaratives of its alternatives, the inquisitive analogue of disjunctive normal form. Off normal questions only the inequality ⨆ p ∈ alt P, ofSet p ≤ P holds.

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

The join of the declaratives of the alternatives of P entails P.

theorem Question.IsNormal.eq_iSup_ofSet_alt {W : Type u} {P : Question W} (hP : P.IsNormal) : P = ⨆ p ∈ P.alt, ofSet p

A normal question is the join of the declaratives of its alternatives, the resolutions theorem.

Finitely generated questions

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

A question is finitely generated when it is the join of the declaratives of finitely many states, cf. Submodule.FG.

Equations

• P.FG = ∃ (S : Set (Set W)), S.Finite ∧ ⨆ a ∈ S, Question.ofSet a = P

theorem Question.fg_ofSet {W : Type u} (p : Set W) : (ofSet p).FG

theorem Question.FG.sup {W : Type u} {P Q : Question W} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem Question.FG.inf {W : Type u} {P Q : Question W} (hP : P.FG) (hQ : Q.FG) : (P ⊓ Q).FG

theorem Question.FG.isNormal {W : Type u} {P : Question W} (hP : P.FG) : P.IsNormal

theorem Question.FG.finite_alt {W : Type u} {P : Question W} (hP : P.FG) : P.alt.Finite

theorem Question.fg_iff_finite_alt_and_isNormal {W : Type u} {P : Question W} : P.FG ↔ P.alt.Finite ∧ P.IsNormal

A question is finitely generated exactly when it has finitely many alternatives and is generated by them.

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.mem_iff_subset_info {W : Type u} {P : Question W} (h : P.info ∈ P) {s : Set W} : s ∈ P ↔ s ⊆ P.info

A question resolved by its own informative content is resolved by exactly the states included in it.

theorem Question.info_mem_iff_eq_ofSet_info {W : Type u} (P : Question W) : P.info ∈ P ↔ P = ofSet P.info

A question is resolved by its informative content iff it is the declarative of its informative content.

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

A question is resolved by its informative content iff that is its only alternative.

theorem Question.IsNormal.exists_alt_eq_singleton_iff {W : Type u} {P : Question W} (hP : P.IsNormal) : (∃ (p : Set W), P.alt = {p}) ↔ P.info ∈ P

A normal content has a single alternative iff it is declarative: its alternatives generate it, so a lone alternative is its informative content. Normality is needed, since over an infinite W a content can have one alternative and resolving states beyond it.

Heyting derivatives

The pseudo-complement of a question is the declarative of the complement of its informative content (compl_eq). From this identity follow the operators of [CGR18] and [Pun19]: the non-inquisitive projection !P = Pᶜᶜ = ofSet (info P) (compl_compl_eq), whose fixed points, the non-inquisitive contents, are the regular elements (isRegular_iff_not_isInquisitive); the non-informative projection ?P = P ⊔ Pᶜ (query_eq_sup_compl); and the division law !P ⊓ ?P = P (compl_compl_inf_query).

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

The pseudo-complement of a question is the declarative of the complement of its informative content.

@[simp]

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

The informative content of the pseudo-complement is the complement of the informative content.

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

The non-inquisitive projection !P = Pᶜᶜ consists of the states within the informative content of P ([CGR18]).

@[simp]

theorem Question.mem_compl_compl {W : Type u} {P : Question W} {q : Set W} : q ∈ Pᶜᶜ ↔ q ⊆ P.info

@[simp]

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

theorem Question.not_isInquisitive_compl {W : Type u} (P : Question W) : ¬Pᶜ.IsInquisitive

A complement is never inquisitive.

theorem Question.isRegular_iff_not_isInquisitive {W : Type u} {P : Question W} : Heyting.IsRegular P ↔ ¬P.IsInquisitive

The non-inquisitive contents are the regular elements of the Heyting algebra of contents, the fixed points of the non-inquisitive projection.

theorem Question.isRegular_ofSet {W : Type u} (p : Set W) : Heyting.IsRegular (ofSet p)

@[simp]

theorem Question.compl_compl_ofSet {W : Type u} (p : Set W) : (ofSet p)ᶜᶜ = ofSet p

theorem Question.query_eq_sup_compl {W : Type u} (P : Question W) : P.query = P ⊔ Pᶜ

The non-informative projection ?P is P ⊔ Pᶜ ([CGR18]).

theorem Question.compl_compl_inf_query {W : Type u} (P : Question W) : Pᶜᶜ ⊓ P.query = P

Every question is the meet of its non-inquisitive and its non-informative projection, the division law.

Excluded middle fails

The lattice is Heyting but not Boolean: the join of a declarative and its complement is a polar question, inquisitive unless the declarative is the tautology or the contradiction, and so not ⊤.

theorem Question.isInquisitive_ofSet_sup_ofSet {W : Type u} {A B : Set W} (hAB : ¬A ⊆ B) (hBA : ¬B ⊆ A) : (ofSet A ⊔ ofSet B).IsInquisitive

The join of two incomparable declaratives is inquisitive.

theorem Question.ofSet_sup_compl_ne_top {W : Type u} {p : Set W} (h₁ : p.Nonempty) (h₂ : pᶜ.Nonempty) : ofSet p ⊔ (ofSet p)ᶜ ≠ ⊤

Excluded middle fails for every declarative other than the tautology and the contradiction.

The declarative embedding

The classical propositions embed into the questions through ofSet, [Cia22]'s truth-support bridge, by which a statement names the information type generated by its truth set. The embedding is order-faithful (ofSetEmbedding) and preserves meets and ⊤ (ofSetHom) but not joins (ofSet_sup_ofSet_ne): inquisitive content enters at ⊔. The context sets of Discourse/CommonGround.lean are the declarative fragment 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

theorem Question.disjoint_ofSet_iff {W : Type u} {A B : Set W} : Disjoint (ofSet A) (ofSet B) ↔ Disjoint A B

Declaratives are disjoint exactly when their informative contents are.

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

ofSet is an order embedding of the propositions into the questions.

Equations

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

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

ofSet preserves meets and ⊤, but not joins (ofSet_sup_ofSet_ne).

Equations

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

theorem Question.ofSet_sup_ofSet_ne {W : Type u} {A B : Set W} (hAB : ¬A ⊆ B) (hBA : ¬B ⊆ A) : ofSet A ⊔ ofSet B ≠ ofSet (A ∪ B)

ofSet does not preserve joins: the join of two incomparable declaratives is inquisitive, and the declarative of their union is not.