@[reducible, inline]

abbrev Semantics.Dynamic.PLA.DoxAccessibility (E : Type u_2) : Type u_2

Doxastic accessibility relation: what worlds/possibilities agent a considers compatible with their beliefs.

R a p q means: in possibility p, agent a considers q doxastically accessible (q is compatible with what a believes in p).

Equations

• Semantics.Dynamic.PLA.DoxAccessibility E = (E → Semantics.Dynamic.PLA.Poss E → Semantics.Dynamic.PLA.Poss E → Prop)

def Semantics.Dynamic.PLA.doxAccessible {E : Type u_1} (R : DoxAccessibility E) (a : E) (p : Poss E) : Set (Poss E)

The set of doxastically accessible possibilities for agent a at p.

Equations

• Semantics.Dynamic.PLA.doxAccessible R a p = {q : Semantics.Dynamic.PLA.Poss E | R a p q}

def Semantics.Dynamic.PLA.DoxAccessibility.isReflexive {E : Type u_1} (R : DoxAccessibility E) : Prop

Reflexivity: agent believes truths (factivity for knowledge). Note: belief is not typically factive, but this is useful for knowledge.

Equations

• R.isReflexive = ∀ (a : E) (p : Semantics.Dynamic.PLA.Poss E), R a p p

def Semantics.Dynamic.PLA.DoxAccessibility.isTransitive {E : Type u_1} (R : DoxAccessibility E) : Prop

Transitivity: positive introspection (believing implies believing you believe).

Equations

• R.isTransitive = ∀ (a : E) (p q r : Semantics.Dynamic.PLA.Poss E), R a p q → R a q r → R a p r

def Semantics.Dynamic.PLA.DoxAccessibility.isSerial {E : Type u_1} (R : DoxAccessibility E) : Prop

Seriality: no inconsistent belief states (for every p, some q is accessible). This is the minimal requirement for belief: consistent belief states.

Equations

• R.isSerial = ∀ (a : E) (p : Semantics.Dynamic.PLA.Poss E), ∃ (q : Semantics.Dynamic.PLA.Poss E), R a p q

def Semantics.Dynamic.PLA.Formula.believe {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ : Formula) : Update E

Belief operator: agent a believes φ.

B(a, φ) is true at (g, ê) iff φ is true at all doxastically accessible possibilities.

This is a TEST: it checks if the agent's belief state supports φ.

Equations

• Semantics.Dynamic.PLA.Formula.believe R M a φ s = {p : Semantics.Dynamic.PLA.Poss E | p ∈ s ∧ ∀ q ∈ Semantics.Dynamic.PLA.doxAccessible R a p, Semantics.Dynamic.PLA.Formula.sat M q.1 q.2 φ}

def Semantics.Dynamic.PLA.Formula.believeTerm {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (t : Term) (φ : Formula) : Update E

Belief with term: B(t, φ) where t is a term denoting the agent.

Equations

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

theorem Semantics.Dynamic.PLA.believe_eliminative {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ : Formula) (s : InfoState E) : Formula.believe R M a φ s ⊆ s

Belief is eliminative: Filtering to believers never adds possibilities.

theorem Semantics.Dynamic.PLA.believe_closure {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ ψ : Formula) (s : InfoState E) (p : Poss E) (hent : ∀ (g : Assignment E) (ê : WitnessSeq E), Formula.sat M g ê φ → Formula.sat M g ê ψ) (hp : p ∈ Formula.believe R M a φ s) : p ∈ Formula.believe R M a ψ s

Belief closure under entailment: If you believe φ and φ entails ψ, you believe ψ.

theorem Semantics.Dynamic.PLA.believe_conj {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ ψ : Formula) (s : InfoState E) (p : Poss E) : p ∈ Formula.believe R M a (φ ⋀ ψ) s ↔ p ∈ Formula.believe R M a φ s ∧ p ∈ Formula.believe R M a ψ s

Conjunction distribution: B(a, φ ∧ ψ) ↔ B(a, φ) ∧ B(a, ψ)

@[reducible, inline]

abbrev Semantics.Dynamic.PLA.Cover (E : Type u_2) : Type u_2

A Conceptual Cover is a set of concepts (ways of identifying entities).

In Aloni's framework, a cover represents the "ways of thinking" available to an agent or in a context.

Equations

• Semantics.Dynamic.PLA.Cover E = Set (Semantics.Dynamic.PLA.Concept E)

def Semantics.Dynamic.PLA.Cover.isExhaustive {E : Type u_1} (C : Cover E) : Prop

A cover is exhaustive if every entity in the domain is picked out by some concept in the cover (at every possibility).

Equations

• C.isExhaustive = ∀ (p : Semantics.Dynamic.PLA.Poss E) (e : E), ∃ c ∈ C, c p = e

def Semantics.Dynamic.PLA.nameCover {E : Type u_1} (dom : Set E) : Cover E

The name cover: rigid concepts for each entity. This is the "de re" cover - thinking of entities as themselves.

Equations

• Semantics.Dynamic.PLA.nameCover dom = {x : Semantics.Dynamic.PLA.Concept E | ∃ e ∈ dom, Semantics.Dynamic.PLA.Concept.const e = x}

def Semantics.Dynamic.PLA.variableCover {E : Type u_1} : Cover E

The variable cover: concepts from variable assignments. This is more "de dicto" - thinking via variable bindings.

Equations

• Semantics.Dynamic.PLA.variableCover = {x : Semantics.Dynamic.PLA.Concept E | ∃ (i : Semantics.Dynamic.PLA.VarIdx), Semantics.Dynamic.PLA.Concept.fromVar i = x}

theorem Semantics.Dynamic.PLA.nameCover_exhaustive {E : Type u_1} [Nonempty E] (dom : Set E) (_hne : dom.Nonempty) (p : Poss E) (e : E) : e ∈ dom → ∃ c ∈ nameCover dom, c p = e

Name cover is exhaustive over its domain.

theorem Semantics.Dynamic.PLA.nameCover_rigid {E : Type u_1} [Nonempty E] (dom : Set E) (c : Concept E) : c ∈ nameCover dom → c.isRigid

All concepts in the name cover are rigid.

def Semantics.Dynamic.PLA.believeDeRe {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent individual : E) (pred : String) : Update E

De re belief: Belief about a specific individual, identified rigidly.

"John believes of Mary that she is smart."

The individual (Mary) is fixed across all of John's belief worlds.

Equations

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

def Semantics.Dynamic.PLA.believeDeDicto {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (description : Concept E) (pred : String) : Update E

De dicto belief: Belief about whoever satisfies a description.

"John believes that the winner is smart."

The individual may vary across John's belief worlds (whoever is the winner there).

Equations

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

theorem Semantics.Dynamic.PLA.deRe_implies_deDicto_rigid {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent individual : E) (c : Concept E) (pred : String) (_hrigid : c.isRigid) (hpicks : ∀ (p : Assignment E × WitnessSeq E), c p = individual) (s : InfoState E) (p : Poss E) (hp : p ∈ believeDeRe R M agent individual pred s) : p ∈ believeDeDicto R M agent c pred s

De re implies de dicto when the concept is rigid.

If you believe of x that P(x), and concept c rigidly picks out x, then you believe that P(c).

theorem Semantics.Dynamic.PLA.substitutivity_deRe {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent a b : E) (pred : String) (heq : a = b) (s : InfoState E) (p : Poss E) (hp : p ∈ believeDeRe R M agent a pred s) : p ∈ believeDeRe R M agent b pred s

Substitutivity of identicals (de re): If a = b and you believe P(a), then you believe P(b).

This holds for de re beliefs because the individual is fixed.

Quine's Ortcutt Puzzle

@cite{quine-1956}

The linguistic puzzle that motivates conceptual covers:

"Ralph believes that the man in the brown hat is a spy." "Ralph believes that the man seen at the beach is not a spy." The man in the brown hat IS the man seen at the beach (= Ortcutt).

Naively, this seems to attribute contradictory beliefs to Ralph. But Ralph is perfectly rational - he simply doesn't know that the two descriptions pick out the same individual.

The apparent contradiction dissolves when we recognize that Ralph's beliefs are relativized to conceptual covers:

• Under the "brown hat" cover, Ralph believes Ortcutt is a spy
• Under the "beach" cover, Ralph believes Ortcutt is not a spy

These are consistent because the covers don't overlap in Ralph's belief worlds.

def Semantics.Dynamic.PLA.quineConsistent {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (c1 c2 : Concept E) (pred : String) (_s : InfoState E) (p : Poss E) : Prop

Quine consistency: An agent can believe P(x) under one cover and ¬P(x) under another cover, without inconsistency.

This is the formal core of Quine's puzzle: what looks like believing both P(o) and ¬P(o) is actually consistent when the beliefs are relativized to different conceptual covers.

Linguistic example: Ralph believes "the man in the brown hat is a spy" AND "the man seen at the beach is not a spy" - both about Ortcutt, yet consistent.

Equations

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

theorem Semantics.Dynamic.PLA.quine_requires_divergence {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent : E) (c1 c2 : Concept E) (pred : String) (s : InfoState E) (p : Poss E) (_hs : Set.Nonempty s) (hdox : (doxAccessible R agent p).Nonempty) (hquine : quineConsistent R M agent c1 c2 pred s p) : ∃ q ∈ doxAccessible R agent p, c1 q ≠ c2 q

Quine consistency requires concept divergence: If an agent has Quine-consistent beliefs about an individual (believing P under one cover, ¬P under another), then the concepts must diverge in some belief-accessible world.

Quine consistency is possible because the concepts that coincide in the actual world must pick out different individuals in some of the agent's belief worlds.

Observation 20: Quantifier Scope and Belief

@cite{dekker-2012} Observation 20 (Quantifier Import and Export, p.95):

B(r, ∃x_C Sx) = ∃x_C B(r, Sx)

This equivalence holds when quantification is relativized to a conceptual cover C. An existential quantifier can be "exported" from inside a belief context, provided it ranges over concepts in the agent's cover.

Linguistic motivation: consider "Ralph believes someone is a spy."

1. Wide scope (de re): ∃x_C B(r, Sx) "There is someone (under cover C) such that Ralph believes they are a spy." Ralph has a specific individual in mind.

2. Narrow scope (de dicto): B(r, ∃x_C Sx) "Ralph believes that someone (under cover C) is a spy." Ralph believes the existential claim without necessarily having a specific individual in mind.

These readings are equivalent when the cover C represents Ralph's available ways of identifying individuals.

In classical intensional semantics (without covers), wide and narrow scope are not equivalent. Covers make them equivalent because the quantifier domain is "grounded" in the agent's conceptual repertoire.

def Semantics.Dynamic.PLA.believeExistsNarrow {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (pred : String) : Update E

Narrow scope existential belief: Agent believes ∃x.P(x) The existential is inside the belief operator.

Equations

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

def Semantics.Dynamic.PLA.believeExistsWide {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (pred : String) : Update E

Wide scope existential belief: ∃x.B(agent, P(x)) The existential scopes over the belief operator.

Equations

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

theorem Semantics.Dynamic.PLA.obs20_wide_implies_narrow {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (pred : String) (s : InfoState E) : believeExistsWide R M agent C pred s ⊆ believeExistsNarrow R M agent C pred s

Observation 20 (wide → narrow): Wide scope implies narrow scope (always holds).

∃x_C B(r, Sx) → B(r, ∃x_C Sx)

If there's a specific concept c such that Ralph believes P(c), then Ralph believes that something satisfies P.

theorem Semantics.Dynamic.PLA.obs20_equiv_iff_uniform_witness {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (pred : String) (s : InfoState E) (p : Poss E) (hp : p ∈ s) : p ∈ believeExistsWide R M agent C pred s ↔ p ∈ s ∧ ∃ c ∈ C, ∀ q ∈ doxAccessible R agent p, M.interp pred [c q] = true

Observation 20 (equivalence characterization): Wide and narrow scope are equivalent iff there exists a uniform witnessing concept.

The narrow → wide direction requires Skolemization: turning per-world witnesses (∀q, ∃c) into a uniform witness (∃c, ∀q). This holds when:

• The cover is finite and doxastic state is finite (by pigeonhole)
• The cover satisfies a "tracking" condition (concepts persist across worlds)

We state the precise equivalence condition rather than assuming it.

Observation 21: Knowing Who is Cover-Relative

@cite{dekker-2012} Observation 21 (Knowing and not Knowing Who, p.97):

"Knowing who" is relative to a conceptual cover.

The Hesperus/Phosphorus puzzle:

The ancients knew that:

• Hesperus is the evening star (visible at dusk)
• Phosphorus is the morning star (visible at dawn)

They did not know that Hesperus = Phosphorus (both are Venus).

Question: Did the ancients "know who Hesperus is"?

Answer depends on the cover:

• Under the astronomical cover (celestial bodies as physical objects): No - they didn't know Hesperus is Venus.
• Under the observational cover (celestial bodies by when they appear): Yes - they knew Hesperus is "the bright thing in the evening sky."

"Knowing who" is not absolute but relative to a contextually supplied way of carving up the domain of individuals.

This explains why "knowing who" questions are context-sensitive:

• "Do you know who the president is?" (identification by role)
• "Do you know who that person is?" (identification by name/face)

Different questions presuppose different conceptual covers.

def Semantics.Dynamic.PLA.knowsWho {E : Type u_1} (R : DoxAccessibility E) (agent individual : E) (C : Cover E) (p : Poss E) : Prop

Knowing who (cover-relative): Agent knows who x is under cover C.

K_C(a, who(x)) holds iff:

1. Agent has an identifying concept c in cover C
2. c picks out x in all epistemically accessible worlds
3. Agent knows that c picks out x

Equations

• Semantics.Dynamic.PLA.knowsWho R agent individual C p = ∃ c ∈ C, c p = individual ∧ ∀ q ∈ Semantics.Dynamic.PLA.doxAccessible R agent p, c q = individual

def Semantics.Dynamic.PLA.hesperusPhosphorusScenario {E : Type u_1} (R : DoxAccessibility E) (agent : E) (hesperus phosphorus : Concept E) (venus : E) (p : Poss E) : Prop

Hesperus/Phosphorus: Two concepts can pick out the same individual at the actual world but different individuals in belief-accessible worlds.

Equations

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

theorem Semantics.Dynamic.PLA.knowsWho_with_rigid_cover {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (agent individual : E) (C : Cover E) (p : Poss E) (hrigid : ∀ c ∈ C, c.isRigid) (hknows : knowsWho R agent individual C p) : ∃ c ∈ C, ∀ (q : Poss E), c q = individual

Observation 21: Knowing who is cover-relative.

If the cover includes only rigid concepts (like proper names), then knowing who is equivalent to de re identification.

But if the cover includes descriptive concepts (like "the evening star"), knowing who becomes weaker - it only requires identifying x via the contextually appropriate description.

theorem Semantics.Dynamic.PLA.knowsWho_not_transferable {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (agent individual : E) (_C₁ C₂ : Cover E) (p : Poss E) (_hknows : knowsWho R agent individual _C₁ p) (hno_rigid : ∀ c ∈ C₂, c p = individual → ∃ q ∈ doxAccessible R agent p, c q ≠ individual) : ¬knowsWho R agent individual C₂ p

Knowing who under one cover does not transfer to another cover.

If the agent knows who x is under cover C₁, this does NOT imply they know who x is under a different cover C₂.

This is the formal content of the Hesperus/Phosphorus puzzle: the ancients knew "who Hesperus is" under an observational cover but not under an astronomical cover.

def Semantics.Dynamic.PLA.believeExistsWithCover {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (pred : String) : Update E

Belief relative to a cover: The agent's beliefs are interpreted relative to a conceptual cover (their available ways of thinking).

B_C(a, ∃x.P(x)) is true iff for some concept c in cover C, a believes P(c).

Equations

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

theorem Semantics.Dynamic.PLA.believeExists_nameCover_deRe {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (agent : E) (dom : Set E) (pred : String) (s : InfoState E) (p : Poss E) : p ∈ believeExistsWithCover R M agent (nameCover dom) pred s ↔ p ∈ s ∧ ∃ e ∈ dom, ∀ q ∈ doxAccessible R agent p, M.interp pred [e] = true

Belief relative to name cover is equivalent to de re quantification.

def Semantics.Dynamic.PLA.isAcquaintedWith {E : Type u_1} (_agent individual : E) (C : Cover E) (p : Poss E) : Prop

Acquaintance requirement (Russell): De re belief requires acquaintance.

You can only have de re beliefs about entities you're "acquainted with" (entities in your conceptual cover).

Equations

• Semantics.Dynamic.PLA.isAcquaintedWith _agent individual C p = ∃ c ∈ C, c p = individual

def Semantics.Dynamic.PLA.believeDeReWithAcquaintance {E : Type u_1} (R : DoxAccessibility E) (M : Model E) (agent : E) (C : Cover E) (individual : E) (pred : String) : Update E

De re belief presupposes acquaintance (relative to a cover).

Equations

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

def Semantics.Dynamic.PLA.Formula.know {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ : Formula) : Update E

Knowledge: factive belief (what you know is true).

K(a, φ) implies φ is actually true, not just believed.

Equations

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

theorem Semantics.Dynamic.PLA.know_implies_believe {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ : Formula) (s : InfoState E) : Formula.know R M a φ s ⊆ Formula.believe R M a φ s

Knowledge implies belief.

theorem Semantics.Dynamic.PLA.know_factive {E : Type u_1} [Nonempty E] (R : DoxAccessibility E) (M : Model E) (a : E) (φ : Formula) (s : InfoState E) (p : Poss E) (hp : p ∈ Formula.know R M a φ s) : Formula.sat M p.1 p.2 φ

Knowledge is factive: K(a, φ) → φ