Linglib.Core.Logic.Modal.Inquisitive

[Cia22] [Cia14] [CGR18]

Inquisitive modal logic extends classical modal logic with a treatment of questions alongside statements, following the Ciardelli-Groenendijk-Roelofsen tradition. The originating modal paper is [Cia14] (Advances in Modal Logic), with the propositional inquisitive system InqB developed in [CGR18] (Oxford University Press) and the modal preview in [Cia22] Chapter 8.

Formulas are evaluated at information states (teams of worlds), with two crucial novelties relative to BSML / MDL / MIL:

The inquisitive disjunction φ \\/ ψ (written inqDisj here), which is supported by a team s iff s ⊨ φ or s ⊨ ψ (global disjunction, not the team-split ∨ of BSML).
The implication φ → ψ, which is supported by s iff every subteam t ⊆ s satisfies t ⊨ φ → t ⊨ ψ (universal subteam quantification).
The Kripke modality □φ, supported by s iff every w ∈ s has M, R[w] ⊨ φ (per-world full image of the accessibility relation, distinct from BSML's per-world sub-witness or MDL's single-witness or MIL's lax form).

Reference: [Cia22] Chapter 8 (modal preview), with the propositional InqB base from Chapter 3.

Closure profile #

Property	InqML formula
`IsLowerSet`	✓ (persistence)
`SupClosed`	✗ broken by `\\/`
`∅ ∈ support`	✓

InqML inhabits the same closure cell as MDL (downward-closed + empty, sup-closure broken) — but via a different syntactic mechanism: the inquisitive disjunction \\/ breaks union closure where MDL's dependence atom does. This is the second inhabitant of this cell in linglib, demonstrating that the architectural pattern "team-semantic logic with non-classical disjunction-like connective fails union closure" applies regardless of whether the connective is question- flavored (InqML) or dependence-flavored (MDL).

Main declarations #

Formula — InqML syntax (Ciardelli §8.2 modal + §3 propositional base).
eval — single-relation team-semantic evaluation (only support, no anti-support). Negation derived as φ → ⊥, matching [Cia22].
Formula.neg, Formula.polarQ — standard inquisitive abbreviations (¬φ := φ → ⊥, ?φ := φ \\/ ¬φ).
Formula.modalDepth — depth of nested □.
isLowerSet_support — persistence property (Ciardelli §3 Lemma).
support_empty — every formula supported on the empty team.
not_supClosed_inqDisj_of_witness — constructive witness that inquisitive disjunction \\/ breaks union closure.

Implementation notes #

The standard inquisitive connective set is {⊥, ∧, →, \\/} with ¬φ := φ → ⊥, !φ := ¬¬φ (declarative variant), and ?φ := φ \\/ ¬φ (polar question) as standard abbreviations. We include \\/ and → as primitives; ¬, !, ? can be added as helpers later when a consumer needs them.

The modal extension adds only □ per [Cia22] §8.2. Section 8.3 introduces a second modality ⊞ (properly inquisitive, using a relation R : W × ℘(W) instead of R : W × W) — deferred to a follow-up file/PR because it requires a different model carrier than KripkeModel.

The KripkeModel carrier from Core/Logic/Modal/Kripke.lean is reused. Per-world □ semantics naturally fits the R : W → Finset W shape.

Sibling logics in `Core/Logic/Modal/` #

Modal/Kripke.lean — the carrier type.
Modal/Dependence.lean — MDL (Väänänen 2008), bilateral, dep atoms.
Modal/Inclusion.lean — MIL (AHY 2024), unilateral, inclusion atoms.
Modal/Inquisitive.lean (this file) — InqML, unilateral, inquisitive disjunction.

Todo #

⊞ modality (Ciardelli §8.3) — needs a InquisitiveModalModel with R : W → Finset (Finset W). Add when a downstream consumer needs it.
Declarative !φ := ¬¬φ and polar question ?φ := φ \\/ ¬φ abbreviations + their closure-property lemmas.
First-order inquisitive modal logic (InqBQ + modality) — Ciardelli §8 mentions but full development in subsequent literature.
Bisim invariance — Ciardelli & Otto (2020) "Inquisitive bisimulation".

Documentation