Inquisitive logic

Inquisitive logic interprets formulas by support at information states, sets of possible worlds, rather than by truth at worlds, so that questions and statements share one language: the inquisitive disjunction φ \\/ ψ is supported by a state that supports either disjunct. The propositional system InqB has ⊥, ∧, → and \\/ over atoms, and inquisitive modal logic adds the modalities □ and ⊞, interpreted over a model that relates each world to a set of states. This file develops basic results about support, including persistence, truth-conditionality, the proposition a formula expresses, and the validities of the two modalities.

Main definitions

• Inquisitive.Model: a valuation and a map from worlds to sets of information states.
• Inquisitive.Formula: formulas with \\/, □ and ⊞; the modal-free ones (Inquisitive.Formula.IsModalFree) are those of InqB.
• Inquisitive.support: the lower set of states supporting a formula.
• Inquisitive.TruthConditional: the statements, whose support is truth at every world.
• Inquisitive.proposition: the proposition a formula expresses, as a Question.

Implementation notes

The support of a modal-free formula depends only on the valuation (Inquisitive.support_eq_of_isModalFree), so InqB is the modal-free fragment of the modal language rather than a language of its own. States are finite sets of worlds.

References

• I. Ciardelli, Inquisitive Logic: Consequence and Inference in the Realm of Questions (2022)
• I. Ciardelli, Modalities in the realm of questions: Axiomatizing inquisitive epistemic logic (2014)
• I. Ciardelli and F. Roelofsen, Inquisitive dynamic epistemic logic (2015)
• I. Ciardelli, J. Groenendijk and F. Roelofsen, Inquisitive Semantics (2018)
• A. Anttila, Expressive completeness in team semantics (2025)

Models (§8.3)

structure Inquisitive.Model (W : Type u_3) (Atom : Type u_4) : Type (max u_3 u_4)

An inquisitive model has a valuation and relates each world w to a set Σ(w) of information states, under the epistemic reading the states in which the agent's issues are settled.

• inq : W → Finset (Finset W)

  inq w is the set Σ(w) of states related to w.

• val : Atom → W → Prop

  val p w says that the atom p is true at the world w.

def Inquisitive.Model.access {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (w : W) : Finset W

The induced accessibility σ(w) = ⋃ Σ(w), the agent's epistemic state at w.

Equations

• M.access w = (M.inq w).sup id

@[simp]

theorem Inquisitive.Model.mem_access {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) {w v : W} : v ∈ M.access w ↔ ∃ t ∈ M.inq w, v ∈ t

theorem Inquisitive.Model.subset_access {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) {w : W} {t : Finset W} (ht : t ∈ M.inq w) : t ⊆ M.access w

def ModalLogic.KripkeModel.toInquisitive {W : Type u_1} {Atom : Type u_2} (M : KripkeModel W Atom) : Inquisitive.Model W Atom

A Kripke model as the inquisitive modal model relating each world to its single successor state R[w] (§8.2).

Equations

• M.toInquisitive = { inq := fun (w : W) => {M.access w}, val := M.val }

@[simp]

theorem ModalLogic.KripkeModel.access_toInquisitive {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (w : W) : M.toInquisitive.access w = M.access w

Syntax (Definition 3.2.1; §8.2, §8.3)

inductive Inquisitive.Formula (Atom : Type u_3) : Type u_3

A formula is built from atoms and ⊥ by ∧, →, inquisitive disjunction \\/ and the two modalities.

• atom {Atom : Type u_3} (p : Atom) : Formula Atom
• bot {Atom : Type u_3} : Formula Atom
• conj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom
• impl {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom
• inqDisj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

  Inquisitive disjunction φ \\/ ψ.

• nec {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  The Kripke modality □φ (§8.2).

• ent {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  The properly inquisitive modality ⊞φ (§8.3), the entertain modality of [CR15].

@[instance_reducible]

instance Inquisitive.instReprFormula {Atom✝ : Type u_3} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• Inquisitive.instReprFormula = { reprPrec := Inquisitive.instReprFormula.repr }

def Inquisitive.instReprFormula.repr {Atom✝ : Type u_3} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Inquisitive.instReprFormula.repr Inquisitive.Formula.bot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Inquisitive.Formula.bot")).group prec✝

@[instance_reducible]

instance Inquisitive.instDecidableEqFormula {Atom✝ : Type u_3} [DecidableEq Atom✝] : DecidableEq (Formula Atom✝)

Equations

• Inquisitive.instDecidableEqFormula = Inquisitive.instDecidableEqFormula.decEq

def Inquisitive.instDecidableEqFormula.decEq {Atom✝ : Type u_3} [DecidableEq Atom✝] (x✝ x✝¹ : Formula Atom✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom a) (Inquisitive.Formula.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) (φ.conj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) (φ.impl ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) (φ.inqDisj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) φ.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (Inquisitive.Formula.atom p) φ.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot Inquisitive.Formula.bot = isTrue ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot (φ.conj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot (φ.impl ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot (φ.inqDisj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot φ.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq Inquisitive.Formula.bot φ.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) (φ_1.impl ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) (φ_1.inqDisj ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) φ_1.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.conj ψ) φ_1.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) (φ_1.conj ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) (φ_1.inqDisj ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) φ_1.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.impl ψ) φ_1.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) (φ_1.conj ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) (φ_1.impl ψ_1) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) φ_1.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq (φ.inqDisj ψ) φ_1.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec (φ_1.conj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec (φ_1.impl ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec (φ_1.inqDisj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq a.nec b.nec = if h : a = b then h ▸ have inst := Inquisitive.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.nec φ_1.ent = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent (Inquisitive.Formula.atom p) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent Inquisitive.Formula.bot = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent (φ_1.conj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent (φ_1.impl ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent (φ_1.inqDisj ψ) = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq φ.ent φ_1.nec = isFalse ⋯
• Inquisitive.instDecidableEqFormula.decEq a.ent b.ent = if h : a = b then h ▸ have inst := Inquisitive.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Inquisitive.Formula.neg {Atom : Type u_2} (φ : Formula Atom) : Formula Atom

¬φ := φ → ⊥ (Definition 3.1.2).

Equations

• φ.neg = φ.impl Inquisitive.Formula.bot

@[reducible, inline]

abbrev Inquisitive.Formula.disj {Atom : Type u_2} (φ ψ : Formula Atom) : Formula Atom

Classical disjunction φ ∨ ψ := ¬(¬φ ∧ ¬ψ) (Definition 3.1.2).

Equations

• φ.disj ψ = (φ.neg.conj ψ.neg).neg

@[reducible, inline]

abbrev Inquisitive.Formula.polarQ {Atom : Type u_2} (φ : Formula Atom) : Formula Atom

The polar question ?φ := φ \\/ ¬φ (Definition 3.2.2).

Equations

• φ.polarQ = φ.inqDisj φ.neg

def Inquisitive.Formula.IsModalFree {Atom : Type u_2} : Formula Atom → Prop

The modal-free formulas are those of the propositional system InqB (Definition 3.2.1).

Equations

• (Inquisitive.Formula.atom p).IsModalFree = True
• Inquisitive.Formula.bot.IsModalFree = True
• (φ.conj ψ).IsModalFree = (φ.IsModalFree ∧ ψ.IsModalFree)
• (φ.impl ψ).IsModalFree = (φ.IsModalFree ∧ ψ.IsModalFree)
• (φ.inqDisj ψ).IsModalFree = (φ.IsModalFree ∧ ψ.IsModalFree)
• φ.nec.IsModalFree = False
• φ.ent.IsModalFree = False

def Inquisitive.Formula.IsClassical {Atom : Type u_2} : Formula Atom → Prop

The classical formulas, those without inquisitive disjunction (§3.1, §8.2).

Equations

• (Inquisitive.Formula.atom p).IsClassical = True
• Inquisitive.Formula.bot.IsClassical = True
• (φ.conj ψ).IsClassical = (φ.IsClassical ∧ ψ.IsClassical)
• (φ.impl ψ).IsClassical = (φ.IsClassical ∧ ψ.IsClassical)
• (φ.inqDisj ψ).IsClassical = False
• φ.nec.IsClassical = φ.IsClassical
• φ.ent.IsClassical = φ.IsClassical

theorem Inquisitive.isLowerSet_image_coe {W : Type u_1} [Fintype W] {S : Set (Finset W)} (hS : IsLowerSet S) : IsLowerSet ((fun (t : Finset W) => ↑t) '' S)

Support (Definitions 3.1.3 and 3.2.3; §8.2, §8.3)

def Inquisitive.support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) : Formula Atom → LowerSet (Finset W)

The support set of φ in M is the set of information states that settle it. Support is persistent (Proposition 3.3.1), so the support set is a lower set of states, and conjunction, implication and inquisitive disjunction are the operations ⊓, ⇨, ⊔ of the Heyting algebra of lower sets ([CGR18]); ⊥ is supported by the empty state alone.

Equations

• Inquisitive.support M (Inquisitive.Formula.atom p) = { carrier := Team.flat (M.val p), lower' := ⋯ }
• Inquisitive.support M Inquisitive.Formula.bot = LowerSet.Iic ∅
• Inquisitive.support M (φ.conj ψ) = Inquisitive.support M φ ⊓ Inquisitive.support M ψ
• Inquisitive.support M (φ.impl ψ) = Inquisitive.support M φ ⇨ Inquisitive.support M ψ
• Inquisitive.support M (φ.inqDisj ψ) = Inquisitive.support M φ ⊔ Inquisitive.support M ψ
• Inquisitive.support M φ.nec = { carrier := Team.nec M.access ↑(Inquisitive.support M φ), lower' := ⋯ }
• Inquisitive.support M φ.ent = { carrier := Team.flat fun (w : W) => ∀ t ∈ M.inq w, t ∈ Inquisitive.support M φ, lower' := ⋯ }

@[simp]

theorem Inquisitive.mem_support_atom {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (s : Finset W) (p : Atom) : s ∈ support M (Formula.atom p) ↔ ∀ w ∈ s, M.val p w

@[simp]

theorem Inquisitive.mem_support_bot {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (s : Finset W) : s ∈ support M Formula.bot ↔ s = ∅

@[simp]

theorem Inquisitive.mem_support_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) (s : Finset W) : s ∈ support M (φ.conj ψ) ↔ s ∈ support M φ ∧ s ∈ support M ψ

@[simp]

theorem Inquisitive.mem_support_impl {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) (s : Finset W) : s ∈ support M (φ.impl ψ) ↔ ∀ t ⊆ s, t ∈ support M φ → t ∈ support M ψ

@[simp]

theorem Inquisitive.mem_support_inqDisj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) (s : Finset W) : s ∈ support M (φ.inqDisj ψ) ↔ s ∈ support M φ ∨ s ∈ support M ψ

@[simp]

theorem Inquisitive.mem_support_nec {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (s : Finset W) : s ∈ support M φ.nec ↔ ∀ w ∈ s, M.access w ∈ support M φ

@[simp]

theorem Inquisitive.mem_support_ent {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (s : Finset W) : s ∈ support M φ.ent ↔ ∀ w ∈ s, ∀ t ∈ M.inq w, t ∈ support M φ

def Inquisitive.decidableMemSupport {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) [Fintype W] [DecidableRel M.val] (φ : Formula Atom) (s : Finset W) : Decidable (s ∈ support M φ)

Support is decidable over a finite set of worlds, by structural recursion.

Equations

• Inquisitive.decidableMemSupport M (Inquisitive.Formula.atom p) x✝ = decidable_of_iff (∀ w ∈ x✝, M.val p w) ⋯
• Inquisitive.decidableMemSupport M Inquisitive.Formula.bot x✝ = decidable_of_iff (x✝ = ∅) ⋯
• Inquisitive.decidableMemSupport M (φ.conj ψ) x✝ = decidable_of_iff (x✝ ∈ Inquisitive.support M φ ∧ x✝ ∈ Inquisitive.support M ψ) ⋯
• Inquisitive.decidableMemSupport M (φ.impl ψ) x✝ = decidable_of_iff (∀ t ⊆ x✝, t ∈ Inquisitive.support M φ → t ∈ Inquisitive.support M ψ) ⋯
• Inquisitive.decidableMemSupport M (φ.inqDisj ψ) x✝ = decidable_of_iff (x✝ ∈ Inquisitive.support M φ ∨ x✝ ∈ Inquisitive.support M ψ) ⋯
• Inquisitive.decidableMemSupport M φ.nec x✝ = decidable_of_iff (∀ w ∈ x✝, M.access w ∈ Inquisitive.support M φ) ⋯
• Inquisitive.decidableMemSupport M φ.ent x✝ = decidable_of_iff (∀ w ∈ x✝, ∀ t ∈ M.inq w, t ∈ Inquisitive.support M φ) ⋯

@[instance_reducible]

instance Inquisitive.instDecidableMemFinsetLowerSetSupportOfFintypeOfDecidableRelVal {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) [Fintype W] [DecidableRel M.val] (φ : Formula Atom) (s : Finset W) : Decidable (s ∈ support M φ)

Equations

• Inquisitive.instDecidableMemFinsetLowerSetSupportOfFintypeOfDecidableRelVal M φ s = Inquisitive.decidableMemSupport M φ s

theorem Inquisitive.support_eq_of_isModalFree {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M M' : Model W Atom} (hval : M.val = M'.val) {φ : Formula Atom} : φ.IsModalFree → support M φ = support M' φ

The support of a modal-free formula depends only on the valuation.

The empty state (Proposition 3.3.1)

theorem Inquisitive.empty_mem_support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : ∅ ∈ support M φ

By the empty state property, the inconsistent state supports every formula.

Truth (Proposition 3.1.7)

theorem Inquisitive.mem_support_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (s : Finset W) : s ∈ support M φ.neg ↔ ∀ t ⊆ s, t ∈ support M φ → t = ∅

theorem Inquisitive.singleton_mem_support_impl {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) (w : W) : {w} ∈ support M (φ.impl ψ) ↔ {w} ∈ support M φ → {w} ∈ support M ψ

theorem Inquisitive.singleton_mem_support_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (w : W) : {w} ∈ support M φ.neg ↔ {w} ∉ support M φ

theorem Inquisitive.singleton_mem_support_disj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) (w : W) : {w} ∈ support M (φ.disj ψ) ↔ {w} ∈ support M φ ∨ {w} ∈ support M ψ

Truth-conditional formulas (§3.4)

def Inquisitive.truthSet {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : Set W

The truth set |φ|_M (§3.1) is the set of worlds at which φ is true, truth being support at the singleton state.

Equations

• Inquisitive.truthSet M φ = {w : W | {w} ∈ Inquisitive.support M φ}

def Inquisitive.TruthConditional {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : Prop

φ is truth-conditional in M (Definitions 2.6.3 and 3.4.1) when a state supports it iff it is true at each of its worlds: a statement rather than a question. This is flatness (Team.IsFlat) of the support set.

Equations

• Inquisitive.TruthConditional M φ = Team.IsFlat ↑(Inquisitive.support M φ)

theorem Inquisitive.truthConditional_atom {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (p : Atom) : TruthConditional M (Formula.atom p)

theorem Inquisitive.truthConditional_bot {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) : TruthConditional M Formula.bot

theorem Inquisitive.truthConditional_nec {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : TruthConditional M φ.nec

theorem Inquisitive.truthConditional_ent {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : TruthConditional M φ.ent

theorem Inquisitive.TruthConditional.iff {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : Model W Atom} {φ : Formula Atom} (s : Finset W) (h : TruthConditional M φ) : s ∈ support M φ ↔ ∀ w ∈ s, {w} ∈ support M φ

theorem Inquisitive.TruthConditional.support_iff {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : Model W Atom} {φ : Formula Atom} (s : Finset W) (h : TruthConditional M φ) : s ∈ support M φ ↔ ↑s ⊆ truthSet M φ

theorem Inquisitive.TruthConditional.conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : Model W Atom} {φ ψ : Formula Atom} (hφ : TruthConditional M φ) (hψ : TruthConditional M ψ) : TruthConditional M (φ.conj ψ)

theorem Inquisitive.TruthConditional.impl {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : Model W Atom} {ψ : Formula Atom} (hψ : TruthConditional M ψ) (φ : Formula Atom) : TruthConditional M (φ.impl ψ)

An implication with a truth-conditional consequent is truth-conditional, whatever its antecedent (Proposition 3.4.7).

theorem Inquisitive.truthConditional_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : TruthConditional M φ.neg

Every negation is truth-conditional (Proposition 3.4.8).

theorem Inquisitive.truthConditional_disj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : TruthConditional M (φ.disj ψ)

theorem Inquisitive.truthConditional_of_isClassical {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (h : φ.IsClassical) : TruthConditional M φ

Classical formulas are truth-conditional (Proposition 3.1.8).

theorem Inquisitive.mem_support_neg_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (s : Finset W) : s ∈ support M φ.neg.neg ↔ ∀ w ∈ s, {w} ∈ support M φ

¬¬φ is supported exactly where φ is true at every world (Proposition 3.4.9).

theorem Inquisitive.truthSet_neg_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : truthSet M φ.neg.neg = truthSet M φ

theorem Inquisitive.truthConditional_iff_support_neg_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : TruthConditional M φ ↔ support M φ.neg.neg = support M φ

The double negation law holds exactly for statements (Proposition 3.4.10).

theorem Inquisitive.mem_support_impl_iff_of_truthConditional {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (ψ : Formula Atom) (s : Finset W) [Fintype W] [DecidableRel M.val] {α : Formula Atom} (hα : TruthConditional M α) : s ∈ support M (α.impl ψ) ↔ {w ∈ s | {w} ∈ support M α} ∈ support M ψ

By the Ramsey test (Proposition 2.5.2), for a statement α, α → ψ is supported at s iff ψ is supported at the α-worlds of s.

The proposition expressed (Proposition 3.3.1, §3.5)

def Inquisitive.proposition {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) [Fintype W] : Question W

The inquisitive proposition [φ]_M expressed by φ is the support set as a Question, carried from finite states to sets of worlds.

Equations

• Inquisitive.proposition M φ = Question.ofLowerSet ((fun (t : Finset W) => ↑t) '' ↑(Inquisitive.support M φ)) ⋯ ⋯

@[simp]

theorem Inquisitive.mem_proposition {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) [Fintype W] {s : Set W} : s ∈ proposition M φ ↔ ∃ (t : Finset W), ↑t = s ∧ t ∈ support M φ

@[simp]

theorem Inquisitive.coe_mem_proposition {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (s : Finset W) [Fintype W] : ↑s ∈ proposition M φ ↔ s ∈ support M φ

theorem Inquisitive.proposition_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) [Fintype W] : proposition M (φ.conj ψ) = proposition M φ ⊓ proposition M ψ

Conjunction is the meet of propositions.

theorem Inquisitive.proposition_inqDisj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) [Fintype W] : proposition M (φ.inqDisj ψ) = proposition M φ ⊔ proposition M ψ

Inquisitive disjunction is the join.

theorem Inquisitive.proposition_impl {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) [Fintype W] : proposition M (φ.impl ψ) = proposition M φ ⇨ proposition M ψ

Implication is the Heyting arrow.

theorem Inquisitive.proposition_bot {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) [Fintype W] : proposition M Formula.bot = ⊥

⊥ is the bottom.

theorem Inquisitive.info_proposition {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) [Fintype W] : (proposition M φ).info = truthSet M φ

The truth set is the union of the proposition (Proposition 3.3.5).

theorem Inquisitive.truthConditional_iff_proposition_eq {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) [Fintype W] : TruthConditional M φ ↔ proposition M φ = Question.ofSet (truthSet M φ)

On propositions, Definition 3.4.1 says that φ is a statement iff it expresses the declarative proposition of its truth set.

theorem Inquisitive.proposition_neg_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) [Fintype W] : proposition M φ.neg.neg = (proposition M φ)ᶜᶜ

¬¬φ expresses the non-inquisitive projection of [φ]_M, its double complement (Proposition 3.4.9).

Modalities (§8.2, §8.3)

theorem Inquisitive.TruthConditional.support_eq {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : Model W Atom} {φ ψ : Formula Atom} (hφ : TruthConditional M φ) (hψ : TruthConditional M ψ) (h : ∀ (w : W), {w} ∈ support M φ ↔ {w} ∈ support M ψ) : support M φ = support M ψ

Two statements that agree at every world have the same support.

theorem Inquisitive.support_nec_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : support M (φ.conj ψ).nec = support M (φ.nec.conj ψ.nec)

□ commutes with ∧ (§8.2).

theorem Inquisitive.support_nec_impl_nec {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : support M ((φ.impl ψ).nec.impl (φ.nec.impl ψ.nec)) = ⊤

The K axiom for □ (§8.2).

theorem Inquisitive.support_nec_of_eq_top {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (h : support M φ = ⊤) : support M φ.nec = ⊤

Necessitation for □ (§8.2).

theorem Inquisitive.support_nec_inqDisj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : support M (φ.inqDisj ψ).nec = support M (φ.nec.disj ψ.nec)

□ distributes over inquisitive disjunction, □(φ \\/ ψ) ≡ □φ ∨ □ψ (§8.2).

theorem Inquisitive.support_ent_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : support M (φ.conj ψ).ent = support M (φ.ent.conj ψ.ent)

⊞ commutes with ∧ (§8.3).

theorem Inquisitive.support_ent_impl_ent {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ ψ : Formula Atom) : support M ((φ.impl ψ).ent.impl (φ.ent.impl ψ.ent)) = ⊤

The K axiom for ⊞ (§8.3).

theorem Inquisitive.support_ent_of_eq_top {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (h : support M φ = ⊤) : support M φ.ent = ⊤

Necessitation for ⊞ (§8.3).

theorem Inquisitive.support_nec_le_ent {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) : support M φ.nec ≤ support M φ.ent

□φ entails ⊞φ, since each related state lies in the epistemic state and support is persistent (§8.3).

theorem Inquisitive.support_ent_eq_nec_of_truthConditional {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) (φ : Formula Atom) (h : TruthConditional M φ) : support M φ.ent = support M φ.nec

On statements the two modalities coincide (§8.3).

theorem Inquisitive.support_ent_toInquisitive {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (φ : Formula Atom) (M : ModalLogic.KripkeModel W Atom) : support M.toInquisitive φ.ent = support M.toInquisitive φ.nec

On a Kripke model ⊞ is □, the only related state being R[w] (§8.2).

The closure cell

theorem Inquisitive.not_supClosed_inqDisj_of_witness {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) {p q : Atom} {w₁ w₂ : W} (hp₁ : M.val p w₁) (hq₁ : ¬M.val q w₁) (hp₂ : ¬M.val p w₂) (hq₂ : M.val q w₂) : ¬SupClosed ↑(support M ((Formula.atom p).inqDisj (Formula.atom q)))

Inquisitive disjunction breaks union closure. With p true only at w₁ and q only at w₂, the singletons support p \\/ q but their union supports neither disjunct.

theorem Inquisitive.definableClass_support_subset {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : Model W Atom) : (Team.definableClass fun (φ : Formula Atom) (t : Finset W) => t ∈ support M φ) ⊆ {P : Team.TeamProperty W | IsLowerSet P ∧ ∅ ∈ P}

Inquisitive modal logic is sound for the downward-closed, empty-team cell of [Ant25]'s programme, which it shares with dependence logic.