van Rooy (2003): Questioning to Resolve Decision Problems

Van Rooy grounds the meaning of questions in the questioner's decision problem, a prior over worlds and a utility for each action in each world. Information resolves the problem when some action is optimal in every world it leaves open. A question, a partition of the worlds, is worth the average gain in decision value from learning its answer; that theory of question value, consumed beyond this paper, is Semantics/Questions/Value.lean. A wh-question denotes the propositions that some value is among the optimal true values of its predicate, those with no more relevant true value, and this one rule yields both mention-all and mention-some readings.

Main statements

• isResolved_iff_exists_subset_optimalityRegion: information resolves the problem exactly when it lies within the worlds where one action is optimal.
• newspaper_station_resolves, newspaper_betterAnswer: in the Italian newspaper example the partial answer at least at the station resolves the problem and is a better answer than the complete one.
• questionR_entailment, bestPlace_questionR: when relevance is informativity the rule gives the mention-all partition, and the newspaper question has a mention-some meaning that Hamblin's rule misses.
• killer_byName, killer_byMask, liveIn_visit, beatles_questionR: the decision problem decides the partition, by name or by mask for Who killed spiderman?, by city or by address for Where do you live?, and by an autograph hierarchy for Which Beatles' autograph do you have?.

Implementation notes

A decision problem is a real utility on worlds and actions together with a prior measure, the actions forming a type, and questions over a finite set of worlds are Finpartitions. The relevance of a value in a world is a utility into a preorder; the paper's relation > orders answers, which for the newspaper example of section 5.2 is world-relative, the best place differing between worlds. Section 5.3 assumes the questioner most wants to resolve her problem, so for Who killed spiderman? a concept is more relevant when it resolves the problem, and for Where do you live? an answer is more relevant when it resolves the problem and, among answers alike in that, when it is less informative, the ordering of answers of section 3.1 with effort taken into account. The examples are rows of Data.Examples.VanRooy2003.

TODO

• The group-valued domain example of section 5.3, the questions (23) and (25), the individual-wise relevance condition on wh-domains of section 4.2 (Question.better_wh_of_factorsThrough covers utilities that depend only on the domain), and the argumentative value of section 5.4.

References

• [vR03b]
• [Bla53]
• [RS61]
• [GS84]
• [Ham73]
• [Rul95]
• [Alo01]
• [Mer99b]

Resolving a decision problem

def VanRooy2003.IsResolved {W : Type u} {A : Type u_1} (U : W → A → ℝ) (C : Set W) : Prop

Information C resolves the decision problem with utility U when some action is at least as good as every other in every world of C.

Equations

• VanRooy2003.IsResolved U C = ∃ (a : A), ∀ (b : A), ∀ w ∈ C, U w b ≤ U w a

def VanRooy2003.optimalityRegion {W : Type u} {A : Type u_1} (U : W → A → ℝ) (a : A) : Set W

The proposition an action induces is the set of worlds where no action is strictly better.

Equations

• VanRooy2003.optimalityRegion U a = {w : W | ∀ (b : A), U w b ≤ U w a}

theorem VanRooy2003.isResolved_iff_exists_subset_optimalityRegion {W : Type u} {A : Type u_1} (U : W → A → ℝ) (C : Set W) : IsResolved U C ↔ ∃ (a : A), C ⊆ optimalityRegion U a

Information resolves the decision problem exactly when it lies within the optimality region of some action.

theorem VanRooy2003.iUnion_optimalityRegion {W : Type u} {A : Type u_1} [Finite A] [Nonempty A] (U : W → A → ℝ) : ⋃ (a : A), optimalityRegion U a = Set.univ

Over finitely many actions every world has an optimal one, so the regions cover the worlds.

theorem VanRooy2003.pairwise_disjoint_optimalityRegion {W : Type u} {A : Type u_1} (U : W → A → ℝ) (hstrict : ∀ (w : W), ∃ (a : A), ∀ (b : A), b ≠ a → U w b < U w a) : Pairwise (Function.onFun Disjoint (optimalityRegion U))

When every world has a strictly best action the regions are pairwise disjoint, and the actions induce a partition.

The Italian newspaper

inductive VanRooy2003.NewsW : Type

The worlds of the newspaper examples are named by where to go, only the station, only the palace, or either (the paper's u, v and w).

• station : NewsW
• palace : NewsW
• both : NewsW

@[instance_reducible]

instance VanRooy2003.instDecidableEqNewsW : DecidableEq NewsW

Equations

• VanRooy2003.instDecidableEqNewsW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeNewsW : Fintype NewsW

Equations

• VanRooy2003.instFintypeNewsW = { elems := { val := ↑VanRooy2003.NewsW.enumList, nodup := VanRooy2003.NewsW.enumList_nodup }, complete := VanRooy2003.instFintypeNewsW._proof_1 }

@[instance_reducible]

instance VanRooy2003.instInhabitedNewsW : Inhabited NewsW

Equations

• VanRooy2003.instInhabitedNewsW = { default := VanRooy2003.instInhabitedNewsW.default }

@[instance_reducible]

instance VanRooy2003.instMeasurableSpaceNewsW : MeasurableSpace NewsW

Equations

• VanRooy2003.instMeasurableSpaceNewsW = ⊤

instance VanRooy2003.instDiscreteMeasurableSpaceNewsW : DiscreteMeasurableSpace NewsW

inductive VanRooy2003.Walk : Type

The actions of the newspaper example are walking to the station and walking to the palace.

• station : Walk
• palace : Walk

@[instance_reducible]

instance VanRooy2003.instDecidableEqWalk : DecidableEq Walk

Equations

• VanRooy2003.instDecidableEqWalk x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeWalk : Fintype Walk

Equations

• VanRooy2003.instFintypeWalk = { elems := { val := ↑VanRooy2003.Walk.enumList, nodup := VanRooy2003.Walk.enumList_nodup }, complete := VanRooy2003.instFintypeWalk._proof_1 }

@[instance_reducible]

instance VanRooy2003.instInhabitedWalk : Inhabited Walk

Equations

• VanRooy2003.instInhabitedWalk = { default := VanRooy2003.instInhabitedWalk.default }

def VanRooy2003.newspaper : NewsW → Walk → ℝ

Walking to a place is worth 1 where the newspaper is sold there (Examples.ex_12).

Equations

• VanRooy2003.newspaper VanRooy2003.NewsW.station VanRooy2003.Walk.station = 1
• VanRooy2003.newspaper VanRooy2003.NewsW.both VanRooy2003.Walk.station = 1
• VanRooy2003.newspaper VanRooy2003.NewsW.palace VanRooy2003.Walk.palace = 1
• VanRooy2003.newspaper VanRooy2003.NewsW.both VanRooy2003.Walk.palace = 1
• VanRooy2003.newspaper VanRooy2003.NewsW.palace VanRooy2003.Walk.station = 0
• VanRooy2003.newspaper VanRooy2003.NewsW.station VanRooy2003.Walk.palace = 0

@[reducible, inline]

noncomputable abbrev VanRooy2003.newsPrior : MeasureTheory.Measure NewsW

The worlds of the newspaper example are equiprobable.

Equations

• VanRooy2003.newsPrior = ProbabilityTheory.uniformOn Set.univ

theorem VanRooy2003.newspaper_optimalityRegions : optimalityRegion newspaper Walk.station = {NewsW.station, NewsW.both} ∧ optimalityRegion newspaper Walk.palace = {NewsW.palace, NewsW.both}

The actions induce overlapping propositions, not a partition.

theorem VanRooy2003.newspaper_station_resolves : IsResolved newspaper {NewsW.station, NewsW.both}

The mention-some answer at least at the station resolves the problem although it is only a partial answer to the partition question.

theorem VanRooy2003.newspaper_betterAnswer : Question.BetterAnswer newspaper newsPrior {NewsW.station, NewsW.both} {NewsW.station}

Taking effort into account, the mention-some answer at least at the station is a better answer than the complete answer only at the station, since both resolve the problem and the first says less.

Mention-some and mention-all from one rule

def VanRooy2003.optimalValues {W : Type u} {G : Type u_2} {R : Type u_3} [Preorder R] (P : W → Set G) (u : W → G → R) (w : W) : Set G

The optimal values of P in w are its true values for which no true value is more relevant.

Equations

• VanRooy2003.optimalValues P u w = {g : G | g ∈ P w ∧ ∀ g' ∈ P w, ¬u w g < u w g'}

theorem VanRooy2003.mem_optimalValues {W : Type u} {G : Type u_2} {R : Type u_3} [LinearOrder R] {P : W → Set G} {u : W → G → R} {w : W} {g : G} : g ∈ optimalValues P u w ↔ g ∈ P w ∧ ∀ g' ∈ P w, u w g' ≤ u w g

theorem VanRooy2003.optimalValues_eq_singleton {W : Type u} {G : Type u_2} {R : Type u_3} [Preorder R] {P : W → Set G} {u : W → G → R} {w : W} {x y : G} (hP : P w = {x, y}) (h : u w x < u w y) : optimalValues P u w = {y}

Of two true values, a strictly more relevant one is the only optimal one.

theorem VanRooy2003.optimalValues_eq_pair {W : Type u} {G : Type u_2} {R : Type u_3} [Preorder R] {P : W → Set G} {u : W → G → R} {w : W} {x y : G} (hP : P w = {x, y}) (hxy : ¬u w x < u w y) (hyx : ¬u w y < u w x) : optimalValues P u w = {x, y}

Two true values neither of which is more relevant are both optimal.

def VanRooy2003.whAnswers {W : Type u} {G : Type u_2} (P : W → Set G) : Set (Set W)

Hamblin's rule makes the answers the propositions that a value satisfies the predicate, one for each value satisfying it somewhere.

Equations

• VanRooy2003.whAnswers P = {p : Set W | ∃ (w : W), ∃ g ∈ P w, p = {v : W | g ∈ P v}}

def VanRooy2003.questionR {W : Type u} {G : Type u_2} {R : Type u_3} [Preorder R] (P : W → Set G) (u : W → G → R) : Set (Set W)

The paper's rule is Hamblin's rule applied to the optimal values, whose answers are the propositions that a value is among the optimal ones.

Equations

• VanRooy2003.questionR P u = VanRooy2003.whAnswers (VanRooy2003.optimalValues P u)

def VanRooy2003.overlapCells {W : Type u} {G : Type u_2} (op : W → Set G) : Set (Set W)

The rule of footnote 28 puts two worlds together whenever their optimal values overlap.

Equations

• VanRooy2003.overlapCells op = {p : Set W | ∃ (w : W), p = {v : W | (op w ∩ op v).Nonempty}}

theorem VanRooy2003.whAnswers_eq_image {W : Type u} {G : Type u_2} (P : W → Set G) : whAnswers P = (fun (g : G) => {v : W | g ∈ P v}) '' ⋃ (w : W), P w

Hamblin's rule collects, for each value true somewhere, the worlds where it is true.

theorem VanRooy2003.whAnswers_singleton {W : Type u} {G : Type u_2} (f : W → G) : (whAnswers fun (w : W) => {f w}) = (Setoid.ker f).classes

When the optimal value is unique in every world the rule gives the partition by that value.

theorem VanRooy2003.questionR_const {W : Type u} {G : Type u_2} {R : Type u_3} [Preorder R] (P : W → Set G) (r : R) : (questionR P fun (x : W) (x_1 : G) => r) = whAnswers P

When every value is equally relevant, the rule is Hamblin's.

theorem VanRooy2003.questionR_actions {W : Type u} {A : Type u_1} (U : W → A → ℝ) : questionR (fun (x : W) => Set.univ) U = {r : Set W | r ∈ Set.range (optimalityRegion U) ∧ r.Nonempty}

Asking which action is optimal, the rule yields the nonempty propositions the actions induce.

theorem VanRooy2003.questionR_entailment {W : Type u} {D : Type u_4} (ext : W → Set D) : (questionR (fun (w : W) => {g : Set D | g ⊆ ext w}) fun (x : W) (g : Set D) => OrderDual.toDual {v : W | g ⊆ ext v}) = (Setoid.ker ext).classes

When an answer is more relevant the more informative it is, the rule asks for the most informative true answer, and for a distributive predicate it gives the partition by the predicate's extension, the mention-all reading of [GS84].

The best place to buy the newspaper

def VanRooy2003.bestPlace : NewsW → Walk → ℝ

In the second newspaper example the paper is sold at both places in every world, and each world is named by its best place (Examples.ex_20).

Equations

• VanRooy2003.bestPlace VanRooy2003.NewsW.station VanRooy2003.Walk.station = 2
• VanRooy2003.bestPlace VanRooy2003.NewsW.palace VanRooy2003.Walk.palace = 2
• VanRooy2003.bestPlace VanRooy2003.NewsW.station VanRooy2003.Walk.palace = 1
• VanRooy2003.bestPlace VanRooy2003.NewsW.palace VanRooy2003.Walk.station = 1
• VanRooy2003.bestPlace VanRooy2003.NewsW.both x✝ = 1

theorem VanRooy2003.bestPlace_optimalValues : optimalValues (fun (x : NewsW) => Set.univ) bestPlace NewsW.station = {Walk.station} ∧ optimalValues (fun (x : NewsW) => Set.univ) bestPlace NewsW.palace = {Walk.palace} ∧ optimalValues (fun (x : NewsW) => Set.univ) bestPlace NewsW.both = Set.univ

The optimal places are the best place of each world.

theorem VanRooy2003.bestPlace_questionR : questionR (fun (x : NewsW) => Set.univ) bestPlace = {{NewsW.station, NewsW.both}, {NewsW.palace, NewsW.both}}

The rule yields the overlapping mention-some answers.

theorem VanRooy2003.bestPlace_overlapCells : overlapCells (optimalValues (fun (x : NewsW) => Set.univ) bestPlace) = {{NewsW.station, NewsW.both}, {NewsW.palace, NewsW.both}, Set.univ}

The rule of footnote 28 adds the trivial answer, which is why the paper rejects it.

theorem VanRooy2003.bestPlace_hamblin : (whAnswers fun (x : NewsW) => Set.univ) = {Set.univ}

Hamblin's rule, which ignores which places are best, yields only the trivial answer.

Degree questions

theorem VanRooy2003.optimalValues_le {W : Type u} (jump : W → ℕ) (w : W) : optimalValues (fun (w : W) => {n : ℕ | n ≤ jump w}) (fun (x : W) => id) w = {jump w}

Ranking the numbers by size, the optimal answer to How many meters can you jump? is [Rul95]'s maximum, the height you can jump (Examples.ex_18b).

theorem VanRooy2003.optimalValues_ge {W : Type u} (time : W → ℕ) (w : W) : optimalValues (fun (w : W) => {n : ℕ | time w ≤ n}) (fun (x : W) => ⇑OrderDual.toDual) w = {time w}

Ranking the numbers in reverse, the optimal answer to In how many seconds can you run the 100 meters? is the minimum (Examples.ex_19).

theorem VanRooy2003.optimalValues_gt_eq_empty {W : Type u} (jump : W → ℕ) (w : W) : optimalValues (fun (w : W) => {n : ℕ | jump w < n}) (fun (x : W) => id) w = ∅

When jumping high is better there is no best number of meters you cannot jump, so How many meters can't you jump? is undefined (Examples.ex_24).

theorem VanRooy2003.optimalValues_gt_toDual {W : Type u} (jump : W → ℕ) (w : W) : optimalValues (fun (w : W) => {n : ℕ | jump w < n}) (fun (x : W) => ⇑OrderDual.toDual) w = {jump w + 1}

With the preferences reversed, the unique optimal answer to How many meters can't you jump? is the first number of meters you cannot jump.

Granularity

def VanRooy2003.relevanceWithEffort {W : Type u} {A : Type u_1} {G : Type u_2} (U : W → A → ℝ) (P : W → Set G) : W → (g : G) → Lex (Prop × Set W)

Taking effort into account, an answer is more relevant when it resolves the decision problem, and among answers alike in that, when it is less informative.

Equations

• VanRooy2003.relevanceWithEffort U P x✝ g = toLex (VanRooy2003.IsResolved U {v : W | g ∈ P v}, {v : W | g ∈ P v})

inductive VanRooy2003.Address : Type

The worlds of Where do you live? are four addresses, two in Amsterdam and two in Utrecht as in section 3.2 (Examples.ex_21).

• amsterdam₁ : Address
• amsterdam₂ : Address
• utrecht₁ : Address
• utrecht₂ : Address

@[instance_reducible]

instance VanRooy2003.instDecidableEqAddress : DecidableEq Address

Equations

• VanRooy2003.instDecidableEqAddress x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeAddress : Fintype Address

Equations

• VanRooy2003.instFintypeAddress = { elems := { val := ↑VanRooy2003.Address.enumList, nodup := VanRooy2003.Address.enumList_nodup }, complete := VanRooy2003.instFintypeAddress._proof_1 }

instance VanRooy2003.instNonemptyAddress : Nonempty Address

inductive VanRooy2003.City : Type

A city is Amsterdam or Utrecht.

• amsterdam : City
• utrecht : City

@[instance_reducible]

instance VanRooy2003.instDecidableEqCity : DecidableEq City

Equations

• VanRooy2003.instDecidableEqCity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeCity : Fintype City

Equations

• VanRooy2003.instFintypeCity = { elems := { val := ↑VanRooy2003.City.enumList, nodup := VanRooy2003.City.enumList_nodup }, complete := VanRooy2003.instFintypeCity._proof_1 }

def VanRooy2003.Address.city : Address → City

The city of an address.

Equations

• VanRooy2003.Address.amsterdam₁.city = VanRooy2003.City.amsterdam
• VanRooy2003.Address.amsterdam₂.city = VanRooy2003.City.amsterdam
• VanRooy2003.Address.utrecht₁.city = VanRooy2003.City.utrecht
• VanRooy2003.Address.utrecht₂.city = VanRooy2003.City.utrecht

inductive VanRooy2003.Location : Type

An answer to Where do you live? names an address or a city.

• address (a : Address) : Location
• city (c : City) : Location

def VanRooy2003.livesAt (w : Address) : Set Location

In each world you live at its address and in its city.

Equations

• VanRooy2003.livesAt w = {VanRooy2003.Location.address w, VanRooy2003.Location.city w.city}

def VanRooy2003.letter (w a : Address) : ℝ

To send a letter one has to choose the address.

Equations

• VanRooy2003.letter w a = if a = w then 1 else 0

def VanRooy2003.visit (w : Address) (c : City) : ℝ

To decide on a visit one has to choose the city.

Equations

• VanRooy2003.visit w c = if c = w.city then 1 else 0

theorem VanRooy2003.liveIn_visit : questionR livesAt (relevanceWithEffort visit livesAt) = (Setoid.ker Address.city).classes

For a visit, taking effort into account, Where do you live? denotes the partition by city.

theorem VanRooy2003.liveIn_letter : questionR livesAt (relevanceWithEffort letter livesAt) = (Setoid.ker id).classes

For a letter, Where do you live? denotes the partition by address.

theorem VanRooy2003.liveIn_visit_not_pairwiseDisjoint : ¬(questionR livesAt fun (x : Address) (g : Location) => IsResolved visit {v : Address | g ∈ livesAt v}).PairwiseDisjoint id

Without effort, for a visit both the address and the city are optimal, so Where do you live? has overlapping answers and is no partition.

@[instance_reducible]

instance VanRooy2003.instMeasurableSpaceAddress : MeasurableSpace Address

Equations

• VanRooy2003.instMeasurableSpaceAddress = ⊤

instance VanRooy2003.instDiscreteMeasurableSpaceAddress : DiscreteMeasurableSpace Address

theorem VanRooy2003.liveIn_visit_better (μ : MeasureTheory.Measure Address) [MeasureTheory.IsProbabilityMeasure μ] : Question.Better visit μ (Finpartition.ofFun Address.city) ⊥

For a visit, whatever the prior, asking for the city is a better question than asking for the address: it is worth as much, since the city settles the decision, and it asks for less.

Conceptual covers

inductive VanRooy2003.SpiderW : Type

In the worlds of Who killed spiderman? John or Bill did it, wearing a blue or a green mask (Examples.ex_22).

• johnBlue : SpiderW
• johnGreen : SpiderW
• billBlue : SpiderW
• billGreen : SpiderW

@[instance_reducible]

instance VanRooy2003.instDecidableEqSpiderW : DecidableEq SpiderW

Equations

• VanRooy2003.instDecidableEqSpiderW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeSpiderW : Fintype SpiderW

Equations

• VanRooy2003.instFintypeSpiderW = { elems := { val := ↑VanRooy2003.SpiderW.enumList, nodup := VanRooy2003.SpiderW.enumList_nodup }, complete := VanRooy2003.instFintypeSpiderW._proof_1 }

inductive VanRooy2003.Concept : Type

The concepts that may identify the killer are two names and two masks.

• john : Concept
• bill : Concept
• blue : Concept
• green : Concept

@[instance_reducible]

instance VanRooy2003.instDecidableEqConcept : DecidableEq Concept

Equations

• VanRooy2003.instDecidableEqConcept x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeConcept : Fintype Concept

Equations

• VanRooy2003.instFintypeConcept = { elems := { val := ↑VanRooy2003.Concept.enumList, nodup := VanRooy2003.Concept.enumList_nodup }, complete := VanRooy2003.instFintypeConcept._proof_1 }

def VanRooy2003.killer : SpiderW → Set Concept

The concepts true of the killer in each world.

Equations

• VanRooy2003.killer VanRooy2003.SpiderW.johnBlue = {VanRooy2003.Concept.john, VanRooy2003.Concept.blue}
• VanRooy2003.killer VanRooy2003.SpiderW.johnGreen = {VanRooy2003.Concept.john, VanRooy2003.Concept.green}
• VanRooy2003.killer VanRooy2003.SpiderW.billBlue = {VanRooy2003.Concept.bill, VanRooy2003.Concept.blue}
• VanRooy2003.killer VanRooy2003.SpiderW.billGreen = {VanRooy2003.Concept.bill, VanRooy2003.Concept.green}

def VanRooy2003.byName : SpiderW → Concept → ℝ

A questioner who has to know the culprit's name decides whom to accuse.

Equations

• VanRooy2003.byName VanRooy2003.SpiderW.johnBlue VanRooy2003.Concept.john = 1
• VanRooy2003.byName VanRooy2003.SpiderW.johnGreen VanRooy2003.Concept.john = 1
• VanRooy2003.byName VanRooy2003.SpiderW.billBlue VanRooy2003.Concept.bill = 1
• VanRooy2003.byName VanRooy2003.SpiderW.billGreen VanRooy2003.Concept.bill = 1
• VanRooy2003.byName x✝¹ x✝ = 0

def VanRooy2003.byMask : SpiderW → Concept → ℝ

A questioner who has to know what the culprit looks like decides which mask to look for.

Equations

• VanRooy2003.byMask VanRooy2003.SpiderW.johnBlue VanRooy2003.Concept.blue = 1
• VanRooy2003.byMask VanRooy2003.SpiderW.johnGreen VanRooy2003.Concept.green = 1
• VanRooy2003.byMask VanRooy2003.SpiderW.billBlue VanRooy2003.Concept.blue = 1
• VanRooy2003.byMask VanRooy2003.SpiderW.billGreen VanRooy2003.Concept.green = 1
• VanRooy2003.byMask x✝¹ x✝ = 0

def VanRooy2003.nameOf : SpiderW → Concept

The culprit's name in each world.

Equations

• VanRooy2003.nameOf VanRooy2003.SpiderW.johnBlue = VanRooy2003.Concept.john
• VanRooy2003.nameOf VanRooy2003.SpiderW.johnGreen = VanRooy2003.Concept.john
• VanRooy2003.nameOf VanRooy2003.SpiderW.billBlue = VanRooy2003.Concept.bill
• VanRooy2003.nameOf VanRooy2003.SpiderW.billGreen = VanRooy2003.Concept.bill

def VanRooy2003.maskOf : SpiderW → Concept

The culprit's mask in each world.

Equations

• VanRooy2003.maskOf VanRooy2003.SpiderW.johnBlue = VanRooy2003.Concept.blue
• VanRooy2003.maskOf VanRooy2003.SpiderW.billBlue = VanRooy2003.Concept.blue
• VanRooy2003.maskOf VanRooy2003.SpiderW.johnGreen = VanRooy2003.Concept.green
• VanRooy2003.maskOf VanRooy2003.SpiderW.billGreen = VanRooy2003.Concept.green

theorem VanRooy2003.killer_byName : (questionR killer fun (x : SpiderW) (c : Concept) => IsResolved byName {v : SpiderW | c ∈ killer v}) = {{SpiderW.johnBlue, SpiderW.johnGreen}, {SpiderW.billBlue, SpiderW.billGreen}}

For a questioner who has to know the culprit's name, Who killed spiderman? denotes the partition by name, as if quantifying over the cover {John, Bill}.

theorem VanRooy2003.killer_byMask : (questionR killer fun (x : SpiderW) (c : Concept) => IsResolved byMask {v : SpiderW | c ∈ killer v}) = {{SpiderW.johnBlue, SpiderW.billBlue}, {SpiderW.johnGreen, SpiderW.billGreen}}

For a questioner who has to know what the culprit looks like, Who killed spiderman? denotes the partition by mask, as if quantifying over the cover {blue, green}.

theorem VanRooy2003.killer_anyConcept : (questionR killer fun (x : SpiderW) (x_1 : Concept) => True) = {{SpiderW.johnBlue, SpiderW.johnGreen}, {SpiderW.billBlue, SpiderW.billGreen}, {SpiderW.johnBlue, SpiderW.billBlue}, {SpiderW.johnGreen, SpiderW.billGreen}}

When any one concept resolves the problem every true concept is optimal, and Who killed spiderman? denotes four overlapping answers, one per concept.

Scalar questions

inductive VanRooy2003.Beatle : Type

The Beatles whose autographs one might have (Examples.ex_26).

• lennon : Beatle
• mccartney : Beatle
• harrison : Beatle
• starr : Beatle

@[instance_reducible]

instance VanRooy2003.instDecidableEqBeatle : DecidableEq Beatle

Equations

• VanRooy2003.instDecidableEqBeatle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanRooy2003.instFintypeBeatle : Fintype Beatle

Equations

• VanRooy2003.instFintypeBeatle = { elems := { val := ↑VanRooy2003.Beatle.enumList, nodup := VanRooy2003.Beatle.enumList_nodup }, complete := VanRooy2003.instFintypeBeatle._proof_1 }

def VanRooy2003.autographRank : Beatle → ℕ

The autographic hierarchy ranks Lennon over Harrison over Starr.

Equations

• VanRooy2003.autographRank VanRooy2003.Beatle.lennon = 3
• VanRooy2003.autographRank VanRooy2003.Beatle.harrison = 2
• VanRooy2003.autographRank VanRooy2003.Beatle.starr = 1
• VanRooy2003.autographRank VanRooy2003.Beatle.mccartney = 0

def VanRooy2003.counted (w : Finset Beatle) : Set Beatle

The autographs that count, McCartney's ignored.

Equations

• VanRooy2003.counted w = ↑(w.erase VanRooy2003.Beatle.mccartney)

theorem VanRooy2003.beatles_questionR : (questionR counted fun (x : Finset Beatle) => autographRank) = {{w : Finset Beatle | Beatle.lennon ∈ w}, {w : Finset Beatle | Beatle.harrison ∈ w ∧ Beatle.lennon ∉ w}, {w : Finset Beatle | Beatle.starr ∈ w ∧ Beatle.harrison ∉ w ∧ Beatle.lennon ∉ w}}

Ranked by the hierarchy, Which Beatles' autograph do you have? has just three resolving answers, at least a Lennon autograph, Harrison but not Lennon, and only Starr.