Ciardelli (2022): Inquisitive Logic: Consequence and Inference in the Realm of Questions

This file formalizes the illustrations of inquisitive modal logic in the last chapter of [Cia22]. The Kripke modality □ applied to a question is a statement, so that knowing whether p amounts to knowing that p or knowing that ¬p (nec_polarQ). The properly inquisitive modality ⊞, supported when every state related to each world supports its argument, coincides with □ on statements, and on questions it expresses Ciardelli and Roelofsen's wondering, ¬□μ ∧ ⊞μ.

In the three inquisitive states of Fig. 8.1 the agent knows whether p, wonders whether p, and does neither (fig81a_knows, fig81b_wonders, fig81c_neither), and the second shows that ⊞, unlike □, does not distribute over inquisitive disjunction (fig81b_ent_polarQ_not_disj).

References

• I. Ciardelli, Inquisitive Logic: Consequence and Inference in the Realm of Questions (2022)
• I. Ciardelli and F. Roelofsen, Inquisitive dynamic epistemic logic (2015)

Knowing whether (§8.2)

theorem Ciardelli2022.nec_polarQ {W : Type u_1} {A : Type u_2} [DecidableEq W] (M : Inquisitive.Model W A) (φ : Inquisitive.Formula A) : Inquisitive.support M φ.polarQ.nec = Inquisitive.support M (φ.nec.disj φ.neg.nec)

Knowing whether φ is knowing that φ or knowing that ¬φ (3b), the polar instance of support_nec_inqDisj.

@[reducible, inline]

abbrev Ciardelli2022.wonders {A : Type u_2} (μ : Inquisitive.Formula A) : Inquisitive.Formula A

The agent wonders about μ when ¬□μ ∧ ⊞μ ([CR15]; §8.3).

Equations

• Ciardelli2022.wonders μ = μ.nec.neg.conj μ.ent

Fig. 8.1: knowing, wondering and neither (§8.3)

inductive Ciardelli2022.Atom : Type

• p : Atom
• q : Atom

@[instance_reducible]

instance Ciardelli2022.instDecidableEqAtom : DecidableEq Atom

Equations

• Ciardelli2022.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ciardelli2022.instFintypeAtom : Fintype Atom

Equations

• Ciardelli2022.instFintypeAtom = { elems := { val := ↑Ciardelli2022.Atom.enumList, nodup := Ciardelli2022.Atom.enumList_nodup }, complete := Ciardelli2022.instFintypeAtom._proof_1 }

@[reducible, inline]

abbrev Ciardelli2022.p : Inquisitive.Formula Atom

p as a formula.

Equations

• Ciardelli2022.p = Inquisitive.Formula.atom Ciardelli2022.Atom.p

@[reducible, inline]

abbrev Ciardelli2022.model (inq : Finset Atom → Finset (Finset (Finset Atom))) : Inquisitive.Model (Finset Atom) Atom

model inq is the Fig. 8.1 model with inquisitive states inq. As in the book (p. 255), w_pq is the world where p and q are both true, w_p¬q the world where only p is, and so on, so a world is the set of atoms true at it.

Equations

• Ciardelli2022.model inq = { inq := inq, val := fun (a : Ciardelli2022.Atom) (w : Finset Ciardelli2022.Atom) => a ∈ w }

@[reducible, inline]

abbrev Ciardelli2022.fig81a : Inquisitive.Model (Finset Atom) Atom

In Fig. 8.1a, Σ(w) = {{w_pq, w_p¬q}}↓, so the agent knows that p and has no open issue.

Equations

• Ciardelli2022.fig81a = Ciardelli2022.model fun (x : Finset Ciardelli2022.Atom) => {{Ciardelli2022.Atom.p, Ciardelli2022.Atom.q}, {Ciardelli2022.Atom.p}}.powerset

@[reducible, inline]

abbrev Ciardelli2022.fig81b : Inquisitive.Model (Finset Atom) Atom

In Fig. 8.1b, Σ(w) = {{w_pq, w_p¬q}, {w_¬pq, w_¬p¬q}}↓, so the agent knows nothing and is interested in whether p.

Equations

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

@[reducible, inline]

abbrev Ciardelli2022.fig81c : Inquisitive.Model (Finset Atom) Atom

In Fig. 8.1c, Σ(w) = {{w_pq, w_¬pq}, {w_p¬q, w_¬p¬q}}↓, so the agent knows nothing and is interested in whether q.

Equations

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

theorem Ciardelli2022.fig81a_knows (w : Finset Atom) : {w} ∈ Inquisitive.support fig81a p.nec ∧ {w} ∈ Inquisitive.support fig81a p.polarQ.nec

In (a) the agent knows that p, hence knows whether p.

theorem Ciardelli2022.fig81b_wonders (w : Finset Atom) : {w} ∈ Inquisitive.support fig81b (wonders p.polarQ)

In (b) the agent wonders whether p.

theorem Ciardelli2022.fig81c_neither (w : Finset Atom) : {w} ∈ Inquisitive.support fig81c (p.polarQ.nec.neg.conj p.polarQ.ent.neg)

In (c) the agent neither knows whether p nor wonders about it.

theorem Ciardelli2022.fig81b_ent_polarQ_not_disj (w : Finset Atom) : {w} ∈ Inquisitive.support fig81b p.polarQ.ent ∧ {w} ∉ Inquisitive.support fig81b (p.ent.disj p.neg.ent)

⊞ does not pseudo-commute: in (b) the agent entertains whether p without entertaining p or entertaining ¬p.