George (2011): Question Embedding and the Semantics of Answers

George builds a question from an abstract, the extension at each world of a property of the things a wh-phrase ranges over. The question operator gives its mention-some answers and, composed with an exhaustivity operator, its strongly exhaustive answers, the fibers of the abstract; a responsive predicate holds of a question when it holds of some answer. Against weak exhaustivity, the strongly exhaustive answers of a question and its negation coincide because complementation is a bijection of extensions, and knowing one settles the other only for an agent who knows the domain, so Maggie knows who was admitted but not who wasn't is consistent on strong readings. Against reducibility, question-embedding know depends on belief as well as knowledge, and George's twin relations theory derives both uses of a responsive predicate from a pair of an existential and a universal relation to propositions.

Main statements

• classes_partition_mentionSome: the cells of the partition are the strongly exhaustive answers other than the contradiction.
• negation_generalization, restricted_compl_subsingleton_iff: a question and its negation have the same strongly exhaustive answers, and with a restrictor outside the negation knowing one settles the other exactly when the domain is known.
• reducible_iff_exists, reducible_embed: a reducible predicate is one computed from the answers and the propositions it holds of, as every reductive account is.
• TwinRelations.exists_proposition_of_question, TwinRelations.question_of_forall_proposition, TwinRelations.question_singleton: the linking results of the twin relations theory.
• Newspaper.know_not_reducible, know_question_stronglyExhaustive_iff: know is not reducible, but on strongly exhaustive answers it is knowing the true answer.
• rows_predicted: the dissertation's truth judgments in its scenarios.

Implementation notes

Abstracts are functions W → Set τ from worlds to extensions, and answer sets are Set (Set W). George takes knowledge and belief as primitives; the scenarios model belief by doxastic states and knowledge as true belief, and only factivity is used in general. His ignorare (101b) drops the existential conjunct that the twin relations rule yields, so the two agree on nonempty answer sets. In the admission scenarios the fourth candidate is Wesley of (16), and Rupert's state is Maggie's: the scenarios differ in their questions.

References

• [Geo11]
• [GS84]
• [Hei94b]
• [Kar77b]
• [Lah02]
• [Sha02b]

Answer sets from abstracts

def George2011.mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : Set (Set W)

The question operator Q (113) gives the mention-some answers of an abstract, one for each value.

Equations

• George2011.mentionSome α = Set.range fun (β : τ) => {w : W | β ∈ α w}

def George2011.stronglyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : Set (Set W)

The strongly exhaustive answers are Q applied to the abstract composed with the exhaustivity operator X (111), so they are the fibers of the abstract, and an extension no world realizes contributes the contradiction.

Equations

• George2011.stronglyExhaustive α = Set.range fun (S : Set τ) => α ⁻¹' {S}

theorem George2011.mem_mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) {p : Set W} : p ∈ mentionSome α ↔ ∃ (β : τ), {w : W | β ∈ α w} = p

theorem George2011.mem_stronglyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) {p : Set W} : p ∈ stronglyExhaustive α ↔ ∃ (S : Set τ), α ⁻¹' {S} = p

theorem George2011.strongAnswer_mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w : W) : Question.strongAnswer (mentionSome α) w = α ⁻¹' {α w}

Groenendijk and Stokhof's true strongly exhaustive answer, George's (125), is the worlds where the abstract has the same extension.

theorem George2011.weakAnswer_mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w : W) : Question.weakAnswer (mentionSome α) w = α ⁻¹' Set.Ici (α w)

The weakly exhaustive answer (130) is the worlds whose extension includes this one's.

theorem George2011.strongAnswer_mentionSome_mem {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w : W) : Question.strongAnswer (mentionSome α) w ∈ stronglyExhaustive α

theorem George2011.trueAnswers_stronglyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w : W) : Question.trueAnswers (stronglyExhaustive α) w = {Question.strongAnswer (mentionSome α) w}

Only one strongly exhaustive answer is true at a world (p. 41).

theorem George2011.partition_mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : Question.partition (mentionSome α) = Setoid.ker α

The partition (129) relates the worlds where the abstract has the same extension, so its cells partition the worlds (p. 70).

theorem George2011.classes_partition_mentionSome {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : (Question.partition (mentionSome α)).classes = stronglyExhaustive α \ {∅}

The cells of the partition (129) are the strongly exhaustive answers other than the contradiction (footnote 24).

theorem George2011.stronglyExhaustive_nonempty {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : (stronglyExhaustive α).Nonempty

theorem George2011.mentionSome_nonempty_iff {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : (mentionSome α).Nonempty ↔ Nonempty τ

theorem George2011.classes_ker_subset_stronglyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : (Setoid.ker α).classes ⊆ stronglyExhaustive α

theorem George2011.empty_mem_stronglyExhaustive_iff {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : ∅ ∈ stronglyExhaustive α ↔ ¬Function.Surjective α

The contradiction is a strongly exhaustive answer exactly when some extension is realized in no world, the dissertation's (128).

def George2011.weaklyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : Set (Set W)

The weakly exhaustive answers (131) are the weak answers of the worlds.

Equations

• George2011.weaklyExhaustive α = Set.range (Question.weakAnswer (George2011.mentionSome α))

theorem George2011.isStrongestTrueAnswer_weaklyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w : W) : Question.IsStrongestTrueAnswer (weaklyExhaustive α) w (Question.weakAnswer (mentionSome α) w)

A world's weakly exhaustive answer is the least true member of (131), not its only one.

theorem George2011.weakAnswer_mem_trueAnswers_weaklyExhaustive_iff {W : Type u_1} {τ : Type u_2} (α : W → Set τ) (w v : W) : Question.weakAnswer (mentionSome α) v ∈ Question.trueAnswers (weaklyExhaustive α) w ↔ α v ⊆ α w

The weak answers true at w are those of the worlds with smaller extensions, so a world has several true weakly exhaustive answers (p. 76).

Negation: (9)

theorem George2011.stronglyExhaustive_comp {W : Type u_1} {τ : Type u_2} (α : W → Set τ) {τ' : Type u_4} {f : Set τ → Set τ'} (hf : Function.Bijective f) : stronglyExhaustive (f ∘ α) = stronglyExhaustive α

Relabelling extensions bijectively leaves the strongly exhaustive answers fixed.

theorem George2011.negation_generalization {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : (stronglyExhaustive fun (w : W) => (α w)ᶜ) = stronglyExhaustive α

With negation outscoping any restrictor, a question and its negation have the same strongly exhaustive answers (9).

Partial answers: (116)–(118)

def George2011.part {W : Type u_1} : ClosureOperator (Set (Set W))

The generalized partial answers (116) close an answer set under arbitrary disjunction, which is a closure operator (117a)–(117c).

Equations

• George2011.part = ClosureOperator.ofPred (fun (P : Set (Set W)) => Set.sUnion '' 𝒫 P) (fun (P : Set (Set W)) => ∀ T ⊆ P, ⋃₀ T ∈ P) ⋯ ⋯ ⋯

theorem George2011.mem_part {W : Type u_1} {P : Set (Set W)} {q : Set W} : q ∈ part P ↔ ∃ T ⊆ P, ⋃₀ T = q

theorem George2011.mentionSome_subset_part {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : mentionSome α ⊆ part (stronglyExhaustive α)

Every mention-some answer is a partial answer to the strongly exhaustive answers (117d).

theorem George2011.empty_mem_part {W : Type u_1} (P : Set (Set W)) : ∅ ∈ part P

theorem George2011.sUnion_mem_part {W : Type u_1} (P : Set (Set W)) : ⋃₀ P ∈ part P

theorem George2011.sUnion_stronglyExhaustive {W : Type u_1} {τ : Type u_2} (α : W → Set τ) : ⋃₀ stronglyExhaustive α = Set.univ

The disjunction of all strongly exhaustive answers is the tautology (123b).

Information states knowing a strongly exhaustive answer

theorem George2011.supported_stronglyExhaustive_nonempty_iff {W : Type u_1} {τ : Type u_2} {α : W → Set τ} {σ : Set W} : (Question.supported (stronglyExhaustive α) σ).Nonempty ↔ (α '' σ).Subsingleton

A state supports a strongly exhaustive answer exactly when the extension is constant on it.

theorem George2011.supported_stronglyExhaustive_nonempty_iff_subset {W : Type u_1} {τ : Type u_2} {α : W → Set τ} (w : W) {σ : Set W} (hw : w ∈ σ) : (Question.supported (stronglyExhaustive α) σ).Nonempty ↔ σ ⊆ Question.strongAnswer (mentionSome α) w

With the actual world in the state, supporting a strongly exhaustive answer is entailing the true one (p. 41).

theorem George2011.restricted_compl_subsingleton_iff {W : Type u_1} {τ : Type u_2} {σ : Set W} {A D : W → Set τ} (hAD : ∀ (w : W), A w ⊆ D w) (hA : (A '' σ).Subsingleton) : ((fun (w : W) => D w \ A w) '' σ).Subsingleton ↔ (D '' σ).Subsingleton

With the restrictor D outside the negation and the positive extension A ⊆ D settled, the negated question is settled exactly when the domain is (p. 86).

Embedding and reducibility

def George2011.embed {W : Type u_1} {E : Type u_3} (R : Set W → E → Prop) (P : Set (Set W)) (x : E) : Prop

By the embedding rule (51) a responsive predicate holds of a question when it holds of some answer.

Equations

• George2011.embed R P x = ∃ p ∈ P, R p x

def George2011.Reducible {W : Type u_1} {E : Type u_3} (R : Set W → E → Prop) (RQ : Set (Set W) → E → Prop) : Prop

A predicate has the reducibility property (9) of chapter 4 when the questions it relates an individual to are a function of the propositions it relates it to.

Equations

• George2011.Reducible R RQ = Function.FactorsThrough (fun (x : E) => {P : Set (Set W) | RQ P x}) fun (x : E) => {p : Set W | R p x}

theorem George2011.reducible_iff {W : Type u_1} {E : Type u_3} {R : Set W → E → Prop} {RQ : Set (Set W) → E → Prop} : Reducible R RQ ↔ ∀ (a b : E), (∀ (p : Set W), R p a ↔ R p b) → ∀ (P : Set (Set W)), RQ P a ↔ RQ P b

theorem George2011.reducible_of_profile {W : Type u_1} {E : Type u_3} {R : Set W → E → Prop} (Φ : Set (Set W) → Set (Set W) → Prop) : Reducible R fun (P : Set (Set W)) (x : E) => Φ P {p : Set W | R p x}

A question relation computed from the answer set and the propositions an individual is related to is reducible, as every reductive account's is (p. 117).

theorem George2011.reducible_iff_exists {W : Type u_1} {E : Type u_3} {R : Set W → E → Prop} {RQ : Set (Set W) → E → Prop} : Reducible R RQ ↔ ∃ (Φ : Set (Set W) → Set (Set W) → Prop), ∀ (P : Set (Set W)) (x : E), RQ P x ↔ Φ P {p : Set W | R p x}

theorem George2011.reducible_embed {W : Type u_1} {E : Type u_3} {R : Set W → E → Prop} (f : Set (Set W) → Set (Set W)) : Reducible R fun (P : Set (Set W)) (x : E) => embed R (f P) x

Existential quantification over any selection of answers is reducible (p. 118), including the baseline rule and Lahiri's quantification over true answers.

theorem George2011.reducible_answer {W : Type u_1} {E : Type u_3} {R : Set W → E → Prop} (ans : Set (Set W) → Set W) : Reducible R fun (P : Set (Set W)) (x : E) => R (ans P) x

Checking the predicate against "the answer" is reducible (p. 119), whichever answer operator picks it.

Twin relations: §4.5.3

structure George2011.TwinRelations (W : Type u_4) (E : Type u_5) : Type (max u_4 u_5)

On the twin relations theory a responsive predicate's lexical entry is a pair of relations, one that some answer must bear and one that every answer must bear (p. 158).

• existential : Set W → E → Prop
• universal : Set W → E → Prop

def George2011.TwinRelations.question {W : Type u_1} {E : Type u_3} (R : TwinRelations W E) (P : Set (Set W)) (x : E) : Prop

The question-embedding use (85b) relates an individual to an answer set every answer of which bears the universal relation and some answer the existential one.

Equations

• R.question P x = ((∀ p ∈ P, R.universal p x) ∧ ∃ p ∈ P, R.existential p x)

def George2011.TwinRelations.proposition {W : Type u_1} {E : Type u_3} (R : TwinRelations W E) (p : Set W) (x : E) : Prop

The propositional use (85a) requires both relations.

Equations

• R.proposition p x = (R.existential p x ∧ R.universal p x)

theorem George2011.TwinRelations.exists_proposition_of_question {W : Type u_1} {E : Type u_3} (R : TwinRelations W E) {P : Set (Set W)} {x : E} (h : R.question P x) : ∃ p ∈ P, R.proposition p x

Relating an individual to an answer set relates it to one of the answers (102).

theorem George2011.TwinRelations.question_of_forall_proposition {W : Type u_1} {E : Type u_3} (R : TwinRelations W E) {P : Set (Set W)} {x : E} (hP : P.Nonempty) (h : ∀ p ∈ P, R.proposition p x) : R.question P x

Relating an individual to every answer of a nonempty answer set relates it to the set (103).

@[simp]

theorem George2011.TwinRelations.question_singleton {W : Type u_1} {E : Type u_3} (R : TwinRelations W E) {p : Set W} {x : E} : R.question {p} x ↔ R.proposition p x

On a singleton the question-embedding use is the propositional use, so a clause can be embedded as the singleton of its proposition (§4.5.3.6).

theorem George2011.TwinRelations.question_of_universal_true {W : Type u_1} {E : Type u_3} {P : Set (Set W)} {x : E} {S : Set W → E → Prop} : { existential := S, universal := fun (x : Set W) (x_1 : E) => True }.question P x ↔ embed S P x

A trivial universal relation, as for be certain (98)–(99), gives back the embedding rule.

theorem George2011.TwinRelations.question_of_existential_true {W : Type u_1} {E : Type u_3} {P : Set (Set W)} {x : E} {S : Set W → E → Prop} (hP : P.Nonempty) : { existential := fun (x : Set W) (x_1 : E) => True, universal := fun (p : Set W) (x : E) => ¬S p x }.question P x ↔ ¬embed S P x

With all its content in the universal relation, as for Italian ignorare (100)–(101), a predicate denies the embedding rule for the negated relation on nonempty answer sets.

def George2011.TwinRelations.know {W : Type u_1} {E : Type u_3} (knows believes : Set W → E → Prop) (w : W) : TwinRelations W E

know (86) has knowledge as its existential relation and the truth of what is believed as its universal one.

Equations

• George2011.TwinRelations.know knows believes w = { existential := knows, universal := fun (p : Set W) (x : E) => believes p x → w ∈ p }

theorem George2011.TwinRelations.know_question {W : Type u_1} {E : Type u_3} {P : Set (Set W)} {x : E} {knows believes : Set W → E → Prop} {w : W} : (know knows believes w).question P x ↔ (∀ p ∈ P, believes p x → w ∈ p) ∧ ∃ p ∈ P, knows p x

Knowing a question is knowing some answer and believing no false one (71).

theorem George2011.TwinRelations.know_proposition {W : Type u_1} {E : Type u_3} {p : Set W} {x : E} {knows believes : Set W → E → Prop} {w : W} (hT : ∀ (p : Set W) (x : E), knows p x → w ∈ p) : (know knows believes w).proposition p x ↔ knows p x

As knowledge entails truth, the propositional use of know is knowledge (84).

def George2011.TwinRelations.forgot {W : Type u_1} {E : Type u_3} (forgot knew : Set W → E → Prop) : TwinRelations W E

forgot (96) has forgetting as its existential relation and the forgetting of whatever was known as its universal one.

Equations

• George2011.TwinRelations.forgot forgot knew = { existential := forgot, universal := fun (p : Set W) (x : E) => knew p x → forgot p x }

theorem George2011.know_question_stronglyExhaustive_iff {W : Type u_1} {τ : Type u_2} {E : Type u_3} (α : W → Set τ) (w : W) {σ : E → Set W} (hσ : ∀ (x : E), (σ x).Nonempty) (x : E) : (TwinRelations.know (fun (p : Set W) (x : E) => σ x ⊆ p ∧ w ∈ p) (fun (p : Set W) (x : E) => σ x ⊆ p) w).question (stronglyExhaustive α) x ↔ σ x ⊆ Question.strongAnswer (mentionSome α) w

For a believer with consistent beliefs the universal half of (71) adds nothing over strongly exhaustive answers, so knowing the question is knowing the true answer (pp. 154, 163).

The newspaper scenario (35)–(36): know is not reducible

@[reducible, inline]

abbrev George2011.Newspaper.World : Type

A world records whether Rupert can buy a newspaper at PaperWorld and at Newstopia.

Equations

• George2011.Newspaper.World = (Bool × Bool)

inductive George2011.Newspaper.Agent : Type

The two agents, Janna and Red.

• janna : Agent
• red : Agent

@[instance_reducible]

instance George2011.Newspaper.instDecidableEqAgent : DecidableEq Agent

Equations

• George2011.Newspaper.instDecidableEqAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def George2011.Newspaper.state : Agent → Set World

Each agent's state is the worlds compatible with what they believe; Janna believes the PaperWorld answer, Red also the Newstopia one (35).

Equations

• George2011.Newspaper.state George2011.Newspaper.Agent.janna = {w : George2011.Newspaper.World | w.1 = true}
• George2011.Newspaper.state George2011.Newspaper.Agent.red = {w : George2011.Newspaper.World | w.1 = true ∧ w.2 = true}

def George2011.Newspaper.actual : World

Newspapers are sold at PaperWorld only.

Equations

• George2011.Newspaper.actual = (true, false)

def George2011.Newspaper.sells (w : World) : Set Bool

Where can Rupert buy a newspaper (37) is the abstract giving the shops that sell, false for PaperWorld and true for Newstopia.

Equations

• George2011.Newspaper.sells w = {s : Bool | (if s = true then w.2 else w.1) = true}

def George2011.Newspaper.believes (p : Set World) (a : Agent) : Prop

An agent believes what their state entails.

Equations

• George2011.Newspaper.believes p a = (George2011.Newspaper.state a ⊆ p)

def George2011.Newspaper.knows (p : Set World) (a : Agent) : Prop

Knowledge as true belief, the propositional relation the scenario holds fixed.

Equations

• George2011.Newspaper.knows p a = (George2011.Newspaper.believes p a ∧ George2011.Newspaper.actual ∈ p)

@[reducible, inline]

abbrev George2011.Newspaper.know : TwinRelations World Agent

The question-embedding know of (71) and (86).

Equations

• George2011.Newspaper.know = George2011.TwinRelations.know George2011.Newspaper.knows George2011.Newspaper.believes George2011.Newspaper.actual

theorem George2011.Newspaper.mentionSome_sells : mentionSome sells = {{w : World | w.1 = true}, {w : World | w.2 = true}}

theorem George2011.Newspaper.knows_janna_iff_red (p : Set World) : knows p Agent.janna ↔ knows p Agent.red

Red and Janna know the same propositions (35a), (35c).

theorem George2011.Newspaper.janna_knows : know.question (mentionSome sells) Agent.janna

(33) is true.

theorem George2011.Newspaper.red_not_knows : ¬know.question (mentionSome sells) Agent.red

(34) is untrue, since Red believes the false Newstopia answer.

theorem George2011.Newspaper.know_not_reducible : ¬Reducible knows know.question

Two agents with the same propositional knowledge differ on the question, so know is not reducible (§4.3.1).

Admissions: §3.1

inductive George2011.Admissions.Status : Type

A candidate's status.

• notApplicant : Status
• admitted : Status
• rejected : Status
• waitlisted : Status

@[instance_reducible]

instance George2011.Admissions.instDecidableEqStatus : DecidableEq Status

Equations

• George2011.Admissions.instDecidableEqStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev George2011.Admissions.World : Type

A world assigns a status to each of four candidates, Riley, Adam, Robin and Wesley in Maggie's scenario and Anne, Red, Alex and Jonathan in Rupert's.

Equations

• George2011.Admissions.World = (Fin 4 → George2011.Admissions.Status)

def George2011.Admissions.applicant (w : World) : Set (Fin 4)

applicant, the restrictor of who in (14b)/(15b).

Equations

• George2011.Admissions.applicant w = {x : Fin 4 | w x ≠ George2011.Admissions.Status.notApplicant}

def George2011.Admissions.admitted (w : World) : Set (Fin 4)

The admitted candidates.

Equations

• George2011.Admissions.admitted w = {x : Fin 4 | w x = George2011.Admissions.Status.admitted}

def George2011.Admissions.rejected (w : World) : Set (Fin 4)

The rejected candidates.

Equations

• George2011.Admissions.rejected w = {x : Fin 4 | w x = George2011.Admissions.Status.rejected}

def George2011.Admissions.admittedApplicant (w : World) : Set (Fin 4)

Which applicants were admitted (14b), with the restrictor outside the negation.

Equations

• George2011.Admissions.admittedApplicant w = George2011.Admissions.applicant w ∩ George2011.Admissions.admitted w

def George2011.Admissions.notAdmittedApplicant (w : World) : Set (Fin 4)

Which applicants weren't admitted (15b).

Equations

• George2011.Admissions.notAdmittedApplicant w = George2011.Admissions.applicant w \ George2011.Admissions.admitted w

def George2011.Admissions.listed : Set World

The state of someone sent the complete list of admitted candidates, the first two.

Equations

• George2011.Admissions.listed = {w : George2011.Admissions.World | ∀ (x : Fin 4), w x = George2011.Admissions.Status.admitted ↔ x = 0 ∨ x = 1}

@[instance_reducible]

instance George2011.Admissions.instDecidablePredWorldMemSetListed : DecidablePred fun (x : World) => x ∈ listed

Equations

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

@[instance_reducible]

instance George2011.Admissions.instDecidablePredFinOfNatNatMemSetApplicant (w : World) : DecidablePred fun (x : Fin 4) => x ∈ applicant w

Equations

• George2011.Admissions.instDecidablePredFinOfNatNatMemSetApplicant w x = { decide := !decide (w x = George2011.Admissions.Status.notApplicant), reflects_decide := ⋯ }

@[instance_reducible]

instance George2011.Admissions.instDecidablePredFinOfNatNatMemSetAdmitted (w : World) : DecidablePred fun (x : Fin 4) => x ∈ admitted w

Equations

• George2011.Admissions.instDecidablePredFinOfNatNatMemSetAdmitted w x = George2011.Admissions.instDecidablePredFinOfNatNatMemSetAdmitted._aux_1 w x

@[instance_reducible]

instance George2011.Admissions.instDecidablePredFinOfNatNatMemSetRejected (w : World) : DecidablePred fun (x : Fin 4) => x ∈ rejected w

Equations

• George2011.Admissions.instDecidablePredFinOfNatNatMemSetRejected w x = George2011.Admissions.instDecidablePredFinOfNatNatMemSetRejected._aux_1 w x

@[instance_reducible]

instance George2011.Admissions.instDecidablePredFinOfNatNatMemSetNotAdmittedApplicant (w : World) : DecidablePred fun (x : Fin 4) => x ∈ notAdmittedApplicant w

Equations

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

theorem George2011.Admissions.admitted_subset_applicant (w : World) : admitted w ⊆ applicant w

theorem George2011.Admissions.admittedApplicant_eq (w : World) : admittedApplicant w = admitted w

theorem George2011.Admissions.admitted_image_subsingleton : (admitted '' listed).Subsingleton

theorem George2011.Admissions.applicant_image_not_subsingleton : ¬(applicant '' listed).Subsingleton

Maggie does not know who the applicants are, since Robin may or may not have applied.

theorem George2011.Admissions.maggie_knows_admitted : (Question.supported (stronglyExhaustive admittedApplicant) listed).Nonempty

(12) is true on the strongly exhaustive reading.

theorem George2011.Admissions.maggie_not_knows_notAdmitted : ¬(Question.supported (stronglyExhaustive notAdmittedApplicant) listed).Nonempty

(13) is false on the strongly exhaustive reading, by domain uncertainty.

theorem George2011.Admissions.maggie_not_knows_notAdmitted_mentionSome : ¬(Question.supported (mentionSome notAdmittedApplicant) listed).Nonempty

Nor any mention-some answer (p. 86).

theorem George2011.Admissions.rupert_knows_admitted : (Question.supported (stronglyExhaustive admitted) listed).Nonempty

Rupert knows which of his four students were admitted.

theorem George2011.Admissions.rupert_knows_compl_admitted : (Question.supported (stronglyExhaustive fun (w : World) => (admitted w)ᶜ) listed).Nonempty

Read as complementation, which weren't admitted is known too, by (9).

theorem George2011.Admissions.rupert_not_knows_rejected : ¬(Question.supported (stronglyExhaustive rejected) listed).Nonempty

Read as were rejected, which weren't admitted is not known, the complementation failure of (17)–(20).

Spector's spies (20)–(22), §4.2.3

@[reducible, inline]

abbrev George2011.Spies.World : Type

A world says which of Alex's four colleagues (Faith, William, Andrew, Robin) are spies.

Equations

• George2011.Spies.World = (Fin 4 → Bool)

def George2011.Spies.spy (w : World) : Set (Fin 4)

Which of his colleagues are spies.

Equations

• George2011.Spies.spy w = {x : Fin 4 | w x = true}

def George2011.Spies.actual : World

In the actual world of (20) Faith and William are the spies.

Equations

• George2011.Spies.actual = ![true, true, false, false]

def George2011.Spies.alex : Set World

Alex believes all four are spies.

Equations

• George2011.Spies.alex = {w : George2011.Spies.World | ∀ (x : Fin 4), w x = true}

def George2011.Spies.knows (p : Set World) : Prop

Alex knows what his state entails and is true.

Equations

• George2011.Spies.knows p = (George2011.Spies.alex ⊆ p ∧ George2011.Spies.actual ∈ p)

theorem George2011.Spies.not_knows_stronglyExhaustive : ¬∃ p ∈ stronglyExhaustive spy, knows p

(21d) is false on the strongly exhaustive reading, since Alex knows no strongly exhaustive answer.

theorem George2011.Spies.knows_weakAnswer : knows (Question.weakAnswer (mentionSome spy) actual)

Yet Alex knows the weakly exhaustive answer (21b), so a weakly exhaustive know wrongly makes (21d) true.

theorem George2011.Spies.not_know_question_mentionSome : ¬(TwinRelations.know (fun (p : Set World) (x : Unit) => knows p) (fun (p : Set World) (x : Unit) => alex ⊆ p) actual).question (mentionSome spy) ()

Spector's repair, (71) over the mention-some answers, makes (21d) false, since Alex believes the false answer that Andrew is a spy.

forgot, (44)–(46)

@[reducible, inline]

abbrev George2011.Forgot.World : Type

A world records whether Rupert can buy a newspaper at PaperWorld and at Cellulose City.

Equations

• George2011.Forgot.World = (Bool × Bool)

inductive George2011.Forgot.Agent : Type

The two agents, Janna and Red.

• janna : Agent
• red : Agent

@[instance_reducible]

instance George2011.Forgot.instDecidableEqAgent : DecidableEq Agent

Equations

• George2011.Forgot.instDecidableEqAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def George2011.Forgot.past : Agent → Set World

Both agents once knew the PaperWorld answer, and Red also the Cellulose City one (45).

Equations

• George2011.Forgot.past George2011.Forgot.Agent.janna = {w : George2011.Forgot.World | w.1 = true}
• George2011.Forgot.past George2011.Forgot.Agent.red = {w : George2011.Forgot.World | w.1 = true ∧ w.2 = true}

def George2011.Forgot.present : Agent → Set World

Janna now knows nothing about newspapers and Red still knows the Cellulose City answer.

Equations

• George2011.Forgot.present George2011.Forgot.Agent.janna = Set.univ
• George2011.Forgot.present George2011.Forgot.Agent.red = {w : George2011.Forgot.World | w.2 = true}

def George2011.Forgot.knew (p : Set World) (a : Agent) : Prop

An agent knew what their past state entailed.

Equations

• George2011.Forgot.knew p a = (George2011.Forgot.past a ⊆ p)

def George2011.Forgot.forgot (p : Set World) (a : Agent) : Prop

An agent forgot what they knew and no longer know.

Equations

• George2011.Forgot.forgot p a = (George2011.Forgot.knew p a ∧ ¬George2011.Forgot.present a ⊆ p)

def George2011.Forgot.sells (w : World) : Set Bool

Where could Rupert buy a newspaper, false for PaperWorld and true for Cellulose City.

Equations

• George2011.Forgot.sells w = {s : Bool | (if s = true then w.2 else w.1) = true}

@[reducible, inline]

abbrev George2011.Forgot.forgotEntry : TwinRelations World Agent

forgot as a twin relations pair.

Equations

• George2011.Forgot.forgotEntry = George2011.TwinRelations.forgot George2011.Forgot.forgot George2011.Forgot.knew

theorem George2011.Forgot.mentionSome_sells : mentionSome sells = {{w : World | w.1 = true}, {w : World | w.2 = true}}

theorem George2011.Forgot.janna_forgot : forgotEntry.question (mentionSome sells) Agent.janna

(44a) is true.

theorem George2011.Forgot.red_not_forgot : ¬forgotEntry.question (mentionSome sells) Agent.red

(44b) is untrue, since Red still knows the Cellulose City answer.

theorem George2011.Forgot.forgot_ne : ¬∀ (p : Set World), forgot p Agent.janna ↔ forgot p Agent.red

In a state model Red has also forgotten the conjunction (47c), so the scenario is not a counterexample to reducibility, as George anticipates (p. 138).

The dissertation's judgments

inductive George2011.Sentence : Type

The sentences whose truth in their scenarios the file settles.

• admittedKnown : Sentence
• notAdmittedKnown : Sentence
• admittedButNot : Sentence
• fourStudents : Sentence
• jannaNewspaper : Sentence
• redNewspaper : Sentence

@[instance_reducible]

instance George2011.instDecidableEqSentence : DecidableEq Sentence

Equations

• George2011.instDecidableEqSentence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance George2011.instReprSentence : Repr Sentence

Equations

• George2011.instReprSentence = { reprPrec := George2011.instReprSentence.repr }

def George2011.instReprSentence.repr : Sentence → ℕ → Std.Format

Equations

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

def George2011.Verdict : Sentence → Prop

What each sentence claims in its scenario, on the readings the dissertation assigns.

Equations

• One or more equations did not get rendered due to their size.
• George2011.Verdict George2011.Sentence.admittedKnown = (Question.supported (George2011.stronglyExhaustive George2011.Admissions.admittedApplicant) George2011.Admissions.listed).Nonempty
• George2011.Verdict George2011.Sentence.notAdmittedKnown = (Question.supported (George2011.stronglyExhaustive George2011.Admissions.notAdmittedApplicant) George2011.Admissions.listed).Nonempty
• George2011.Verdict George2011.Sentence.jannaNewspaper = George2011.Newspaper.know.question (George2011.mentionSome George2011.Newspaper.sells) George2011.Newspaper.Agent.janna
• George2011.Verdict George2011.Sentence.redNewspaper = George2011.Newspaper.know.question (George2011.mentionSome George2011.Newspaper.sells) George2011.Newspaper.Agent.red

structure George2011.Row : Type

A row's sentence and whether the dissertation judges it true.

• sentence : Sentence
• holds : Bool

@[instance_reducible]

instance George2011.instDecidableEqRow : DecidableEq Row

Equations

• George2011.instDecidableEqRow = George2011.instDecidableEqRow.decEq

def George2011.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• George2011.instDecidableEqRow.decEq { sentence := a, holds := a_1 } { sentence := b, holds := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def George2011.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance George2011.instReprRow : Repr Row

Equations

• George2011.instReprRow = { reprPrec := George2011.instReprRow.repr }

def George2011.Row.ofDatum (ex : Datum) : Option Row

The sentence and truth judgment recorded in a datum.

Equations

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

def George2011.rows : List Row

The rows of the dissertation's judgments.

Equations

• George2011.rows = List.filterMap George2011.Row.ofDatum George2011.Examples.all

theorem George2011.rows_eq : rows = [{ sentence := Sentence.admittedKnown, holds := true }, { sentence := Sentence.notAdmittedKnown, holds := false }, { sentence := Sentence.admittedButNot, holds := true }, { sentence := Sentence.fourStudents, holds := true }, { sentence := Sentence.jannaNewspaper, holds := true }, { sentence := Sentence.redNewspaper, holds := false }]

theorem George2011.rows_predicted (r : Row) : r ∈ rows → (r.holds = true ↔ Verdict r.sentence)