Unrestricted inquisitive propositions

In the unrestricted inquisitive semantics of Ciardelli, Groenendijk and Roelofsen a proposition is a set of possibilities, sets of worlds, that need not be closed downward, so a possibility may sit inside another and still count. A proposition is inquisitive when it has two maximal possibilities, attentive when it has a non-maximal one, and informative when its possibilities do not cover every world. Having more than one possibility, interactivity in Coppock and Brochhagen's term, is Set.Nontrivial, and it is exactly being inquisitive or attentive.

The library's Question and the support semantics of Logic/Team/Inquisitive.lean are closed downward, so they identify a proposition with its maximal possibilities and lose the non-maximal ones; this file keeps the raw Set (Set W).

Main definitions

• Inquisitive.Unrestricted.IsInquisitive, IsAttentive, IsInformative.
• Inquisitive.Unrestricted.restrict: a proposition restricted to an information set.
• Inquisitive.Unrestricted.exh: exhaustification against a question.

Main results

• Inquisitive.Unrestricted.nontrivial_iff: a proposition has more than one possibility just in case it is inquisitive or attentive.

References

• [CGR09]
• [RvG10]
• [CB13]

def Inquisitive.Unrestricted.IsProposition {W : Type u_1} (P : Set (Set W)) : Prop

A proposition is a nonempty set of possibilities that omits the empty possibility unless it is the contradictory proposition {∅}.

Equations

• Inquisitive.Unrestricted.IsProposition P = (P.Nonempty ∧ (∅ ∉ P ∨ P = {∅}))

def Inquisitive.Unrestricted.IsInquisitive {W : Type u_1} (P : Set (Set W)) : Prop

A proposition is inquisitive when it has at least two maximal possibilities.

Equations

• Inquisitive.Unrestricted.IsInquisitive P = {p : Set W | Maximal (fun (x : Set W) => x ∈ P) p}.Nontrivial

def Inquisitive.Unrestricted.IsInformative {W : Type u_1} (P : Set (Set W)) : Prop

A proposition is informative when its possibilities do not cover every world.

Equations

• Inquisitive.Unrestricted.IsInformative P = (⋃₀ P ≠ Set.univ)

def Inquisitive.Unrestricted.IsAttentive {W : Type u_1} (P : Set (Set W)) : Prop

A proposition is attentive when it has a non-maximal possibility.

Equations

• Inquisitive.Unrestricted.IsAttentive P = ∃ p ∈ P, ¬Maximal (fun (x : Set W) => x ∈ P) p

theorem Inquisitive.Unrestricted.nontrivial_iff {W : Type u_1} (P : Set (Set W)) : P.Nontrivial ↔ IsInquisitive P ∨ IsAttentive P

A proposition has more than one possibility just in case it is inquisitive or attentive.

noncomputable def Inquisitive.Unrestricted.pro {W : Type u_1} (P : Set (Set W)) : Set (Set W)

The propositional closure removes the empty possibility from any proposition but {∅}.

Equations

• Inquisitive.Unrestricted.pro P = if P = {∅} then P else P \ {∅}

noncomputable def Inquisitive.Unrestricted.restrict {W : Type u_1} (P : Set (Set W)) (k : Set W) : Set (Set W)

A proposition restricted to an information set k keeps the part of each possibility that lies in k.

Equations

• Inquisitive.Unrestricted.restrict P k = Inquisitive.Unrestricted.pro ((fun (x : Set W) => k ∩ x) '' P)

def Inquisitive.Unrestricted.exh {W : Type u_1} (P Q : Set (Set W)) : Set (Set W)

Exhaustification against a question Q removes from each possibility the worlds of the alternatives it does not entail ([CB13]'s (77)).

Equations

• Inquisitive.Unrestricted.exh P Q = (fun (p : Set W) => p \ ⋃₀ {q : Set W | q ∈ Q ∧ ¬p ⊆ q}) '' P

theorem Inquisitive.Unrestricted.pro_eq_singleton {W : Type u_1} {P : Set (Set W)} {k : Set W} (hk : k ≠ ∅) (hkP : k ∈ P) (hP : P ⊆ {k, ∅}) : pro P = {k}