Theiler, Roelofsen and Aloni (2018): A Uniform Semantics for Declarative and Interrogative Complements

This file formalizes Theiler, Roelofsen and Aloni's uniform semantics for the complements of responsive verbs such as know, verbs that embed declaratives and interrogatives alike. Both kinds of nucleus denote an inquisitive sentence meaning, a Question, and the embedding operator turns a nucleus into the function from worlds to its truthful resolutions there: the consistent resolutions that entail no answer or partial answer false at the world, Definitions 3 and 4, with the complete variant also entailing every true alternative, Definitions 5 and 6. A verb then relates the subject's information state to the truthful resolutions: know requires the state to be one of them at the world of evaluation, (33); its internal interpretation adds resolution introspection, that the state is a truthful resolution at every world it contains, (35); be certain keeps only the introspective conjunct, (50), and be right, be wrong, be surprised and care are built from the same parts, (59), (64), (68) and (72).

The false-answer sensitivity of know is the no-false-alternatives condition, not_know_of_subset, and its absence for be certain is that in the subject's own worlds her state entails no false partial answer, certain_E_iff. For declarative nuclei the truthful resolutions are the nonempty subsets of the proposition at the worlds where it is true, isTruthful_ofSet_iff, so know is factive and veridical, know_ofSet_iff, and be certain is not, certain_ofSet_iff. Fact 1 holds in general: the mention-some reading and, on partition nuclei, the strongly exhaustive reading do not distinguish the internal from the external verb, knowInt_E_iff, Ecmp_eq_E_of_isPartition. Fact 2 is that the internal verb does not distinguish the intermediate exhaustive reading of a wh-nucleus from its strongly exhaustive one, knowInt_Ecmp_nonExh_iff. Section 6's constraints are Facts 5 and 6: a c-distributive verb veridical for declaratives is veridical for interrogatives, IntVeridical.of_cDistributive, and one with the choice property veridical for interrogatives is veridical for declaratives, DeclVeridical.of_choice; know is c-distributive, cDistributive_know.

Implementation notes

Verb meanings are predicates on worlds; the paper's sentence meanings are their principal ideals, the non-inquisitive contents Question.ofSet. Presuppositional entries are trivalent propositions W → SignType. Worlds are finite where the paper assumes so, footnote 7, which gives every resolution an alternative above it. The wh-nucleus of Fact 2 is a family of answers, one per individual, with the non-exhaustive reading resolved by an answer or by there being none and the exhaustive reading the partition by the set of true answers; the answers are assumed nonempty and mutually non-entailing, the independence of the paper's diagrams. C-distributivity is stated for partition nuclei, whose decomposition is the family of their cells, which is all Facts 5 and 6 use. The examples are the rows of Data.Examples.TheilerRoelofsenAloni2018.

References

• [TRA18]
• [GS84]
• [Geo11]
• [SE15]
• [Ueg15]
• [CC16]
• [KR11]
• [EKSU17]
• [CR15]

Truthful resolutions (section 3.3)

def TheilerRoelofsenAloni2018.altUnion {W : Type u_1} (P : Question W) : Set (Set W)

The unions of alternatives of a nucleus meaning, its answers and partial answers (Definition 3).

Equations

• TheilerRoelofsenAloni2018.altUnion P = Set.sUnion '' 𝒫 P.alt

theorem TheilerRoelofsenAloni2018.mem_altUnion {W : Type u_1} {P : Question W} {q : Set W} : q ∈ altUnion P ↔ ∃ S ⊆ P.alt, ⋃₀ S = q

theorem TheilerRoelofsenAloni2018.mem_altUnion_of_mem_alt {W : Type u_1} {P : Question W} {q : Set W} (h : q ∈ P.alt) : q ∈ altUnion P

def TheilerRoelofsenAloni2018.ProvidesFalse {W : Type u_1} (P : Question W) (w : W) (p : Set W) : Prop

A resolution provides false information at a world if it entails an answer or partial answer false there.

Equations

• TheilerRoelofsenAloni2018.ProvidesFalse P w p = ∃ q ∈ TheilerRoelofsenAloni2018.altUnion P, w ∉ q ∧ p ⊆ q

structure TheilerRoelofsenAloni2018.IsTruthful {W : Type u_1} (P : Question W) (w : W) (p : Set W) : Prop

A truthful resolution is a consistent resolution providing no false information, the no-false-alternatives condition (Definition 4).

• mem : p ∈ P
• nonempty : p.Nonempty
• nfa : ¬ProvidesFalse P w p

structure TheilerRoelofsenAloni2018.IsCompleteTruthful {W : Type u_1} (P : Question W) (w : W) (p : Set W) extends TheilerRoelofsenAloni2018.IsTruthful P w p : Prop

A complete truthful resolution also entails every true alternative (Definition 5).

• mem : p ∈ P
• nonempty : p.Nonempty
• nfa : ¬ProvidesFalse P w p
• complete (q : Set W) : q ∈ P.alt → w ∈ q → p ⊆ q

def TheilerRoelofsenAloni2018.E {W : Type u_1} (P : Question W) (w : W) : Set (Set W)

The non-complete embedding operator (Definition 6).

Equations

• TheilerRoelofsenAloni2018.E P w = {p : Set W | TheilerRoelofsenAloni2018.IsTruthful P w p}

def TheilerRoelofsenAloni2018.Ecmp {W : Type u_1} (P : Question W) (w : W) : Set (Set W)

The complete embedding operator (Definition 6).

Equations

• TheilerRoelofsenAloni2018.Ecmp P w = {p : Set W | TheilerRoelofsenAloni2018.IsCompleteTruthful P w p}

theorem TheilerRoelofsenAloni2018.mem_E {W : Type u_1} {P : Question W} {w : W} {p : Set W} : p ∈ E P w ↔ IsTruthful P w p

theorem TheilerRoelofsenAloni2018.mem_Ecmp {W : Type u_1} {P : Question W} {w : W} {p : Set W} : p ∈ Ecmp P w ↔ IsCompleteTruthful P w p

theorem TheilerRoelofsenAloni2018.Ecmp_subset_E {W : Type u_1} {P : Question W} {w : W} : Ecmp P w ⊆ E P w

theorem TheilerRoelofsenAloni2018.IsTruthful.of_mem {W : Type u_1} {P : Question W} {w v : W} {p : Set W} (h : IsTruthful P w p) (hv : v ∈ p) : IsTruthful P v p

A truthful resolution is truthful at every world it contains, since there it entails nothing false.

theorem TheilerRoelofsenAloni2018.IsTruthful.mem_of_subset {W : Type u_1} {P : Question W} {w : W} {p q : Set W} (h : IsTruthful P w p) (hq : q ∈ P.alt) (hpq : p ⊆ q) : w ∈ q

An alternative entailed by a truthful resolution is true.

Declarative complements (section 3.6)

theorem TheilerRoelofsenAloni2018.altUnion_ofSet {W : Type u_1} (q : Set W) : altUnion (Question.ofSet q) = {∅, q}

theorem TheilerRoelofsenAloni2018.isTruthful_ofSet_iff {W : Type u_1} {w : W} {p q : Set W} : IsTruthful (Question.ofSet q) w p ↔ w ∈ q ∧ p ⊆ q ∧ p.Nonempty

At a world where a declarative nucleus is true its truthful resolutions are the nonempty propositions entailing it; where it is false there are none.

theorem TheilerRoelofsenAloni2018.isCompleteTruthful_ofSet_iff {W : Type u_1} {w : W} {p q : Set W} : IsCompleteTruthful (Question.ofSet q) w p ↔ IsTruthful (Question.ofSet q) w p

Every truthful resolution of a declarative complement is complete.

theorem TheilerRoelofsenAloni2018.isTruthful_ofSet_of_subset {W : Type u_1} {w : W} {p q : Set W} (h : IsTruthful (Question.ofSet q) w p) {r : Set W} (hr : r ⊆ p) (hne : r.Nonempty) : IsTruthful (Question.ofSet q) w r

The truthful resolutions of a declarative complement are downward closed among nonempty propositions.

Partition nuclei

theorem TheilerRoelofsenAloni2018.IsTruthful.exists_alt {W : Type u_1} {P : Question W} {w : W} {p : Set W} [Finite W] (h : IsTruthful P w p) : ∃ c ∈ P.alt, w ∈ c ∧ p ⊆ c

Over finitely many worlds a truthful resolution entails a true alternative.

theorem TheilerRoelofsenAloni2018.E_nonempty_iff {W : Type u_1} {P : Question W} {w : W} [Finite W] : (E P w).Nonempty ↔ w ∈ P.info

A nucleus has a truthful resolution at a world exactly when it is true there.

theorem TheilerRoelofsenAloni2018.Ecmp_eq_E_of_isPartition {W : Type u_1} {P : Question W} [Finite W] (h : P.IsPartition) : Ecmp P = E P

On a partition nucleus, whose alternatives are the cells of the strongly exhaustive reading, every truthful resolution is complete.

Responsive verbs (sections 3.4, 4.2 and 5)

def TheilerRoelofsenAloni2018.know {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) (w : W) : Prop

On its external interpretation know holds when the subject's information state is a truthful resolution at the world of evaluation (33).

Equations

• TheilerRoelofsenAloni2018.know dox f x w = (dox x w ∈ f w)

def TheilerRoelofsenAloni2018.knowInt {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) (w : W) : Prop

On its internal interpretation know holds when the subject's state is a truthful resolution at the world of evaluation and, by resolution introspection, at every world she considers possible (35).

Equations

• TheilerRoelofsenAloni2018.knowInt dox f x w = (dox x w ∈ f w ∧ ∀ v ∈ dox x w, dox x w ∈ f v)

def TheilerRoelofsenAloni2018.certain {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) (w : W) : Prop

be certain holds when the subject's state is a truthful resolution at every world she considers possible (50).

Equations

• TheilerRoelofsenAloni2018.certain dox f x w = ∀ v ∈ dox x w, dox x w ∈ f v

noncomputable def TheilerRoelofsenAloni2018.knowFactive {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) : W → SignType

know with its factivity presupposition, (43), presupposes that the nucleus is true.

Equations

• TheilerRoelofsenAloni2018.knowFactive dox f x = {w : W | (f w).Nonempty}.indicator fun (w : W) => SignType.ofProp (TheilerRoelofsenAloni2018.know dox f x w)

noncomputable def TheilerRoelofsenAloni2018.right {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) : W → SignType

be right, (59), presupposes be certain and asserts know.

Equations

• TheilerRoelofsenAloni2018.right dox f x = {w : W | TheilerRoelofsenAloni2018.certain dox f x w}.indicator fun (w : W) => SignType.ofProp (TheilerRoelofsenAloni2018.know dox f x w)

noncomputable def TheilerRoelofsenAloni2018.wrong {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) : W → SignType

be wrong, (64), presupposes that the state is a truthful resolution at some world the subject considers possible and asserts that it is none at the world of evaluation.

Equations

• TheilerRoelofsenAloni2018.wrong dox f x = {w : W | ∃ v ∈ dox x w, dox x w ∈ f v}.indicator fun (w : W) => SignType.ofProp (dox x w ∉ f w)

def TheilerRoelofsenAloni2018.surprised {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) (exp : X → W → Set W) (w : W) : Prop

be surprised holds when some maximal truthful resolution at the world of evaluation is believed but was not expected (68).

Equations

• TheilerRoelofsenAloni2018.surprised dox f x exp w = ∃ (q : Set W), Maximal (fun (x : Set W) => x ∈ f w) q ∧ dox x w ⊆ q ∧ ¬exp x w ⊆ q

noncomputable def TheilerRoelofsenAloni2018.care {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) (f : W → Set (Set W)) (x : X) (bou : X → W → Set W) : W → SignType

care, (72), presupposes truthful resolutions at the world of evaluation and at every world the subject considers possible, and asserts that some maximal truthful resolution at some world is desired or undesired.

Equations

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

theorem TheilerRoelofsenAloni2018.knowInt_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {f : W → Set (Set W)} {x : X} {w : W} : knowInt dox f x w ↔ certain dox f x w ∧ know dox f x w

The internal know is be certain together with the assertion of be right (section 5.3).

theorem TheilerRoelofsenAloni2018.know_ofSet_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {q : Set W} {w : W} : know dox (E (Question.ofSet q)) x w ↔ w ∈ q ∧ dox x w ⊆ q ∧ (dox x w).Nonempty

know of a declarative holds when the nucleus is true and the subject believes it, so know is veridical and factive for declaratives ((39) and (41)).

theorem TheilerRoelofsenAloni2018.certain_ofSet_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {q : Set W} {w : W} (hne : (dox x w).Nonempty) : certain dox (E (Question.ofSet q)) x w ↔ dox x w ⊆ q

A consistent subject is certain of a declarative exactly when she believes it, so be certain is not veridical (40).

theorem TheilerRoelofsenAloni2018.not_know_of_subset {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {q : Set W} {w : W} (hq : q ∈ altUnion P) (hw : w ∉ q) (h : dox x w ⊆ q) : ¬know dox (E P) x w

A subject believing an answer or partial answer false at the world of evaluation does not know the question, the false-answer sensitivity of (13b) and (25).

theorem TheilerRoelofsenAloni2018.certain_E_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {w : W} (hne : (dox x w).Nonempty) : certain dox (E P) x w ↔ dox x w ∈ P

A consistent subject is certain of a question exactly when her state resolves it, so be certain shows no false-answer sensitivity effects ((15) and (53)).

theorem TheilerRoelofsenAloni2018.knowInt_E_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {w : W} : knowInt dox (E P) x w ↔ know dox (E P) x w

On mention-some readings resolution introspection is automatic, so the internal and external interpretations coincide (Fact 1).

theorem TheilerRoelofsenAloni2018.knowInt_Ecmp_iff_of_isPartition {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {w : W} [Finite W] (h : P.IsPartition) : knowInt dox (Ecmp P) x w ↔ know dox (Ecmp P) x w

On strongly exhaustive readings the internal and external interpretations coincide, since on a partition nucleus the complete operator is the non-complete one (Fact 1).

theorem TheilerRoelofsenAloni2018.knowFactive_ofSet_ne_zero_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {q : Set W} {w : W} [Finite W] : knowFactive dox (E (Question.ofSet q)) x w ≠ 0 ↔ w ∈ q

The factivity presupposition of know with a declarative complement, (41).

theorem TheilerRoelofsenAloni2018.knowFactive_ne_zero_of_isPartition {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {w : W} [Finite W] (h : P.IsPartition) : knowFactive dox (E P) x w ≠ 0

With an interrogative complement, a partition nucleus, the presupposition of know is trivial.

theorem TheilerRoelofsenAloni2018.care_ofSet_ne_zero_iff {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {q : Set W} {w : W} [Finite W] (bou : X → W → Set W) : care dox (E (Question.ofSet q)) x bou w ≠ 0 ↔ w ∈ q ∧ dox x w ⊆ q

The presupposition of care with a declarative complement, (69a), is that the subject knows the nucleus.

theorem TheilerRoelofsenAloni2018.mem_info_of_surprised {W : Type u_1} {X : Type u_2} {dox : X → W → Set W} {x : X} {P : Question W} {w : W} [Finite W] {exp : X → W → Set W} (h : surprised dox (E P) x exp w) : w ∈ P.info

be surprised is veridical, since its maximal truthful resolution witnesses the truth of the nucleus (65).

Intermediate and strongly exhaustive readings (section 4, Fact 2)

def TheilerRoelofsenAloni2018.ext {W : Type u_1} {ι : Type u_3} (a : ι → Set W) (w : W) : Set ι

The individuals with the property at a world.

Equations

• TheilerRoelofsenAloni2018.ext a w = {d : ι | w ∈ a d}

def TheilerRoelofsenAloni2018.nobody {W : Type u_1} {ι : Type u_3} (a : ι → Set W) : Set W

The answer that no individual has the property.

Equations

• TheilerRoelofsenAloni2018.nobody a = ⋂ (d : ι), (a d)ᶜ

def TheilerRoelofsenAloni2018.nonExh {W : Type u_1} {ι : Type u_3} (a : ι → Set W) : Question W

The non-exhaustive reading of a wh-nucleus, resolved by establishing of some individual that it has the property, or that none has (Figure 5(b)).

Equations

• TheilerRoelofsenAloni2018.nonExh a = Question.which Set.univ fun (x : Option ι) => x.elim (TheilerRoelofsenAloni2018.nobody a) a

def TheilerRoelofsenAloni2018.exh {W : Type u_1} {ι : Type u_3} (a : ι → Set W) : Question W

The exhaustive reading, resolved by establishing exactly which individuals have the property (Figure 5(a)).

Equations

• TheilerRoelofsenAloni2018.exh a = Question.fromSetoid (Setoid.ker (TheilerRoelofsenAloni2018.ext a))

def TheilerRoelofsenAloni2018.cell {W : Type u_1} {ι : Type u_3} (a : ι → Set W) (w : W) : Set W

The cell of the exhaustive reading containing a world.

Equations

• TheilerRoelofsenAloni2018.cell a w = {v : W | TheilerRoelofsenAloni2018.ext a v = TheilerRoelofsenAloni2018.ext a w}

theorem TheilerRoelofsenAloni2018.mem_cell_iff {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w v : W} : v ∈ cell a w ↔ ∀ (d : ι), v ∈ a d ↔ w ∈ a d

theorem TheilerRoelofsenAloni2018.mem_cell_self {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} : w ∈ cell a w

theorem TheilerRoelofsenAloni2018.cell_eq_of_mem {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w v : W} (hv : v ∈ cell a w) : cell a v = cell a w

theorem TheilerRoelofsenAloni2018.cell_mem_classes {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} : cell a w ∈ (Setoid.ker (ext a)).classes

theorem TheilerRoelofsenAloni2018.mem_nonExh {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {D : Set W} : D ∈ nonExh a ↔ D = ∅ ∨ D ⊆ nobody a ∨ ∃ (d : ι), D ⊆ a d

theorem TheilerRoelofsenAloni2018.alt_nonExh {W : Type u_1} {ι : Type u_3} {a : ι → Set W} (hne : ∀ (d : ι), (a d).Nonempty) (hN : (nobody a).Nonempty) (hind : ∀ (d d' : ι), a d ⊆ a d' → d = d') : (nonExh a).alt = Set.range fun (x : Option ι) => x.elim (nobody a) a

Under independence the alternatives of the non-exhaustive reading are the answers and the answer that none holds.

theorem TheilerRoelofsenAloni2018.subset_cell_of_Ecmp_nonExh {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} {D : Set W} (hne : ∀ (d : ι), (a d).Nonempty) (hN : (nobody a).Nonempty) (hind : ∀ (d d' : ι), a d ⊆ a d' → d = d') (hw : D ∈ Ecmp (nonExh a) w) (h : ∀ v ∈ D, D ∈ Ecmp (nonExh a) v) : D ⊆ cell a w

theorem TheilerRoelofsenAloni2018.mem_Ecmp_nonExh_of_subset_cell {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} {D : Set W} (hne : ∀ (d : ι), (a d).Nonempty) (hN : (nobody a).Nonempty) (hind : ∀ (d d' : ι), a d ⊆ a d' → d = d') (hsub : D ⊆ cell a w) (hne' : D.Nonempty) : D ∈ Ecmp (nonExh a) w

theorem TheilerRoelofsenAloni2018.mem_E_exh_of_subset_cell {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} {D : Set W} [Nonempty W] (hsub : D ⊆ cell a w) (hne' : D.Nonempty) : D ∈ E (exh a) w

theorem TheilerRoelofsenAloni2018.subset_cell_of_E_exh {W : Type u_1} {ι : Type u_3} {a : ι → Set W} {w : W} {D : Set W} [Nonempty W] [Finite W] (h : D ∈ E (exh a) w) : D ⊆ cell a w

theorem TheilerRoelofsenAloni2018.knowInt_Ecmp_nonExh_iff {W : Type u_1} {X : Type u_2} {ι : Type u_3} {a : ι → Set W} {w : W} [Nonempty W] [Finite W] {dox : X → W → Set W} {x : X} (hne : ∀ (d : ι), (a d).Nonempty) (hN : (nobody a).Nonempty) (hind : ∀ (d d' : ι), a d ⊆ a d' → d = d') : knowInt dox (Ecmp (nonExh a)) x w ↔ knowInt dox (E (exh a)) x w

Under the internal interpretation of know, the intermediate exhaustive reading of a wh-complement, the complete operator on the non-exhaustive nucleus, and its strongly exhaustive reading, the operator on the exhaustive nucleus, yield the same truth conditions, that the subject's state lies within one cell of the partition (Fact 2).

Constraints on responsive verb meanings (section 6)

@[reducible, inline]

abbrev TheilerRoelofsenAloni2018.Verb (W : Type u_3) (X : Type u_4) : Type (max u_3 u_4)

A responsive verb meaning, a world predicate from a complement meaning and a subject.

Equations

• TheilerRoelofsenAloni2018.Verb W X = ((W → Set (Set W)) → X → W → Prop)

def TheilerRoelofsenAloni2018.CDistributive {W : Type u_1} {X : Type u_2} (V : Verb W X) : Prop

A verb is c-distributive if it holds of a complement exactly when it holds of one of its cells, Definition 8 on partition nuclei, whose decomposition is the family of their cells.

Equations

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

def TheilerRoelofsenAloni2018.DeclVeridical {W : Type u_1} {X : Type u_2} (V : Verb W X) : Prop

Veridicality with respect to declarative complements (Definition 10).

Equations

• TheilerRoelofsenAloni2018.DeclVeridical V = ∀ (q : Set W) (x : X) (w : W), V (TheilerRoelofsenAloni2018.E (Question.ofSet q)) x w → w ∈ q

def TheilerRoelofsenAloni2018.IntVeridical {W : Type u_1} {X : Type u_2} (V : Verb W X) : Prop

Veridicality with respect to interrogative complements, on exhaustivity-neutral nuclei, the partitions, and the declaratives expressing their cells (Definition 11).

Equations

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

def TheilerRoelofsenAloni2018.Choice {W : Type u_1} {X : Type u_2} (V : Verb W X) : Prop

The choice property, that the verb does not hold of two inconsistent declaratives at once (Definition 9).

Equations

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

theorem TheilerRoelofsenAloni2018.IntVeridical.of_cDistributive {W : Type u_1} {X : Type u_2} {V : Verb W X} (hd : CDistributive V) (hv : DeclVeridical V) : IntVeridical V

A c-distributive verb veridical for declaratives is veridical for interrogatives (Fact 5).

theorem TheilerRoelofsenAloni2018.DeclVeridical.of_choice {W : Type u_1} {X : Type u_2} {V : Verb W X} [Nonempty W] (hd : CDistributive V) (hch : Choice V) (hv : IntVeridical V) : DeclVeridical V

A c-distributive verb with the choice property veridical for interrogatives is veridical for declaratives, by the polar question of the declarative (Fact 6).

theorem TheilerRoelofsenAloni2018.declVeridical_know {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) : DeclVeridical (know dox)

theorem TheilerRoelofsenAloni2018.cDistributive_know {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) [Finite W] : CDistributive (know dox)

know is c-distributive, since on a partition nucleus a state is a truthful resolution exactly when it is a truthful resolution of the true cell.

theorem TheilerRoelofsenAloni2018.intVeridical_know {W : Type u_1} {X : Type u_2} (dox : X → W → Set W) [Finite W] : IntVeridical (know dox)

know is veridical for interrogatives, (45), by Fact 5.