Heim (1994): Interrogative Semantics and Karttunen's Semantics for know

This file formalizes [Hei94b]. A [Kar77b] intension assigns each world a set of true answers; IsKarttunen is the property that every member of the answer set at w holds at w, true of the substrate's Karttunen denotation (isKarttunen_trueAnswers). Karttunen's simplified entry for know (4) has the agent believe the answer in Heim's first sense (15), the intersection of the true answers; his actual entry (5) adds that an empty answer set be believed empty; and the generalized entry (9) has the agent believe that the answer set is what it is, which makes the first clause redundant (Karttunen.simplifiedKnow_of_generalizedKnow). Believing the answer set to be what it is is believing the cell of the kernel of the intension (generalizedKnow_iff_know_ker), so the generalized analysis is [GS82]'s entry (14) on the kernel question; for whether-questions all four entries coincide (knows_whether_tfae).

The comparison for constituent questions rests on one observation: the which-intension (3) is the image of the extension of student who called under the propositional concept C, while Groenendijk and Stokhof's (13) is the kernel of the extension map, so the two agree exactly when C is injective — the paper's premise that no two individuals call in exactly the same possible worlds (ker_which). The two divergences of §7 are the two ways injectivity fails: identity with oneself (21) is constant, reducing the generalized analysis to knowing whether there are students (Karttunen.ker_which_identicalWithSelf), and living with one's actual spouse (24) identifies Bill with Sue (Spouses). Structured propositions (27) restore the agreement for every predicate, since tagging each individual with the property is injective outright (ker_whichStructured), while the unstructured answers stay recoverable (Karttunen.which_eq_image_whichStructured) though not conversely (Spouses.whichStructured_ne). The answer in the second sense (16) entails the answer in the first (ans₂_subset_ans₁), and on a Hamblin set it is the substrate's strongly exhaustive answer (ans₂_trueAnswers).

Implementation notes

Belief is w ∈ (Dox x).core p over doxastic alternatives Dox : E → SetRel W W, with no frame conditions, as the paper assumes none. Groenendijk and Stokhof's entries (13) and (14) are GroenendijkStokhof1984.whichDeDicto and GroenendijkStokhof1984.Knows, their 1982 paper being chapter II of the dissertation. Predicates are topical properties E → Set W, the substrate's trueAnswers_range shape, so the restrictorless who called (6) is the Karttunen denotation of Set.range C (Karttunen.which_univ) and the superset argument of §3 is Karttunen.which_mono. E ranges over individuals, not the groups of the paper's footnote on plurals. identicalWithSelf is the universally necessary property, which every individual has in every world. The scenarios are the paper's own two-world models: in Spouses the worlds record whether Sue is a student and whether the couples live together, and John holds the single false belief that Sue is not a student (§7). The ambiguity of answer in (17)–(20) is a row. The Feynman sentence of §4's footnote is not modelled; the general negation case is George2011.

TODO

• §6 identifies the proposition of (9) with the answer in the second sense (16), but in general only Setoid.ker q ≤ Setoid.ker (ans₁ q) holds (ker_le_ker_ans₁): on identity with oneself, ans₂ is trivial while the kernel of the intension asks whether there are students.

References

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

Karttunen intensions

def Heim1994b.IsKarttunen {W : Type u_1} (q : W → Set (Set W)) : Prop

An interrogative intension is Karttunen's, in the sense of [Kar77b], when each member of its answer set at w is true at w; the redundancy proof of §4 rests on this.

Equations

• Heim1994b.IsKarttunen q = ∀ (w : W), ∀ p ∈ q w, w ∈ p

theorem Heim1994b.isKarttunen_trueAnswers {W : Type u_1} (H : Set (Set W)) : IsKarttunen (Question.trueAnswers H)

def Heim1994b.Karttunen.whether {W : Type u_1} (φ : Set W) : W → Set (Set W)

The intension of "whether φ" is the true one of φ and its negation, (2).

Equations

• Heim1994b.Karttunen.whether φ = Question.trueAnswers {φ, φᶜ}

theorem Heim1994b.Karttunen.whether_nonempty {W : Type u_1} (φ : Set W) (w : W) : (whether φ w).Nonempty

def Heim1994b.extension {W : Type u_1} {E : Type u_2} (S C : E → Set W) (w : W) : Set E

The students who called at w, the extension behind the colon in (3) and (13).

Equations

• Heim1994b.extension S C w = {x : E | w ∈ S x ∩ C x}

def Heim1994b.Karttunen.which {W : Type u_1} {E : Type u_2} (S C : E → Set W) (w : W) : Set (Set W)

The intension of "which students called", (3), gives the propositions that x called for the students x who called, the image of the extension under the propositional concept.

Equations

• Heim1994b.Karttunen.which S C w = C '' Heim1994b.extension S C w

theorem Heim1994b.Karttunen.isKarttunen_which {W : Type u_1} {E : Type u_2} (S C : E → Set W) : IsKarttunen (which S C)

theorem Heim1994b.Karttunen.which_univ {W : Type u_1} {E : Type u_2} (C : E → Set W) : which (fun (x : E) => Set.univ) C = Question.trueAnswers (Set.range C)

Without a restrictor, "who called", (6), is the Karttunen denotation of the Hamblin set of the propositions that each individual called.

theorem Heim1994b.Karttunen.which_mono {W : Type u_1} {E : Type u_2} {S P : E → Set W} (C : E → Set W) (h : ∀ (x : E), S x ⊆ P x) (w : W) : which S C w ⊆ which P C w

Widening the restrictor widens the answer set, the superset argument of §3.

The answer in the two senses

def Heim1994b.ans₁ {W : Type u_1} (q : W → Set (Set W)) (w : W) : Set W

The answer in the first sense, (15), is the intersection of the true answers.

Equations

• Heim1994b.ans₁ q w = ⋂₀ q w

def Heim1994b.ans₂ {W : Type u_1} (q : W → Set (Set W)) (w : W) : Set W

The answer in the second sense, (16), is the proposition that the answer in the first sense is what it is.

Equations

• Heim1994b.ans₂ q w = {w' : W | Heim1994b.ans₁ q w' = Heim1994b.ans₁ q w}

theorem Heim1994b.ans₁_trueAnswers {W : Type u_1} (H : Set (Set W)) : ans₁ (Question.trueAnswers H) = Question.weakAnswer H

theorem Heim1994b.ans₂_trueAnswers {W : Type u_1} (H : Set (Set W)) (w : W) : ans₂ (Question.trueAnswers H) w = Question.strongAnswer H w

On a Hamblin set the answer in the second sense is the strongly exhaustive answer.

theorem Heim1994b.IsKarttunen.self_mem_ans₁ {W : Type u_1} {q : W → Set (Set W)} (hq : IsKarttunen q) (w : W) : w ∈ ans₁ q w

theorem Heim1994b.ker_le_ker_ans₁ {W : Type u_1} (q : W → Set (Set W)) : Setoid.ker q ≤ Setoid.ker (ans₁ q)

theorem Heim1994b.ans₂_subset_ans₁ {W : Type u_1} {q : W → Set (Set W)} (hq : IsKarttunen q) (w : W) : ans₂ q w ⊆ ans₁ q w

The answer in the second sense always entails the answer in the first (§6).

The entries for know

def Heim1994b.Karttunen.simplifiedKnow {W : Type u_1} {E : Type u_2} (Dox : E → SetRel W W) (x : E) (w : W) (q : W → Set (Set W)) : Prop

On the simplified Karttunen analysis, (4), x believes the answer in the first sense.

Equations

• Heim1994b.Karttunen.simplifiedKnow Dox x w q = (w ∈ (Dox x).core (Heim1994b.ans₁ q w))

def Heim1994b.Karttunen.know {W : Type u_1} {E : Type u_2} (Dox : E → SetRel W W) (x : E) (w : W) (q : W → Set (Set W)) : Prop

On the actual Karttunen analysis, (5), x believes the answer as in (4) and, if the answer set is empty, believes that it is empty.

Equations

• Heim1994b.Karttunen.know Dox x w q = (Heim1994b.Karttunen.simplifiedKnow Dox x w q ∧ (q w = ∅ → w ∈ (Dox x).core {w' : W | q w' = ∅}))

def Heim1994b.generalizedKnow {W : Type u_1} {E : Type u_2} (Dox : E → SetRel W W) (x : E) (w : W) {α : Type u_3} (q : W → α) : Prop

On the generalized Karttunen analysis, (9), x believes that the answer set is what it is, for answer sets of any type, as §8 applies the same entry to structured intensions.

Equations

• Heim1994b.generalizedKnow Dox x w q = (w ∈ (Dox x).core {w' : W | q w' = q w})

theorem Heim1994b.generalizedKnow_iff_know_ker {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {α : Type u_3} {q : W → α} : generalizedKnow Dox x w q ↔ GroenendijkStokhof1984.Knows (Dox x) (Setoid.ker q) w

The generalized analysis is Groenendijk and Stokhof's entry on the kernel of the intension.

theorem Heim1994b.Karttunen.simplifiedKnow_trueAnswers {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} (H : Set (Set W)) : simplifiedKnow Dox x w (Question.trueAnswers H) ↔ Question.KnowsAnswer H w (Dox x)

On a Hamblin set the simplified analysis is [Kar77b]'s meaning postulate as the substrate states it.

theorem Heim1994b.generalizedKnow_trueAnswers {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} (H : Set (Set W)) : generalizedKnow Dox x w (Question.trueAnswers H) ↔ GroenendijkStokhof1984.Knows (Dox x) (Question.partition H) w

On a Hamblin set the generalized analysis is Groenendijk and Stokhof's entry on the partition.

theorem Heim1994b.Karttunen.simplifiedKnow_of_subset {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {q q' : W → Set (Set W)} (h : q w ⊆ q' w) (hk : simplifiedKnow Dox x w q') : simplifiedKnow Dox x w q

Knowing a bigger answer set is knowing the smaller one (§3).

theorem Heim1994b.Karttunen.simplifiedKnow_of_generalizedKnow {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {q : W → Set (Set W)} (hq : IsKarttunen q) (h : generalizedKnow Dox x w q) : simplifiedKnow Dox x w q

Clause (i) of (8) is redundant given clause (ii), since an alternative with the same answer set lies in the answer in the second sense, hence in the first (§4).

theorem Heim1994b.Karttunen.know_of_generalizedKnow {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {q : W → Set (Set W)} (hq : IsKarttunen q) (h : generalizedKnow Dox x w q) : know Dox x w q

Hence (8) and (9) are equivalent, and the generalized analysis implies the actual one.

theorem Heim1994b.Karttunen.know_iff_generalizedKnow_of_eq_empty {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {q : W → Set (Set W)} (h : q w = ∅) : know Dox x w q ↔ generalizedKnow Dox x w q

With an empty answer set the actual analysis is the generalized one, (7).

Whether-questions

theorem Heim1994b.Karttunen.ker_whether {W : Type u_1} (φ : Set W) : Setoid.ker (whether φ) = Setoid.polar φ

Karttunen's whether has [GS82]'s (12) as its kernel.

theorem Heim1994b.ans₁_whether {W : Type u_1} (φ : Set W) (w : W) : ans₁ (Karttunen.whether φ) w = (Setoid.polar φ).cell w

theorem Heim1994b.knows_whether_tfae {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} (φ : Set W) : [Karttunen.simplifiedKnow Dox x w (Karttunen.whether φ), Karttunen.know Dox x w (Karttunen.whether φ), generalizedKnow Dox x w (Karttunen.whether φ), GroenendijkStokhof1984.Knows (Dox x) (Setoid.polar φ) w].TFAE

The simplified, actual, and generalized analyses and Groenendijk and Stokhof's all agree on "NP knows whether φ", the proof §4 leaves to the reader and the paper's footnote 11.

Constituent questions: Karttunen against Groenendijk and Stokhof

theorem Heim1994b.whichDeDicto_eq_ker {W : Type u_1} {E : Type u_2} (S C : E → Set W) : GroenendijkStokhof1984.whichDeDicto S C = Setoid.ker (extension S C)

Groenendijk and Stokhof's partition by which students called, (13), is the kernel of the extension map.

theorem Heim1994b.ker_which {W : Type u_1} {E : Type u_2} {S C : E → Set W} (hC : Function.Injective C) : Setoid.ker (Karttunen.which S C) = GroenendijkStokhof1984.whichDeDicto S C

When no two individuals call in exactly the same possible worlds, the kernel of Karttunen's intension is Groenendijk and Stokhof's partition, so that (10) is (11).

theorem Heim1994b.generalizedKnow_which_iff {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {S C : E → Set W} (hC : Function.Injective C) : generalizedKnow Dox x w (Karttunen.which S C) ↔ GroenendijkStokhof1984.Knows (Dox x) (GroenendijkStokhof1984.whichDeDicto S C) w

The generalized Karttunen analysis and Groenendijk and Stokhof's agree on "which students called" under the injectivity premise.

theorem Heim1994b.whichDeDicto_comm {W : Type u_1} {E : Type u_2} (S C : E → Set W) : GroenendijkStokhof1984.whichDeDicto S C = GroenendijkStokhof1984.whichDeDicto C S

"Which A are B" and "which B are A" raise the same partition, §6's neutralization.

The exhaustiveness scenario (§2)

Bill and Mary, both of them people; Bill called in every world and Mary only in the world true. In the world false, where Mary did not call, John is agnostic.

inductive Heim1994b.Exhaustiveness.Student : Type

• bill : Student
• mary : Student

def Heim1994b.Exhaustiveness.called : Student → Set Bool

Bill called in every world; Mary only in true.

Equations

• Heim1994b.Exhaustiveness.called Heim1994b.Exhaustiveness.Student.bill = Set.univ
• Heim1994b.Exhaustiveness.called Heim1994b.Exhaustiveness.Student.mary = {true}

def Heim1994b.Exhaustiveness.agnostic : Unit → SetRel Bool Bool

John's doxastic alternatives at every world are all the worlds.

Equations

• Heim1994b.Exhaustiveness.agnostic x✝ = Set.univ

theorem Heim1994b.Exhaustiveness.which_false : Karttunen.which (fun (x : Student) => Set.univ) called false = {Set.univ}

theorem Heim1994b.Exhaustiveness.singleton_true_mem_which_true : {true} ∈ Karttunen.which (fun (x : Student) => Set.univ) called true

theorem Heim1994b.Exhaustiveness.karttunen_know : Karttunen.know agnostic () false (Karttunen.which (fun (x : Student) => Set.univ) called)

The actual analysis makes (1) true at false, where Mary did not call, since the only true answer, that Bill called, is believed, and the answer set is not empty.

theorem Heim1994b.Exhaustiveness.not_generalizedKnow : ¬generalizedKnow agnostic () false (Karttunen.which (fun (x : Student) => Set.univ) called)

The generalized analysis makes (1) false there, since in the alternative true Mary called too, so the answer set differs.

theorem Heim1994b.Exhaustiveness.not_groenendijkStokhof_know : ¬GroenendijkStokhof1984.Knows (agnostic ()) (GroenendijkStokhof1984.whichDeDicto (fun (x : Student) => Set.univ) called) false

Groenendijk and Stokhof agree with the generalized analysis here.

The de dicto scenario (§3–§4)

Mary, the sole individual, called in every world but is a student only in the actual world true; John is agnostic. The generalized analysis delivers the de dicto reading: (1) comes out false because John does not know that Mary is a student, while Karttunen's entries make it true. At the other world, where there are no student callers, Karttunen's actual entry correctly blocks the entailment from "John knows who called" (6) to (1).

def Heim1994b.DeDicto.student : Unit → Set Bool

Mary is a student only in true.

Equations

• Heim1994b.DeDicto.student x✝ = {true}

def Heim1994b.DeDicto.called : Unit → Set Bool

Mary called in every world.

Equations

• Heim1994b.DeDicto.called x✝ = Set.univ

def Heim1994b.DeDicto.agnostic : Unit → SetRel Bool Bool

Equations

• Heim1994b.DeDicto.agnostic x✝ = Set.univ

theorem Heim1994b.DeDicto.karttunen_know : Karttunen.know agnostic () true (Karttunen.which student called)

Karttunen's actual analysis makes (1) true at true, where the one true answer is believed.

theorem Heim1994b.DeDicto.not_generalizedKnow : ¬generalizedKnow agnostic () true (Karttunen.which student called)

The generalized analysis makes (1) false, since in the alternative false Mary is not a student, so the answer set differs.

theorem Heim1994b.DeDicto.generalizedKnow_who : generalizedKnow agnostic () true (Karttunen.which (fun (x : Unit) => Set.univ) called)

(6) "John knows who called" stays true on the generalized analysis.

theorem Heim1994b.DeDicto.karttunen_know_who : Karttunen.know agnostic () false (Karttunen.which (fun (x : Unit) => Set.univ) called)

At false there are callers but no student callers, and (6) is true on the actual analysis.

theorem Heim1994b.DeDicto.not_karttunen_know_of_no_student : ¬Karttunen.know agnostic () false (Karttunen.which student called)

But (1) is false there on the actual analysis, since the answer set is empty and John does not believe it empty, so (6) does not entail (1).

Non-equivalence: identity with oneself (§7)

def Heim1994b.identicalWithSelf {W : Type u_1} {E : Type u_2} : E → Set W

The universally necessary property, which every individual has in every world.

Equations

• Heim1994b.identicalWithSelf x✝ = Set.univ

theorem Heim1994b.extension_identicalWithSelf {W : Type u_1} {E : Type u_2} (S : E → Set W) (w : W) : extension S identicalWithSelf w = {x : E | w ∈ S x}

theorem Heim1994b.Karttunen.which_identicalWithSelf_of_exists {W : Type u_1} {E : Type u_2} {S : E → Set W} {w : W} (h : ∃ (x : E), w ∈ S x) : which S identicalWithSelf w = {Set.univ}

theorem Heim1994b.Karttunen.which_identicalWithSelf_of_not_exists {W : Type u_1} {E : Type u_2} {S : E → Set W} {w : W} (h : ¬∃ (x : E), w ∈ S x) : which S identicalWithSelf w = ∅

theorem Heim1994b.whichDeDicto_identicalWithSelf {W : Type u_1} {E : Type u_2} (S : E → Set W) : GroenendijkStokhof1984.whichDeDicto S identicalWithSelf = Setoid.ker fun (w : W) => {x : E | w ∈ S x}

Groenendijk and Stokhof read (21) as knowing what students there are, (22).

theorem Heim1994b.Karttunen.ker_which_identicalWithSelf {W : Type u_1} {E : Type u_2} (S : E → Set W) : Setoid.ker (which S identicalWithSelf) = Setoid.polar {w : W | ∃ (x : E), w ∈ S x}

The generalized analysis reads (21) as knowing whether there are students, (23).

Two worlds with one student each, Bill in true and Mary in false; John agnostic. There are students either way, so the generalized analysis ascribes knowledge of (21) while Groenendijk and Stokhof's does not.

inductive Heim1994b.Identity.Student : Type

• bill : Student
• mary : Student

def Heim1994b.Identity.student : Student → Set Bool

Bill is the student in true, Mary in false.

Equations

• Heim1994b.Identity.student Heim1994b.Identity.Student.bill = {true}
• Heim1994b.Identity.student Heim1994b.Identity.Student.mary = {false}

def Heim1994b.Identity.agnostic : Unit → SetRel Bool Bool

Equations

• Heim1994b.Identity.agnostic x✝ = Set.univ

theorem Heim1994b.Identity.generalizedKnow_holds : generalizedKnow agnostic () true (Karttunen.which student identicalWithSelf)

theorem Heim1994b.Identity.not_groenendijkStokhof_know : ¬GroenendijkStokhof1984.Knows (agnostic ()) (GroenendijkStokhof1984.whichDeDicto student identicalWithSelf) true

Non-equivalence: living with one's actual spouse (§7)

Bill is married to Sue, and the proposition that either lives with their actual spouse is the proposition that they live together, so the two answers coincide. A world records whether Sue is a student and whether the couple live together; in the actual world both hold, and John's one false belief is that Sue is not a student.

inductive Heim1994b.Spouses.Person : Type

• bill : Person
• sue : Person

@[reducible, inline]

abbrev Heim1994b.Spouses.World : Type

A world records whether Sue is a student and whether Bill and Sue live together.

Equations

• Heim1994b.Spouses.World = (Bool × Bool)

def Heim1994b.Spouses.student : Person → Set World

Bill is a student everywhere; Sue where the first coordinate holds.

Equations

• Heim1994b.Spouses.student Heim1994b.Spouses.Person.bill = Set.univ
• Heim1994b.Spouses.student Heim1994b.Spouses.Person.sue = {w : Heim1994b.Spouses.World | w.1 = true}

def Heim1994b.Spouses.livesWithSpouse : Person → Set World

Each lives with their actual spouse exactly where they live together.

Equations

• Heim1994b.Spouses.livesWithSpouse x✝ = {w : Heim1994b.Spouses.World | w.2 = true}

def Heim1994b.Spouses.actual : World

Equations

• Heim1994b.Spouses.actual = (true, true)

def Heim1994b.Spouses.john : Unit → SetRel World World

John's only doxastic alternative is the world where Sue is not a student and they live together.

Equations

• Heim1994b.Spouses.john x✝ = {p : Heim1994b.Spouses.World × Heim1994b.Spouses.World | p.2 = (false, true)}

theorem Heim1994b.Spouses.not_injective_livesWithSpouse : ¬Function.Injective livesWithSpouse

The paper's premise fails, since Bill's and Sue's propositions coincide.

theorem Heim1994b.Spouses.extension_actual : extension student livesWithSpouse actual = Set.univ

theorem Heim1994b.Spouses.extension_alt : extension student livesWithSpouse (false, true) = {Person.bill}

theorem Heim1994b.Spouses.which_eq : Karttunen.which student livesWithSpouse (false, true) = Karttunen.which student livesWithSpouse actual

The answer sets at the actual world and at John's alternative coincide, although Sue is a student in one and not the other, (26).

theorem Heim1994b.Spouses.generalizedKnow_holds : generalizedKnow john () actual (Karttunen.which student livesWithSpouse)

The generalized analysis wrongly makes (24) true.

theorem Heim1994b.Spouses.not_groenendijkStokhof_know : ¬GroenendijkStokhof1984.Knows (john ()) (GroenendijkStokhof1984.whichDeDicto student livesWithSpouse) actual

Groenendijk and Stokhof make (24) false, (25).

Structured propositions (§8)

def Heim1994b.whichStructured {W : Type u_1} {E : Type u_2} (S C : E → Set W) (w : W) : Set (E × (E → Set W))

The structured intension, (27), pairs each student who called with the property of calling.

Equations

• Heim1994b.whichStructured S C w = (fun (x : E) => (x, C)) '' Heim1994b.extension S C w

theorem Heim1994b.ker_whichStructured {W : Type u_1} {E : Type u_2} (S C : E → Set W) : Setoid.ker (whichStructured S C) = GroenendijkStokhof1984.whichDeDicto S C

(28) is Groenendijk and Stokhof's (11) for any predicate, since tagging each individual with the property is injective whatever the property.

theorem Heim1994b.generalizedKnow_whichStructured_iff {W : Type u_1} {E : Type u_2} {Dox : E → SetRel W W} {x : E} {w : W} {S C : E → Set W} : generalizedKnow Dox x w (whichStructured S C) ↔ GroenendijkStokhof1984.Knows (Dox x) (GroenendijkStokhof1984.whichDeDicto S C) w

With structured answers the generalized analysis is Groenendijk and Stokhof's, with no premise on the predicate.

theorem Heim1994b.Karttunen.which_eq_image_whichStructured {W : Type u_1} {E : Type u_2} (S C : E → Set W) (w : W) : which S C w = (fun (p : E × (E → Set W)) => p.2 p.1) '' whichStructured S C w

The unstructured answers are always recoverable from the structured intension.

theorem Heim1994b.Identity.not_generalizedKnow_structured : ¬generalizedKnow agnostic () true (whichStructured student identicalWithSelf)

On (21), structured answers withdraw the knowledge ascription.

theorem Heim1994b.Spouses.not_generalizedKnow_structured : ¬generalizedKnow john () actual (whichStructured student livesWithSpouse)

On (24), structured answers withdraw the knowledge ascription.

theorem Heim1994b.Spouses.whichStructured_ne : whichStructured student livesWithSpouse (false, true) ≠ whichStructured student livesWithSpouse actual

The converse fails, since the structured intensions differ where the unstructured ones coincide.