Ciardelli 2022 — InqML denotation into Question

[Cia22] [CGR18]

Formulas of inquisitive modal logic ([Cia22] Ch. 8) denote inquisitive contents. Question.ofInqML M φ packages the supporting teams of φ — viewed as information states via the canonical Finset W → Set W coercion — into a Question W; the downward-closure and empty-state obligations discharge directly from InqML's persistence (isLowerSet_support) and empty-team (support_empty) lemmas.

The denotation is a lattice/Heyting homomorphism: it carries InqML's conj/inqDisj/impl/bot to the Question algebra's ⊓/⊔/⇨/⊥ (ofInqML_conj … ofInqML_bot), through the injective Finset → Set coercion and the pointwise mem_himp characterization of the Heyting arrow.

Main declarations

• Question.ofInqML — the InqML denotation map.
• Question.mem_ofInqML — its membership characterization.
• Question.ofInqML_conj / _inqDisj / _impl / _bot — the lattice/Heyting homomorphism laws.

def Question.ofInqML {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) (φ : Core.Logic.Modal.Inquisitive.Formula Atom) : Question W

The inquisitive content denoted by an InqML formula at a Kripke model. A state s : Set W lies in the denotation iff some supporting team t : Finset W coerces to s.

Built via Question.ofLowerSet: the two Question obligations are exactly InqML's empty-team property (support_empty) and persistence (isLowerSet_support), bridged across the Finset → Set coercion.

Equations

• Question.ofInqML M φ = Question.ofLowerSet ((fun (t : Finset W) => ↑t) '' {t : Finset W | Core.Logic.Modal.Inquisitive.support M φ t}) ⋯ ⋯

@[simp]

theorem Question.mem_ofInqML {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) (φ : Core.Logic.Modal.Inquisitive.Formula Atom) (s : Set W) : s ∈ ofInqML M φ ↔ ∃ (t : Finset W), ↑t = s ∧ Core.Logic.Modal.Inquisitive.support M φ t

Membership in the InqML denotation: a state s : Set W lies in the Question iff some supporting team t : Finset W coerces to s.

theorem Question.ofInqML_conj {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) (φ ψ : Core.Logic.Modal.Inquisitive.Formula Atom) : ofInqML M (φ.conj ψ) = ofInqML M φ ⊓ ofInqML M ψ

ofInqML carries InqML conjunction to the lattice meet ⊓. support (.conj φ ψ) is the pointwise And, so the supporting-team set is an intersection, and the injective Finset → Set coercion preserves it.

theorem Question.ofInqML_inqDisj {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) (φ ψ : Core.Logic.Modal.Inquisitive.Formula Atom) : ofInqML M (φ.inqDisj ψ) = ofInqML M φ ⊔ ofInqML M ψ

ofInqML carries InqML disjunction to the lattice join ⊔. support (.inqDisj φ ψ) is the pointwise Or, and Set.image distributes over union unconditionally.

theorem Question.ofInqML_impl {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) (φ ψ : Core.Logic.Modal.Inquisitive.Formula Atom) : ofInqML M (φ.impl ψ) = ofInqML M φ ⇨ ofInqML M ψ

ofInqML carries InqML implication to the Heyting arrow ⇨. support (.impl φ ψ) t is ∀ u ⊆ t, support φ u → support ψ u.

theorem Question.ofInqML_bot {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : Core.Logic.Modal.KripkeModel W Atom) : ofInqML M Core.Logic.Modal.Inquisitive.Formula.bot = ⊥

ofInqML carries InqML ⊥ to the lattice bottom ⊥. support .bot t holds iff t = ∅, so the denotation is {∅}.