Groenendijk and Stokhof (1984): Studies on the Semantics of Questions

Groenendijk and Stokhof take a question to be a partition of the indices, here a Setoid. Who walks relates two indices when the same individuals walk at both (who), so that at an index it denotes the proposition true exactly where the walkers are those of that index, and whether p is the bipartition by p. Know and tell relate an individual to the proposition denoted, so to know who walks is to have one's alternatives inside the actual cell (Knows). An individual's information at an index is a set of indices compatible with what they believe inside a set compatible with what they know, which contains the index (InformationSets). A proposition answers a question for the individual when adding it to their information leaves the information inside one cell, and answers it partially when it rules out a cell.

Main statements

• Knows.mem_core: to know the answer is to know every true proposition the question decides.
• not_knows_who_of_believes: believing that someone walks who does not excludes knowing who walks.
• who_compl: who walks and who doesn't walk are one question.
• who_le_whichDeRe, whichDeRe_compl, Men.readings_independent: which man walks read de re follows from who walks and is which man doesn't walk read de re, while the de dicto reading is independent of it.
• karttunen_knows_of_knows, Walkers.karttunen_knows: Karttunen's postulate for know follows from this one, but holds of someone who wrongly believes that Suzy walks.
• InformationSets.update, InformationSets.LetsKnow.givesTrueAnswer: updating with a proposition keeps information well formed, and a proposition that lets one know an answer gives a true one.
• Figure13.letsKnow_byName: of a name and a description that answer alike on someone's beliefs, only the name, which is true, lets them know the answer.
• better_or_inter_or_union: of two compatible partial answers, one is better, or their conjunction or their disjunction is better than both.
• knowsSome_of_knows: knowing who has a pen gives the mention-some knowledge once someone has a pen.

Implementation notes

Extensions are topical properties E → Set W and attitudes are SetRel W W read through SetRel.core. Mathlib's order on Setoid is the dissertation's inclusion of questions (Setoid.le_iff_forall_classes), whose dual atoms are the bipartitions (Setoid.isCoatom_iff). The domain of individuals is fixed across indices, as the dissertation assumes in accepting (X); the update of information is classical, and giving an answer leaves out chapter IV's presupposition that the question is open. The mention-some question is Question.which. Two printed claims are corrected, the equation for the answers compatible with a conjunction (TwoCells.determined_inter_ne) and the cells that (at least) an M G's rules out in figure 15 (Figure15.indefinite_partial_false). Page numbers are the dissertation's printed ones.

TODO

• Chapter IV's indirect answers and its comparison and correctness of answers (sections 7 to 9), the pragmatic comparison of appendix 2 of chapter V, and the claim that a partial answer to a bipartition is complete (chapter IV, p. 235).
• Chapter V's linguistic answers and the pragmatic properties of terms, and chapter VI's choice readings, whose examples are rows of Data.Examples.GroenendijkStokhof1984.
• Chapter III's functional readings.

References

• [GS84]
• [GS82]
• [Kar77b]

Questions

def GroenendijkStokhof1984.extension {W : Type u_1} {E : Type u_2} (P : E → Set W) (w : W) : Set E

The extension of P at w is the set of individuals that have P there.

Equations

• GroenendijkStokhof1984.extension P w = {x : E | w ∈ P x}

@[simp]

theorem GroenendijkStokhof1984.mem_extension {W : Type u_1} {E : Type u_2} {P : E → Set W} {w : W} {x : E} : x ∈ extension P w ↔ w ∈ P x

def GroenendijkStokhof1984.who {W : Type u_1} {E : Type u_2} (P : E → Set W) : Setoid W

Who P? relates two indices at which P has the same extension (chapter II, p. 85).

Equations

• GroenendijkStokhof1984.who P = Setoid.ker (GroenendijkStokhof1984.extension P)

theorem GroenendijkStokhof1984.who_iff {W : Type u_1} {E : Type u_2} {P : E → Set W} {v w : W} : (who P) v w ↔ ∀ (x : E), v ∈ P x ↔ w ∈ P x

def GroenendijkStokhof1984.whichDeDicto {W : Type u_1} {E : Type u_2} (G P : E → Set W) : Setoid W

Which G P? read de dicto asks for the extension of G and P together (chapter II, p. 112).

Equations

• GroenendijkStokhof1984.whichDeDicto G P = GroenendijkStokhof1984.who fun (x : E) => G x ∩ P x

def GroenendijkStokhof1984.whichDeRe {W : Type u_1} {E : Type u_2} (G P : E → Set W) (w : W) : Setoid W

Which G P? read de re at w asks for the extension of P among the individuals that are G at w (chapter II, p. 114).

Equations

• GroenendijkStokhof1984.whichDeRe G P w = Setoid.ker fun (v : W) => GroenendijkStokhof1984.extension G w ∩ GroenendijkStokhof1984.extension P v

theorem GroenendijkStokhof1984.whichDeRe_iff {W : Type u_1} {E : Type u_2} {G P : E → Set W} {w v u : W} : (whichDeRe G P w) v u ↔ ∀ (x : E), w ∈ G x → (v ∈ P x ↔ u ∈ P x)

theorem GroenendijkStokhof1984.who_eq_partition {W : Type u_1} {E : Type u_2} (P : E → Set W) : who P = Question.partition (Set.range P)

Who P? is the partition of the propositions that each individual has P.

theorem GroenendijkStokhof1984.whichDeRe_eq_partition {W : Type u_1} {E : Type u_2} (G P : E → Set W) (w : W) : whichDeRe G P w = Question.partition (P '' extension G w)

Which G P? read de re at w is the partition of Karttunen's denotation of the question for the individuals that are G at w.

theorem GroenendijkStokhof1984.who_eq_iInf_polar {W : Type u_1} {E : Type u_2} (P : E → Set W) : who P = ⨅ (x : E), Setoid.polar (P x)

Who P? is the meet of the polar questions whether each individual has P (chapter IV, p. 220).

theorem GroenendijkStokhof1984.who_le_polar {W : Type u_1} {E : Type u_2} (P : E → Set W) (x : E) : who P ≤ Setoid.polar (P x)

Who walks? entails Does John walk? (chapter I, (5)).

theorem GroenendijkStokhof1984.who_decides {W : Type u_1} {E : Type u_2} (P : E → Set W) (x : E) : (who P).Decides (P x)

theorem GroenendijkStokhof1984.who_compl {W : Type u_1} {E : Type u_2} (P : E → Set W) : (who fun (x : E) => (P x)ᶜ) = who P

Who walks and who doesn't walk are one question, so that knowing the answer to either is knowing the answer to the other (chapter II, (X)).

theorem GroenendijkStokhof1984.who_le_whichDeRe {W : Type u_1} {E : Type u_2} (G P : E → Set W) (w : W) : who P ≤ whichDeRe G P w

Who walks entails which girl walks read de re (chapter II, (XI)).

theorem GroenendijkStokhof1984.whichDeRe_compl {W : Type u_1} {E : Type u_2} (G P : E → Set W) (w : W) : whichDeRe G (fun (x : E) => (P x)ᶜ) w = whichDeRe G P w

Which man walks and which man doesn't walk, both read de re, are one question (chapter II, (XII)).

theorem GroenendijkStokhof1984.whichDeDicto_inf_who_le {W : Type u_1} {E : Type u_2} (G P : E → Set W) : whichDeDicto G P ⊓ who G ≤ whichDeDicto G fun (x : E) => (P x)ᶜ

Which men walk and who are the men together entail which men don't walk, all read de dicto (chapter I, (8)).

theorem GroenendijkStokhof1984.iInf_who {W : Type u_1} {E : Type u_2} (R : E → E → Set W) : ⨅ (x : E), who (R x) = who fun (p : E × E) => R p.1 p.2

Asking of each individual whom they love is asking who loves whom, the pair-list reading of whom does everyone love over a fixed domain (chapter VI, pp. 447–449).

Knowing the answer

def GroenendijkStokhof1984.Knows {W : Type u_1} (R : SetRel W W) (Q : Setoid W) (w : W) : Prop

An individual whose alternatives at w are given by R knows the answer to Q at w when every alternative lies in the cell of w, the proposition the question denotes at w.

Equations

• GroenendijkStokhof1984.Knows R Q w = (w ∈ R.core (Q.cell w))

theorem GroenendijkStokhof1984.Knows.mono {W : Type u_1} {R : SetRel W W} {Q Q' : Setoid W} {w : W} (hQ : Q ≤ Q') (h : Knows R Q w) : Knows R Q' w

Knowing the answer to a question is knowing the answer to every question it entails.

theorem GroenendijkStokhof1984.knows_inf_iff {W : Type u_1} {R : SetRel W W} {Q Q' : Setoid W} {w : W} : Knows R (Q ⊓ Q') w ↔ Knows R Q w ∧ Knows R Q' w

theorem GroenendijkStokhof1984.Knows.mem_core {W : Type u_1} {R : SetRel W W} {Q : Setoid W} {w : W} {p : Set W} (h : Knows R Q w) (hp : Q.Decides p) (hw : w ∈ p) : w ∈ R.core p

To know the answer is to know every true proposition the question decides, which uses no factivity, so that the arguments (I) to (VII) of chapter II hold for tell as for know.

theorem GroenendijkStokhof1984.knows_who_iff {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w : W} {P : E → Set W} : Knows R (who P) w ↔ (∀ (x : E), w ∈ P x → w ∈ R.core (P x)) ∧ ∀ (x : E), w ∉ P x → w ∈ R.core (P x)ᶜ

To know who walks is to know of each walker that they walk and of each non-walker that they don't (chapter II, p. 87).

theorem GroenendijkStokhof1984.knows_nobody {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w : W} {P : E → Set W} (h : Knows R (who P) w) (hw : ∀ (x : E), w ∉ P x) : w ∈ R.core {v : W | ∀ (x : E), v ∉ P x}

Knowing who walks, when nobody walks, is knowing that nobody walks (chapter II, (XIII)).

theorem GroenendijkStokhof1984.not_knows_who_of_believes {W : Type u_1} {E : Type u_2} {w : W} {D K : SetRel W W} {P : E → Set W} {x : E} (hDK : D ⊆ K) (hD : ∃ (v : W), (w, v) ∈ D) (hbel : w ∈ D.core (P x)) (hx : w ∉ P x) : ¬Knows K (who P) w

Someone whose beliefs D are consistent and lie within their knowledge K, and who believes of a non-walker that they walk, doesn't know who walks (chapter II, (VIII) and p. 109).

Karttunen's postulate for know

theorem GroenendijkStokhof1984.karttunen_knows_of_knows {W : Type u_1} {R : SetRel W W} {w : W} {H : Set (Set W)} (h : Knows R (Question.partition H) w) : Karttunen1977.Knows w R H

Knowing the answer to a partition satisfies Karttunen's meaning postulate for know on the Hamblin set, both its clause for the true answers and its clause for an empty set of them.

theorem GroenendijkStokhof1984.knowsAnswer_of_forall_notMem {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w : W} {P : E → Set W} (h : ∀ (x : E), w ∉ P x) : Question.KnowsAnswer (Set.range P) w R

Without its clause for an empty answer set, Karttunen's postulate counts anyone as knowing who walks when nobody walks, so that it validates (XIII) only through that clause (chapter II, pp. 92–93).

Bill and Suzy at two indices. At true only Bill walks and at false both do; John cannot tell the indices apart, and believes that both walk.

inductive GroenendijkStokhof1984.Walkers.Person : Type

• bill : Person
• suzy : Person

def GroenendijkStokhof1984.Walkers.walk : Person → Set Bool

Bill walks at both indices, Suzy only at false.

Equations

• GroenendijkStokhof1984.Walkers.walk GroenendijkStokhof1984.Walkers.Person.bill = Set.univ
• GroenendijkStokhof1984.Walkers.walk GroenendijkStokhof1984.Walkers.Person.suzy = {false}

def GroenendijkStokhof1984.Walkers.john : SetRel Bool Bool

John's knowledge leaves both indices open.

Equations

• GroenendijkStokhof1984.Walkers.john = Set.univ

def GroenendijkStokhof1984.Walkers.johnBelieves : SetRel Bool Bool

John believes that Bill and Suzy walk.

Equations

• GroenendijkStokhof1984.Walkers.johnBelieves = {p : Bool × Bool | p.2 = false}

theorem GroenendijkStokhof1984.Walkers.karttunen_knows : Karttunen1977.Knows true john (Set.range walk) ∧ true ∈ johnBelieves.core (walk Person.suzy) ∧ ¬Karttunen1977.Knows true john (Set.range fun (x : Person) => (walk x)ᶜ)

Karttunen's postulate counts John as knowing who walks at true, where only Bill walks, though he believes that Suzy walks too, so that it does not validate (VIII); nor does it count him as knowing who doesn't walk, so that it does not validate (X) (chapter II, pp. 86–88).

theorem GroenendijkStokhof1984.Walkers.not_knows : ¬Knows john (who walk) true

John does not know who walks.

De dicto and de re readings

One individual at four indices, which record whether it is a man and whether it walks. The actual index is (true, false) or (true, true); each relation lists the indices John cannot exclude.

def GroenendijkStokhof1984.Men.man : Unit → Set (Bool × Bool)

It is a man at the indices (true, _).

Equations

• GroenendijkStokhof1984.Men.man x✝ = {w : Bool × Bool | w.1 = true}

def GroenendijkStokhof1984.Men.walk : Unit → Set (Bool × Bool)

It walks at the indices (_, true).

Equations

• GroenendijkStokhof1984.Men.walk x✝ = {w : Bool × Bool | w.2 = true}

def GroenendijkStokhof1984.Men.notMan : SetRel (Bool × Bool) (Bool × Bool)

John knows that it does not walk but not that it is a man, the counter-model of chapter II, p. 112.

Equations

• GroenendijkStokhof1984.Men.notMan = {p : (Bool × Bool) × Bool × Bool | p.2 = (true, false) ∨ p.2 = (false, false)}

def GroenendijkStokhof1984.Men.notManWalks : SetRel (Bool × Bool) (Bool × Bool)

John knows neither that it is a man nor that it does not walk.

Equations

• GroenendijkStokhof1984.Men.notManWalks = {p : (Bool × Bool) × Bool × Bool | p.2 = (true, false) ∨ p.2 = (false, true)}

def GroenendijkStokhof1984.Men.notManButWalks : SetRel (Bool × Bool) (Bool × Bool)

John knows that it walks but not that it is a man, the situation of chapter II, p. 89.

Equations

• GroenendijkStokhof1984.Men.notManButWalks = {p : (Bool × Bool) × Bool × Bool | p.2 = (true, true) ∨ p.2 = (false, true)}

theorem GroenendijkStokhof1984.Men.who_not_whichDeDicto : Knows notManButWalks (who walk) (true, true) ∧ ¬Knows notManButWalks (whichDeDicto man walk) (true, true) ∧ ¬who walk ≤ whichDeDicto man walk

Who walks does not entail which man walks read de dicto, since John knows the answer to the first but not to the second (chapter II, (XI)).

theorem GroenendijkStokhof1984.Men.whichDeDicto_compl_invalid : Knows notMan (whichDeDicto man walk) (true, false) ∧ Knows notMan (whichDeRe man walk (true, false)) (true, false) ∧ ¬Knows notMan (whichDeDicto man fun (x : Unit) => (walk x)ᶜ) (true, false)

Which man walks does not entail which man doesn't walk with the conclusion read de dicto, whatever the reading of the premiss (chapter II, (XII)).

theorem GroenendijkStokhof1984.Men.whichDeDicto_whichDeRe_compl_invalid : Knows notManWalks (whichDeDicto man walk) (true, false) ∧ ¬Knows notManWalks (whichDeRe man (fun (x : Unit) => (walk x)ᶜ) (true, false)) (true, false)

Which man walks read de dicto does not entail which man doesn't walk read de re (chapter II, (XII)).

theorem GroenendijkStokhof1984.Men.readings_independent : (Knows notManButWalks (whichDeRe man walk (true, true)) (true, true) ∧ ¬Knows notManButWalks (whichDeDicto man walk) (true, true)) ∧ Knows notManWalks (whichDeDicto man walk) (true, false) ∧ ¬Knows notManWalks (whichDeRe man walk (true, false)) (true, false)

The de dicto and de re readings of John knows which man walks are logically independent (chapter II, p. 90).

theorem GroenendijkStokhof1984.Men.whichDeDicto_not_le : (¬whichDeDicto man walk ≤ whichDeDicto man fun (x : Unit) => (walk x)ᶜ) ∧ ¬(whichDeDicto man fun (x : Unit) => (walk x)ᶜ) ≤ whichDeDicto man walk

Neither which men walk? nor which men don't walk? entails the other (chapter I, (7)).

Information and answers

def GroenendijkStokhof1984.compatible {W : Type u_1} (Q : Setoid W) (J : Set W) : Set (Set W)

The semantic answers to Q compatible with the information J (chapter IV, (14)).

Equations

• GroenendijkStokhof1984.compatible Q J = {X : Set W | X ∈ Q.classes ∧ (X ∩ J).Nonempty}

def GroenendijkStokhof1984.restrict {W : Type u_1} (Q : Setoid W) (J : Set W) : Set (Set W)

The partition that Q makes on J, whose blocks are the traces on J of the compatible answers (chapter IV, (15)).

Equations

• GroenendijkStokhof1984.restrict Q J = (fun (x : Set W) => x ∩ J) '' GroenendijkStokhof1984.compatible Q J

def GroenendijkStokhof1984.OffersAnswer {W : Type u_1} (Q : Setoid W) (J : Set W) : Prop

J offers an answer to Q when the partition Q makes on J has the single block J (chapter IV, (20)).

Equations

• GroenendijkStokhof1984.OffersAnswer Q J = (GroenendijkStokhof1984.restrict Q J = {J})

theorem GroenendijkStokhof1984.cell_inter_mem_restrict {W : Type u_1} {Q : Setoid W} {w : W} {J : Set W} (hw : w ∈ J) : Q.cell w ∩ J ∈ restrict Q J

theorem GroenendijkStokhof1984.offersAnswer_iff {W : Type u_1} {Q : Setoid W} {J : Set W} : OffersAnswer Q J ↔ J.Nonempty ∧ ∃ (w : W), J ⊆ Q.cell w

An information set offers an answer exactly when it is nonempty and lies inside one cell.

theorem GroenendijkStokhof1984.offersAnswer_iff_of_mem {W : Type u_1} {Q : Setoid W} {J : Set W} {i : W} (hi : i ∈ J) : OffersAnswer Q J ↔ J ⊆ Q.cell i

theorem GroenendijkStokhof1984.offersAnswer_iff_mem_fromSetoid {W : Type u_1} {Q : Setoid W} {J : Set W} : OffersAnswer Q J ↔ J.Nonempty ∧ J ∈ Question.fromSetoid Q

Information offers an answer exactly when it is nonempty and resolves the question as an inquisitive question.

theorem GroenendijkStokhof1984.OffersAnswer.anti {W : Type u_1} {Q : Setoid W} {J K : Set W} (h : OffersAnswer Q K) (hJK : J ⊆ K) (hJ : J.Nonempty) : OffersAnswer Q J

Less information offers an answer that more information offers, as long as it is not empty (chapter IV, (18)).

def GroenendijkStokhof1984.OffersTrueAnswer {W : Type u_1} (Q : Setoid W) (J : Set W) (i : W) : Prop

J offers a true answer at i when J with i added still offers an answer (chapter IV, (23)).

Equations

• GroenendijkStokhof1984.OffersTrueAnswer Q J i = GroenendijkStokhof1984.OffersAnswer Q (insert i J)

theorem GroenendijkStokhof1984.offersTrueAnswer_iff {W : Type u_1} {Q : Setoid W} {J : Set W} {i : W} : OffersTrueAnswer Q J i ↔ J ⊆ Q.cell i

theorem GroenendijkStokhof1984.offersTrueAnswer_iff_of_mem {W : Type u_1} {Q : Setoid W} {J : Set W} {i : W} (hi : i ∈ J) : OffersTrueAnswer Q J i ↔ OffersAnswer Q J

Information containing the index offers a true answer when it offers an answer.

def GroenendijkStokhof1984.CloserToAnswer {W : Type u_1} (Q : Setoid W) (J K : Set W) : Prop

J is closer to an answer to Q than K when it lies within K and fewer semantic answers are compatible with it (chapter IV, (30)).

Equations

• GroenendijkStokhof1984.CloserToAnswer Q J K = (J ⊆ K ∧ GroenendijkStokhof1984.compatible Q J ⊂ GroenendijkStokhof1984.compatible Q K)

def GroenendijkStokhof1984.GivesAccess {W : Type u_1} (Q : Setoid W) (J : Set W) (i : W) : Prop

J gives access to the true answer at i when the cell of i is compatible with it (chapter IV, (31)).

Equations

• GroenendijkStokhof1984.GivesAccess Q J i = (Q.cell i ∈ GroenendijkStokhof1984.compatible Q J)

theorem GroenendijkStokhof1984.givesAccess_iff {W : Type u_1} {Q : Setoid W} {J : Set W} {i : W} : GivesAccess Q J i ↔ (Q.cell i ∩ J).Nonempty

theorem GroenendijkStokhof1984.closerToAnswer_iff {W : Type u_1} {Q : Setoid W} {J K : Set W} : CloserToAnswer Q J K ↔ (∀ v ∈ J, v ∈ K) ∧ (∀ (w : W), (Q.cell w ∩ J).Nonempty → (Q.cell w ∩ K).Nonempty) ∧ ∃ (w : W), (Q.cell w ∩ K).Nonempty ∧ ¬(Q.cell w ∩ J).Nonempty

@[instance_reducible]

instance GroenendijkStokhof1984.instDecidableNonemptyOfFintypeOfDecidablePredMemSet_studies {W : Type u_1} [Fintype W] {s : Set W} [DecidablePred fun (x : W) => x ∈ s] : Decidable s.Nonempty

Equations

• GroenendijkStokhof1984.instDecidableNonemptyOfFintypeOfDecidablePredMemSet_studies = decidable_of_iff (∃ (v : W), v ∈ s) ⋯

@[instance_reducible]

instance GroenendijkStokhof1984.instDecidableRelROfFintypeOfDecidablePredMemSet_studies {W : Type u_1} {E : Type u_2} [Fintype E] (P : E → Set W) [(x : E) → DecidablePred fun (x_1 : W) => x_1 ∈ P x] : DecidableRel ⇑(who P)

Equations

• GroenendijkStokhof1984.instDecidableRelROfFintypeOfDecidablePredMemSet_studies P x✝¹ x✝ = decidable_of_iff (∀ (x : E), x✝¹ ∈ P x ↔ x✝ ∈ P x) ⋯

@[instance_reducible]

instance GroenendijkStokhof1984.instDecidableOffersAnswerOfFintypeOfDecidableRelROfDecidablePredMemSet {W : Type u_1} {Q : Setoid W} {J : Set W} [Fintype W] [DecidableRel ⇑Q] [DecidablePred fun (x : W) => x ∈ J] : Decidable (OffersAnswer Q J)

Equations

• GroenendijkStokhof1984.instDecidableOffersAnswerOfFintypeOfDecidableRelROfDecidablePredMemSet = decidable_of_iff (J.Nonempty ∧ ∃ (w : W), ∀ v ∈ J, Q v w) ⋯

@[instance_reducible]

instance GroenendijkStokhof1984.instDecidableCloserToAnswerOfFintypeOfDecidableRelROfDecidablePredMemSet {W : Type u_1} {Q : Setoid W} {J K : Set W} [Fintype W] [DecidableRel ⇑Q] [DecidablePred fun (x : W) => x ∈ J] [DecidablePred fun (x : W) => x ∈ K] : Decidable (CloserToAnswer Q J K)

Equations

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

@[instance_reducible]

instance GroenendijkStokhof1984.instDecidableGivesAccessOfFintypeOfDecidableRelROfDecidablePredMemSet {W : Type u_1} {Q : Setoid W} {J : Set W} {i : W} [Fintype W] [DecidableRel ⇑Q] [DecidablePred fun (x : W) => x ∈ J] : Decidable (GivesAccess Q J i)

Equations

• GroenendijkStokhof1984.instDecidableGivesAccessOfFintypeOfDecidableRelROfDecidablePredMemSet = decidable_of_iff (Q.cell i ∩ J).Nonempty ⋯

structure GroenendijkStokhof1984.InformationSets {W : Type u_1} (i : W) : Type u_1

An individual's information at the index i consists of the indices compatible with what they believe, a nonempty set, among those compatible with what they know, which contain i (chapter IV, (21)).

• doxastic : Set W

  The indices compatible with what the individual believes.

• epistemic : Set W

  The indices compatible with what the individual knows.

• doxastic_subset : self.doxastic ⊆ self.epistemic
• doxastic_nonempty : self.doxastic.Nonempty
• mem_epistemic : i ∈ self.epistemic

def GroenendijkStokhof1984.InformationSets.HasAnswer {W : Type u_1} {i : W} (S : InformationSets i) (Q : Setoid W) : Prop

The individual has an answer when their beliefs offer one (chapter IV, (24)).

Equations

• S.HasAnswer Q = GroenendijkStokhof1984.OffersAnswer Q S.doxastic

def GroenendijkStokhof1984.InformationSets.HasTrueAnswer {W : Type u_1} {i : W} (S : InformationSets i) (Q : Setoid W) : Prop

The individual has a true answer when their beliefs offer a true one.

Equations

• S.HasTrueAnswer Q = GroenendijkStokhof1984.OffersTrueAnswer Q S.doxastic i

def GroenendijkStokhof1984.InformationSets.KnowsAnswer {W : Type u_1} {i : W} (S : InformationSets i) (Q : Setoid W) : Prop

The individual knows an answer when their knowledge offers one.

Equations

• S.KnowsAnswer Q = GroenendijkStokhof1984.OffersAnswer Q S.epistemic

theorem GroenendijkStokhof1984.InformationSets.knowsAnswer_iff {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} : S.KnowsAnswer Q ↔ S.epistemic ⊆ Q.cell i

theorem GroenendijkStokhof1984.InformationSets.offersTrueAnswer_epistemic_iff {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} : OffersTrueAnswer Q S.epistemic i ↔ S.KnowsAnswer Q

The individual's knowledge offers a true answer exactly when it offers an answer.

theorem GroenendijkStokhof1984.InformationSets.KnowsAnswer.hasTrueAnswer {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} (h : S.KnowsAnswer Q) : S.HasTrueAnswer Q

To know an answer is to have a true one (chapter IV, p. 226).

theorem GroenendijkStokhof1984.InformationSets.HasTrueAnswer.hasAnswer {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} (h : S.HasTrueAnswer Q) : S.HasAnswer Q

To have a true answer is to have an answer (chapter IV, p. 226).

theorem GroenendijkStokhof1984.InformationSets.knows_iff_knowsAnswer {W : Type u_1} {R : SetRel W W} {i : W} {S : InformationSets i} {Q : Setoid W} (hR : R.image {i} = S.epistemic) : Knows R Q i ↔ S.KnowsAnswer Q

Knowing the answer at i along a relation whose alternatives at i are the individual's knowledge is knowing an answer.

noncomputable def GroenendijkStokhof1984.InformationSets.update {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) : InformationSets i

Updating with P adds P to the beliefs when they are consistent with it, and to the knowledge when, further, P is true (chapter IV, (25)).

Equations

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

theorem GroenendijkStokhof1984.InformationSets.update_doxastic_of_nonempty {W : Type u_1} {i : W} {S : InformationSets i} {P : Set W} (h : (S.doxastic ∩ P).Nonempty) : (S.update P).doxastic = S.doxastic ∩ P

theorem GroenendijkStokhof1984.InformationSets.update_doxastic_of_not_nonempty {W : Type u_1} {i : W} {S : InformationSets i} {P : Set W} (h : ¬(S.doxastic ∩ P).Nonempty) : (S.update P).doxastic = S.doxastic

theorem GroenendijkStokhof1984.InformationSets.update_epistemic_of_mem {W : Type u_1} {i : W} {S : InformationSets i} {P : Set W} (hi : i ∈ P) (h : (S.doxastic ∩ P).Nonempty) : (S.update P).epistemic = S.epistemic ∩ P

theorem GroenendijkStokhof1984.InformationSets.update_epistemic_of_notMem {W : Type u_1} {i : W} {S : InformationSets i} {P : Set W} (hi : i ∉ P) : (S.update P).epistemic = S.epistemic

def GroenendijkStokhof1984.InformationSets.GivesAnswer {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) (Q : Setoid W) : Prop

P gives the individual an answer to Q when updating with it gives them one (chapter IV, (27) and (29)).

Equations

• S.GivesAnswer P Q = (S.update P).HasAnswer Q

def GroenendijkStokhof1984.InformationSets.GivesTrueAnswer {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) (Q : Setoid W) : Prop

P gives the individual a true answer when updating with it gives them a true one.

Equations

• S.GivesTrueAnswer P Q = (S.update P).HasTrueAnswer Q

def GroenendijkStokhof1984.InformationSets.LetsKnow {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) (Q : Setoid W) : Prop

P lets the individual know an answer when updating with it lets them know one.

Equations

• S.LetsKnow P Q = (S.update P).KnowsAnswer Q

theorem GroenendijkStokhof1984.InformationSets.LetsKnow.givesTrueAnswer {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} {P : Set W} (h : S.LetsKnow P Q) : S.GivesTrueAnswer P Q

What lets one know an answer gives a true answer (chapter IV, (28)).

theorem GroenendijkStokhof1984.InformationSets.GivesTrueAnswer.givesAnswer {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} {P : Set W} (h : S.GivesTrueAnswer P Q) : S.GivesAnswer P Q

What gives a true answer gives an answer (chapter IV, (28)).

def GroenendijkStokhof1984.InformationSets.GivesPartialAnswer {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) (Q : Setoid W) : Prop

P gives the individual a partial answer to Q when updating their beliefs with it brings them closer to an answer (chapter IV, (33)).

Equations

• S.GivesPartialAnswer P Q = GroenendijkStokhof1984.CloserToAnswer Q (S.update P).doxastic S.doxastic

def GroenendijkStokhof1984.InformationSets.GivesTruePartialAnswer {W : Type u_1} {i : W} (S : InformationSets i) (P : Set W) (Q : Setoid W) : Prop

P gives a true partial answer when, further, the updated beliefs still give access to the true answer (chapter IV, (32) and (33)).

Equations

• S.GivesTruePartialAnswer P Q = (S.GivesPartialAnswer P Q ∧ GroenendijkStokhof1984.GivesAccess Q (S.update P).doxastic i)

theorem GroenendijkStokhof1984.InformationSets.GivesAnswer.givesPartialAnswer {W : Type u_1} {i : W} {S : InformationSets i} {Q : Setoid W} {P : Set W} (hQ : ¬OffersAnswer Q S.doxastic) (h : S.GivesAnswer P Q) : S.GivesPartialAnswer P Q

A proposition that gives an answer to a question open on the individual's beliefs gives a partial answer (chapter IV, p. 235).

Figure 13 of chapter IV

Two individuals, 0 and 1. An index records which of them is the F, a property true of exactly one individual, and which of them G. At the actual index 1 is the F and only 0 G's. The individual believes, wrongly, that 0 is the F, and knows, rightly, that exactly one individual G's.

@[reducible, inline]

abbrev GroenendijkStokhof1984.Figure13.Index : Type

An index records who is the F and who G's.

Equations

• GroenendijkStokhof1984.Figure13.Index = (Fin 2 × Finset (Fin 2))

@[reducible, inline]

abbrev GroenendijkStokhof1984.Figure13.whoGs : Setoid Index

Who G's?

Equations

• GroenendijkStokhof1984.Figure13.whoGs = GroenendijkStokhof1984.who fun (a : Fin 2) => {w : GroenendijkStokhof1984.Figure13.Index | a ∈ w.2}

@[reducible, inline]

abbrev GroenendijkStokhof1984.Figure13.whoIsTheF : Setoid Index

Who is the F?

Equations

• GroenendijkStokhof1984.Figure13.whoIsTheF = GroenendijkStokhof1984.who fun (a : Fin 2) => {w : GroenendijkStokhof1984.Figure13.Index | w.1 = a}

theorem GroenendijkStokhof1984.Figure13.whoGs_iff {v w : Index} : whoGs v w ↔ v.2 = w.2

theorem GroenendijkStokhof1984.Figure13.whoIsTheF_iff {v w : Index} : whoIsTheF v w ↔ v.1 = w.1

def GroenendijkStokhof1984.Figure13.actual : Index

The actual index.

Equations

• GroenendijkStokhof1984.Figure13.actual = (1, {0})

def GroenendijkStokhof1984.Figure13.info : InformationSets actual

The individual's information at the actual index.

Equations

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

def GroenendijkStokhof1984.Figure13.byName : Set Index

That 0 is the one who G's, an answer that names the individual.

Equations

• GroenendijkStokhof1984.Figure13.byName = {w : GroenendijkStokhof1984.Figure13.Index | w.2 = {0}}

def GroenendijkStokhof1984.Figure13.byDescription : Set Index

That the F is the one who G's, an answer that describes the individual.

Equations

• GroenendijkStokhof1984.Figure13.byDescription = {w : GroenendijkStokhof1984.Figure13.Index | w.2 = {w.1}}

def GroenendijkStokhof1984.Figure13.ifAnyoneThenTheF : Set Index

That if anyone G's, the F does.

Equations

• GroenendijkStokhof1984.Figure13.ifAnyoneThenTheF = {w : GroenendijkStokhof1984.Figure13.Index | w.2.Nonempty → w.1 ∈ w.2}

def GroenendijkStokhof1984.Figure13.nobody : Set Index

That nobody G's.

Equations

• GroenendijkStokhof1984.Figure13.nobody = {w : GroenendijkStokhof1984.Figure13.Index | w.2 = ∅}

def GroenendijkStokhof1984.Figure13.everybody : Set Index

That everybody G's.

Equations

• GroenendijkStokhof1984.Figure13.everybody = {w : GroenendijkStokhof1984.Figure13.Index | w.2 = Finset.univ}

theorem GroenendijkStokhof1984.Figure13.not_offersAnswer : ¬OffersAnswer whoGs info.doxastic ∧ ¬OffersAnswer whoGs info.epistemic

The question who G's is open on the individual's beliefs and on their knowledge.

theorem GroenendijkStokhof1984.Figure13.hasAnswer_whoIsTheF : info.HasAnswer whoIsTheF ∧ ¬info.HasTrueAnswer whoIsTheF

The individual has an answer to who is the F, but not a true one.

theorem GroenendijkStokhof1984.Figure13.independent : (byName ∩ byDescription).Nonempty ∧ (byName \ byDescription).Nonempty ∧ (byDescription \ byName).Nonempty ∧ (byNameᶜ ∩ byDescriptionᶜ).Nonempty

The two answers are logically independent, each combination of their truth values holding at some index.

theorem GroenendijkStokhof1984.Figure13.doxastic_inter_eq {P : Set Index} (h₀ : (0, {0}) ∈ P) (h₁ : (0, {1}) ∉ P) : info.doxastic ∩ P = {(0, {0})}

An answer true at (0, {0}) and false at (0, {1}) leaves the individual's beliefs only (0, {0}).

theorem GroenendijkStokhof1984.Figure13.doxastic_inter_byName : info.doxastic ∩ byName = {(0, {0})}

theorem GroenendijkStokhof1984.Figure13.doxastic_inter_byDescription : info.doxastic ∩ byDescription = {(0, {0})}

theorem GroenendijkStokhof1984.Figure13.pragmatically_equivalent : info.doxastic ∩ byName = info.doxastic ∩ byDescription

The two answers are equivalent on the individual's beliefs.

theorem GroenendijkStokhof1984.Figure13.givesTrueAnswer : info.GivesTrueAnswer byName whoGs ∧ info.GivesTrueAnswer byDescription whoGs

Both answers give the individual a true answer to who G's.

theorem GroenendijkStokhof1984.Figure13.letsKnow_byName : info.LetsKnow byName whoGs ∧ ¬info.LetsKnow byDescription whoGs

Only the answer by name lets the individual know who G's, since the description is false at the actual index and so does not reach their knowledge.

theorem GroenendijkStokhof1984.Figure13.givesTrueAnswer_ifAnyoneThenTheF : info.GivesTrueAnswer ifAnyoneThenTheF whoGs

The much weaker answer that if anyone G's the F does already gives a true answer.

theorem GroenendijkStokhof1984.Figure13.not_givesAnswer_nobody_everybody : ¬info.GivesAnswer nobody whoGs ∧ ¬info.GivesAnswer everybody whoGs

That nobody G's and that everybody G's are incompatible with the individual's beliefs, so neither gives an answer.

Figure 15 of chapter IV

Three individuals, 0 and 1 the M's and 2 the only F; an index is the set of individuals who G there. The individual believes that someone but not everyone G's, and only 2 G's at the actual index.

@[reducible, inline]

abbrev GroenendijkStokhof1984.Figure15.Index : Type

An index records who G's.

Equations

• GroenendijkStokhof1984.Figure15.Index = Finset (Fin 3)

def GroenendijkStokhof1984.Figure15.G (x : Fin 3) : Set Index

The proposition that x G's.

Equations

• GroenendijkStokhof1984.Figure15.G x = {w : GroenendijkStokhof1984.Figure15.Index | x ∈ w}

@[instance_reducible]

instance GroenendijkStokhof1984.Figure15.instDecidablePredIndexMemSetG (x : Fin 3) : DecidablePred fun (x_1 : Index) => x_1 ∈ G x

Equations

• GroenendijkStokhof1984.Figure15.instDecidablePredIndexMemSetG x w = GroenendijkStokhof1984.Figure15.instDecidablePredIndexMemSetG._aux_1 x w

def GroenendijkStokhof1984.Figure15.actual : Index

The actual index.

Equations

• GroenendijkStokhof1984.Figure15.actual = {2}

def GroenendijkStokhof1984.Figure15.someNotAll : Set Index

The indices at which someone but not everyone G's.

Equations

• GroenendijkStokhof1984.Figure15.someNotAll = {w : GroenendijkStokhof1984.Figure15.Index | w ≠ ∅ ∧ w ≠ Finset.univ}

@[instance_reducible]

instance GroenendijkStokhof1984.Figure15.instDecidablePredIndexMemSetSomeNotAll : DecidablePred fun (x : Index) => x ∈ someNotAll

Equations

• GroenendijkStokhof1984.Figure15.instDecidablePredIndexMemSetSomeNotAll w = { decide := decide (w ≠ ∅) && decide (w ≠ Finset.univ), reflects_decide := ⋯ }

def GroenendijkStokhof1984.Figure15.info : InformationSets actual

The individual's information at the actual index, with the same beliefs and knowledge.

Equations

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

theorem GroenendijkStokhof1984.Figure15.info_doxastic : info.doxastic = someNotAll

theorem GroenendijkStokhof1984.Figure15.update_doxastic {P : Set Index} (h : (someNotAll ∩ P).Nonempty) : (info.update P).doxastic = someNotAll ∩ P

theorem GroenendijkStokhof1984.Figure15.conditional_true_partial : info.GivesTruePartialAnswer {w : Index | 0 ∈ w → 1 ∈ w} (who G)

That if 0 G's then 1 does gives a true partial answer.

theorem GroenendijkStokhof1984.Figure15.exhaustive_indefinite_partial_false : info.GivesPartialAnswer {w : Index | ∃ (x : Fin 3), x ≠ 2 ∧ w = {x}} (who G) ∧ ¬GivesAccess (who G) (info.update {w : Index | ∃ (x : Fin 3), x ≠ 2 ∧ w = {x}}).doxastic actual

That the one who G's is an M gives a partial answer that is not true.

theorem GroenendijkStokhof1984.Figure15.indefinite_partial_false : info.GivesPartialAnswer {w : Index | 0 ∈ w ∨ 1 ∈ w} (who G) ∧ ¬GivesAccess (who G) (info.update {w : Index | 0 ∈ w ∨ 1 ∈ w}).doxastic actual

That at least an M G's gives a partial answer that is not true. It rules out of the beliefs only the actual cell, where only 2 G's, where the text says it rules out the cells where nobody and where only 1 G's (p. 236).

theorem GroenendijkStokhof1984.Figure15.exhaustive_indefinite_complete_true : info.GivesTrueAnswer {w : Index | w = {2}} (who G)

That the one who G's is an F gives a complete true answer.

Comparing answers, appendix 2 of chapter V

def GroenendijkStokhof1984.determined {W : Type u_1} (Q : Setoid W) (P : Set W) : Set W

The union of the semantic answers to Q compatible with P (chapter V, appendix 2, (1)).

Equations

• GroenendijkStokhof1984.determined Q P = ⋃₀ GroenendijkStokhof1984.compatible Q P

def GroenendijkStokhof1984.GivesPartialSemanticAnswer {W : Type u_1} (P : Set W) (Q : Setoid W) : Prop

P gives a partial semantic answer to Q when it is compatible with some but not all of its answers (chapter V, appendix 2, (2)).

Equations

• GroenendijkStokhof1984.GivesPartialSemanticAnswer P Q = (GroenendijkStokhof1984.determined Q P ≠ ∅ ∧ GroenendijkStokhof1984.determined Q P ≠ Set.univ)

def GroenendijkStokhof1984.MoreInformative {W : Type u_1} (Q : Setoid W) (P₁ P₂ : Set W) : Prop

P₁ is a more informative answer than P₂ when it is compatible with fewer answers (chapter V, appendix 2, (11)).

Equations

• GroenendijkStokhof1984.MoreInformative Q P₁ P₂ = (GroenendijkStokhof1984.determined Q P₁ ⊂ GroenendijkStokhof1984.determined Q P₂)

def GroenendijkStokhof1984.MoreStandard {W : Type u_1} (Q : Setoid W) (P₁ P₂ : Set W) : Prop

Of two equally informative answers, the weaker is the more standard (chapter V, appendix 2, (12)).

Equations

• GroenendijkStokhof1984.MoreStandard Q P₁ P₂ = (GroenendijkStokhof1984.determined Q P₁ = GroenendijkStokhof1984.determined Q P₂ ∧ P₂ ⊂ P₁)

def GroenendijkStokhof1984.Better {W : Type u_1} (Q : Setoid W) (P₁ P₂ : Set W) : Prop

P₁ is a quantitatively better answer than P₂ when it is more informative, or equally informative and more standard (chapter V, appendix 2, (13)).

Equations

• GroenendijkStokhof1984.Better Q P₁ P₂ = (GroenendijkStokhof1984.MoreInformative Q P₁ P₂ ∨ GroenendijkStokhof1984.MoreStandard Q P₁ P₂)

theorem GroenendijkStokhof1984.determined_mono {W : Type u_1} {Q : Setoid W} {P₁ P₂ : Set W} (h : P₁ ⊆ P₂) : determined Q P₁ ⊆ determined Q P₂

theorem GroenendijkStokhof1984.determined_union {W : Type u_1} {Q : Setoid W} (P₁ P₂ : Set W) : determined Q (P₁ ∪ P₂) = determined Q P₁ ∪ determined Q P₂

The answers compatible with a disjunction are those compatible with either disjunct (chapter V, appendix 2, (4)).

theorem GroenendijkStokhof1984.determined_inter_subset {W : Type u_1} {Q : Setoid W} (P₁ P₂ : Set W) : determined Q (P₁ ∩ P₂) ⊆ determined Q P₁ ∩ determined Q P₂

The answers compatible with a conjunction are compatible with each conjunct (chapter V, appendix 2, (3), which states an equation).

theorem GroenendijkStokhof1984.better_or_inter_or_union {W : Type u_1} {Q : Setoid W} {P₁ P₂ : Set W} (h₁ : GivesPartialSemanticAnswer P₁ Q) (h : (P₁ ∩ P₂).Nonempty) (hne : P₁ ≠ P₂) : Better Q P₁ P₂ ∨ Better Q P₂ P₁ ∨ GivesPartialSemanticAnswer (P₁ ∩ P₂) Q ∧ Better Q (P₁ ∩ P₂) P₁ ∧ Better Q (P₁ ∩ P₂) P₂ ∨ GivesPartialSemanticAnswer (P₁ ∪ P₂) Q ∧ Better Q (P₁ ∪ P₂) P₁ ∧ Better Q (P₁ ∪ P₂) P₂

Of two different compatible propositions the first of which gives a partial answer, one is better than the other, or their conjunction or their disjunction is a partial answer better than both (chapter V, appendix 2, (18), which also assumes that the second gives a partial answer).

Four indices in two cells, {0, 1} and {2, 3}.

@[reducible, inline]

abbrev GroenendijkStokhof1984.TwoCells.cells : Setoid (Fin 4)

The question whose cells are {0, 1} and {2, 3}.

Equations

• GroenendijkStokhof1984.TwoCells.cells = Setoid.ker fun (i : Fin 4) => decide (↑i < 2)

theorem GroenendijkStokhof1984.TwoCells.determined_inter_ne : determined cells ({0, 2} ∩ {1, 2}) ≠ determined cells {0, 2} ∩ determined cells {1, 2}

Each of {0, 2} and {1, 2} is compatible with both cells but their conjunction only with {2, 3}, so the answers compatible with a conjunction need not be those compatible with both conjuncts.

Mention-some knowledge, chapter VI, section 5.3

def GroenendijkStokhof1984.KnowsSome {W : Type u_1} {E : Type u_2} (R : SetRel W W) (P : E → Set W) (w : W) : Prop

Someone knows who P's on the mention-some reading when, of someone who P's, they know that they P (chapter VI, (25) and (28)).

Equations

• GroenendijkStokhof1984.KnowsSome R P w = ∃ (x : E), w ∈ P x ∧ w ∈ R.core (P x)

theorem GroenendijkStokhof1984.knowsSome_of_knows {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w : W} {P : E → Set W} {x : E} (h : Knows R (who P) w) (hx : w ∈ P x) : KnowsSome R P w

Knowing who has a pen gives the mention-some knowledge once someone has a pen (chapter VI, p. 538).

theorem GroenendijkStokhof1984.not_knowsSome {W : Type u_1} {E : Type u_2} {R : SetRel W W} {w : W} {P : E → Set W} (h : ∀ (x : E), w ∉ P x) : ¬KnowsSome R P w

When nobody has a pen, John knows who has a pen is false on its mention-some reading, even when John knows that nobody does (chapter VI, p. 538).

theorem GroenendijkStokhof1984.mem_which_of_mem_fromSetoid {W : Type u_1} {E : Type u_2} {w : W} {P : E → Set W} {s : Set W} {x : E} (hs : s ∈ Question.fromSetoid (who P)) (hw : w ∈ s) (hx : w ∈ P x) : s ∈ Question.which Set.univ P

A true complete answer to who has a pen, other than that nobody does, is a true complete answer on the mention-some reading (chapter VI, p. 538).

theorem GroenendijkStokhof1984.givesPartialSemanticAnswer_of_subset {W : Type u_1} {E : Type u_2} {w : W} {P : E → Set W} {s : Set W} {x : E} {v : W} (hs : s ⊆ P x) (hw : w ∈ s) (hv : v ∉ P x) : GivesPartialSemanticAnswer s (who P) ∧ w ∈ determined (who P) s

A true complete answer on the mention-some reading gives a true partial answer to who has a pen, as long as someone could fail to have one (chapter VI, p. 538).