[Abu97]: Sequence of Tense and Temporal de re

[Abu97] [Sha03] [Hei94a] [Lew79a] [CvS82]

[Abu97]'s theory: tense morphemes are temporal pronouns (variables with presupposed constraints and binding modes). The key innovation is temporal de re: tense can take wide scope over attitude operators via res movement, just as DPs can scope out of attitude complements.

Two derivation styles coexist in this file:

1. Value-level shadow (abusch_derives_* against TensePronoun.fullPresupposition): tense pronoun + Core.Order.holds + temporal assignment. Captures Abusch's predictions at the value level without committing to the centered-world architecture. Cheap, presupposition-free.

2. Centered-world substrate (abusch_derives_*_via_acquaintance / _full / _full_metaphysical against Tense.DeRe.TemporalDeReReading): Intension (KContext) Time time-concept + holder-context base anchor + modal-alternative quantification over a Set (Index W Time). The Abusch §3 + eq. 13 architecture, faithful to the [Lew79a] / [CvS82] centered-world reduction of de re. The value-level style checks the same constraint at the same pair (res-time, holder's now), without the modal-rigidity conjunct.

The substrate is modal-base-agnostic and holder-now-honest: holderContext.time is the holder's now (per §7 ULC), and IsRigidAcrossAlternatives takes a Set (Index) parameter (with metaphysicalAlternatives / doxasticAlternatives convenience constructors).

Core Mechanisms

1. Tense as pronoun: TensePronoun (in Tense) with variable index, constraint, and binding mode.
2. Upper Limit Constraint (ULC): stated by [Abu97] §7 ("the now of an epistemic alternative is an upper limit for the denotation of tenses"); presuppositional construal due to [Hei94a], endorsed by Abusch 1997 fn 20. Lives in Semantics/Tense/Embedding.lean as upperLimitConstraint, formalized at the value level as embeddedR ≤ matrixE. Note: this value-level reduction strips the modal-alternative quantification the original formulation carries; making the modal layer explicit (over HistoricalAlternatives W Time à la [Kle16]) is deferred.
3. Temporal de re: tense variable in the res position of an attitude. The value-level shadow uses TensePronoun.fullPresupposition: constraint applied to (resolved time, eval time). The LF rewrite + acquaintance-relation machinery (Lewis 1979 / Cresswell-von Stechow 1982) is not formalized here.
4. Eval-time shift via attitude embedding: the substrate primitives are Tense.TensePronoun.evalTime_shifts_under_embedding and updateTemporal. Abusch's "relation transmission" (feature passing of relation variables PAST/PRES across embedding) is not what this file currently captures — we only model the value-level eval-time update.

Derivation Theorems

• Shifted reading: free past variable with presupposition against eval time
• Simultaneous reading: bound variable receives matrix event time
• Double-access: indexical present + attitude binding (placeholder; the full Abusch derivation involves doxastic alternatives + acquaintance relations + the rigid-present presupposition, not formalized here)
• Temporal de re: res movement for wide-scope tense

Limitations

• Relative clause tense: [Sha03]'s challenge (the mechanism doesn't extend straightforwardly to relative clauses where the tense takes the perspective of a participant)
• Modal-tense interaction: not addressed in [Abu97]'s framework (see [Kle16] for a successor)
• Counterfactual tense: not addressed
• Counterpart-relation isomorphism [Abu97] §12 invokes for the double-access reading derivation (the constraint that actual and belief worlds be temporally isomorphic, eliminating most of the 4 cells in the DAR diagram on p. 43): not formalized
• Modal-layer ULC formulation: see Core Mechanism 2 above

PLA Belief Reports and Conceptual Covers

The individual-side counterpart of temporal de re, formalized here as the substrate the temporal account parallels. A PLA epistemic layer ([Dek12] ch. 4) supplies doxastic accessibility, belief/knowledge tests, and Aloni-style conceptual covers ([Alo01]) — sets of concepts ("ways of thinking about" entities) relative to which "knowing who" and de re/de dicto are evaluated. Covers dissolve [Qui56]'s Ortcutt puzzle: Ralph believing "the man in the brown hat is a spy" and "the man at the beach is not a spy" (both Ortcutt) is consistent once the beliefs are indexed to non-overlapping covers. isAcquaintedWith here and the temporal-de-re acquaintance relation are the same Reference.Acquaintance substrate at different indices, making Abusch's individual ↔ temporal de re parallel true by construction (pla_isAcquaintedWith_unifies_with_polymorphic).

theorem Abusch1997.abusch_derives_shifted {Time : Type u_1} [LinearOrder Time] (tp : Tense.TensePronoun) (g : Tense.TemporalAssignment Time) (matrixFrame : _root_.Time.ReichenbachFrame Time) (hPresup : tp.resolve g < matrixFrame.eventTime) : (Tense.embeddedFrame matrixFrame (tp.resolve g) (tp.resolve g)).isPast

[Abu97] derives the shifted reading: a free past variable with presupposition checked against the (shifted) eval time. The past constraint gives R < evalTime = matrixE.

Note: the proof closes via embeddedFrame.isPast's definition, which only requires tp.resolve g < matrixFrame.eventTime. The tp.constraint = .past condition is what Abusch's theory says licenses this reading, but it isn't load-bearing in this proof — the conclusion follows for any tense pronoun whose resolution is below the matrix event time. A full Abusch derivation would project through Core.Order.holds tp.constraint from the binding mode.

theorem Abusch1997.abusch_derives_simultaneous {Time : Type u_1} (tp : Tense.TensePronoun) (g : Tense.TemporalAssignment Time) (matrixFrame : _root_.Time.ReichenbachFrame Time) (hBind : tp.resolve g = matrixFrame.eventTime) : (Tense.embeddedFrame matrixFrame (tp.resolve g) (tp.resolve g)).isPresent

[Abu97] derives the simultaneous reading: a bound variable receives the matrix event time via lambda abstraction.

theorem Abusch1997.abusch_derives_simultaneous_via_binding {Time : Type u_1} (tp : Tense.TensePronoun) (g : Tense.TemporalAssignment Time) (matrixFrame : _root_.Time.ReichenbachFrame Time) : tp.resolve (Tense.updateTemporal g tp.varIndex matrixFrame.eventTime) = matrixFrame.eventTime

[Abu97] derives the simultaneous reading via the bound variable mechanism: updating the temporal assignment so the tense variable receives matrix E.

theorem Abusch1997.abusch_derives_double_access {Time : Type u_1} (p : Time → Prop) (speechTime matrixEventTime : Time) (h_speech : p speechTime) (h_matrix : p matrixEventTime) : Tense.doubleAccess p speechTime matrixEventTime

[Abu97]'s double-access placeholder: indexical present requires truth at BOTH speech time (indexical rigidity) AND matrix event time (attitude accessibility). The full Abusch derivation involves doxastic alternatives + acquaintance relations + the rigid-present presupposition; this theorem only states the surface conjunction.

theorem Abusch1997.abusch_derives_temporal_de_re {Time : Type u_1} [LinearOrder Time] (tp : Tense.TensePronoun) (g : Tense.TemporalAssignment Time) (hPast : tp.constraint = Tense.past) (hBefore : tp.resolve g < tp.evalTime g) : tp.fullPresupposition g

[Abu97] derives temporal de re: the tense variable in res position is evaluated in the matrix context, giving wide-scope temporal reference. When the resolved referent satisfies the past constraint against the (matrix-shifted) eval time, the de re reading is felicitous.

Value-level shadow: this theorem checks TensePronoun.fullPresupposition, not Abusch's actual centered-proposition rule (paper def. 13). The g here would, in the full account, be a temporal assignment shifted by the attitude verb to put the matrix event time at tp.evalTimeIndex.

PLA belief reports and conceptual covers

The entity-side de re machinery that the temporal account parallels ([Dek12] ch. 4): a doxastic-accessibility relation over PLA possibilities, belief/knowledge as eliminative tests, and Aloni-style conceptual covers ([Alo01]).

De re belief ("John believes of Mary that she is smart") fixes the individual rigidly across the agent's belief worlds; de dicto belief ("John believes the winner is smart") tracks whoever satisfies a description in each world. A conceptual cover is a set of concepts that covers the domain and is functional per possibility — the agent's available "ways of thinking about" entities.

@[reducible, inline]

abbrev Abusch1997.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

• Abusch1997.DoxAccessibility E = (E → PLA.Poss E → PLA.Poss E → Prop)

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

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

Equations

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

def Abusch1997.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 : PLA.Poss E), R a p p

def Abusch1997.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 : PLA.Poss E), R a p q → R a q r → R a p r

def Abusch1997.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 : PLA.Poss E), ∃ (q : PLA.Poss E), R a p q

def Abusch1997.Formula.believe {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (a : E) (φ : PLA.Formula) : PLA.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

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

def Abusch1997.Formula.believeTerm {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (t : PLA.Term) (φ : PLA.Formula) : PLA.Update E

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

Equations

• Abusch1997.Formula.believeTerm R M t φ s = {p : PLA.Poss E | p ∈ s ∧ have a := PLA.Term.eval p.1 p.2 t; ∀ q ∈ Abusch1997.doxAccessible R a p, PLA.Formula.sat M q.1 q.2 φ}

theorem Abusch1997.believe_eliminative {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (a : E) (φ : PLA.Formula) (s : PLA.InfoState E) : Formula.believe R M a φ s ⊆ s

Belief is eliminative: Filtering to believers never adds possibilities.

theorem Abusch1997.believe_closure {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (a : E) (φ ψ : PLA.Formula) (s : PLA.InfoState E) (p : PLA.Poss E) (hent : ∀ (g : PLA.Assignment E) (ê : PLA.WitnessSeq E), PLA.Formula.sat M g ê φ → PLA.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 Abusch1997.believe_conj {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (a : E) (φ ψ : PLA.Formula) (s : PLA.InfoState E) (p : PLA.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 Abusch1997.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.

This is the PLA-indexed instance of the polymorphic Semantics.Reference.Acquaintance.Cover substrate (Acquaintance.Cover (Poss E) E). The two are definitionally equal — Cover E is the PLA-side name.

Equations

• Abusch1997.Cover E = Set (PLA.Concept E)

def Abusch1997.Cover.isExhaustive {E : Type u_1} (C : Cover E) : Prop

A cover is exhaustive if every entity is picked out by some concept in the cover (at every possibility). PLA-specific universal-domain wrapper around Acquaintance.Cover.isExhaustiveOn _ Set.univ.

Equations

• C.isExhaustive = Semantics.Reference.Acquaintance.Cover.isExhaustiveOn C Set.univ

@[reducible, inline]

abbrev Abusch1997.nameCover {E : Type u_1} (dom : Set E) : Cover E

The name cover: rigid concepts for each entity. PLA-side reference to the polymorphic Semantics.Reference.Acquaintance.nameCover at index Idx := Poss E. Definitionally equal; the polymorphic version is preferred in new proofs (this abbrev exists for PLA-literature readers familiar with the original naming).

Equations

• Abusch1997.nameCover dom = Semantics.Reference.Acquaintance.nameCover dom

def Abusch1997.variableCover {E : Type u_1} : Cover E

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

Equations

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

def Abusch1997.believeDeRe {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent individual : E) (pred : String) : PLA.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

• Abusch1997.believeDeRe R M agent individual pred s = {p : PLA.Poss E | p ∈ s ∧ ∀ q ∈ Abusch1997.doxAccessible R agent p, M.interp pred [individual] = true}

def Abusch1997.believeDeDicto {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (description : PLA.Concept E) (pred : String) : PLA.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

• Abusch1997.believeDeDicto R M agent description pred s = {p : PLA.Poss E | p ∈ s ∧ ∀ q ∈ Abusch1997.doxAccessible R agent p, M.interp pred [description q] = true}

theorem Abusch1997.deRe_implies_deDicto_rigid {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent individual : E) (c : PLA.Concept E) (pred : String) (_hrigid : c.isRigid) (hpicks : ∀ (p : PLA.Assignment E × PLA.WitnessSeq E), c p = individual) (s : PLA.InfoState E) (p : PLA.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 Abusch1997.substitutivity_deRe {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent a b : E) (pred : String) (heq : a = b) (s : PLA.InfoState E) (p : PLA.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

[Qui56]

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 Abusch1997.quineConsistent {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (c1 c2 : PLA.Concept E) (pred : String) (_s : PLA.InfoState E) (p : PLA.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 Abusch1997.quine_requires_divergence {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (c1 c2 : PLA.Concept E) (pred : String) (s : PLA.InfoState E) (p : PLA.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

[Dek12] 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 Abusch1997.believeExistsNarrow {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (C : Cover E) (pred : String) : PLA.Update E

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

Equations

• Abusch1997.believeExistsNarrow R M agent C pred s = {p : PLA.Poss E | p ∈ s ∧ ∀ q ∈ Abusch1997.doxAccessible R agent p, ∃ c ∈ C, M.interp pred [c q] = true}

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

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

Equations

• Abusch1997.believeExistsWide R M agent C pred s = {p : PLA.Poss E | p ∈ s ∧ ∃ c ∈ C, ∀ q ∈ Abusch1997.doxAccessible R agent p, M.interp pred [c q] = true}

theorem Abusch1997.obs20_wide_implies_narrow {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (C : Cover E) (pred : String) (s : PLA.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 Abusch1997.obs20_equiv_iff_uniform_witness {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (C : Cover E) (pred : String) (s : PLA.InfoState E) (p : PLA.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

[Dek12] 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 Abusch1997.knowsWho {E : Type u_1} (R : DoxAccessibility E) (agent individual : E) (C : Cover E) (p : PLA.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

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

def Abusch1997.hesperusPhosphorusScenario {E : Type u_1} (R : DoxAccessibility E) (agent : E) (hesperus phosphorus : PLA.Concept E) (venus : E) (p : PLA.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

• Abusch1997.hesperusPhosphorusScenario R agent hesperus phosphorus venus p = (hesperus p = venus ∧ phosphorus p = venus ∧ ∃ q ∈ Abusch1997.doxAccessible R agent p, hesperus q ≠ phosphorus q)

theorem Abusch1997.knowsWho_with_rigid_cover {E : Type u_1} (R : DoxAccessibility E) (agent individual : E) (C : Cover E) (p : PLA.Poss E) (hrigid : ∀ c ∈ C, c.isRigid) (hknows : knowsWho R agent individual C p) : ∃ c ∈ C, ∀ (q : PLA.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 Abusch1997.knowsWho_not_transferable {E : Type u_1} (R : DoxAccessibility E) (agent individual : E) (_C₁ C₂ : Cover E) (p : PLA.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 Abusch1997.believeExistsWithCover {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (C : Cover E) (pred : String) : PLA.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

• Abusch1997.believeExistsWithCover R M agent C pred s = {p : PLA.Poss E | p ∈ s ∧ ∃ c ∈ C, ∀ q ∈ Abusch1997.doxAccessible R agent p, M.interp pred [c q] = true}

theorem Abusch1997.believeExists_nameCover_deRe {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (dom : Set E) (pred : String) (s : PLA.InfoState E) (p : PLA.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.

@[reducible, inline]

abbrev Abusch1997.isAcquaintedWith {E : Type u_1} (individual : E) (C : Cover E) (p : PLA.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). PLA-side reference to Semantics.Reference.Acquaintance.isAcquaintedWith at the PLA index Idx := Poss E. Definitionally equal — the abbrev preserves the PLA-literature naming.

Equations

• Abusch1997.isAcquaintedWith individual C p = Semantics.Reference.Acquaintance.isAcquaintedWith individual C p

def Abusch1997.believeDeReWithAcquaintance {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (agent : E) (C : Cover E) (individual : E) (pred : String) : PLA.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 Abusch1997.Formula.know {E : Type u_1} (R : DoxAccessibility E) (M : PLA.Model E) (a : E) (φ : PLA.Formula) : PLA.Update E

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

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

Equations

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

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

Knowledge implies belief.

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

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

theorem Abusch1997.abusch_derives_temporal_de_re_via_acquaintance {W : Type u_1} {E : Type u_2} {P : Type u_3} {Time : Type u_4} [LinearOrder Time] (dr : Tense.DeRe.TemporalDeReReading W E P Time) (hBefore : dr.actualRes < dr.holderContext.time) : dr.IsFelicitousWith Tense.past

[Abu97]'s temporal de re via the centered-world substrate (Semantics/Tense/DeRe.lean): any TemporalDeReReading whose actual res-time precedes the holder's now satisfies the past constraint. Value-level felicity reduces to the actualRes ordering; rigidity of the concept (= acquaintance-anchored res reading) is not required for the value-level shadow.

theorem Abusch1997.abusch_derives_temporal_de_re_full {W : Type u_1} {E : Type u_2} {P : Type u_3} {Time : Type u_4} [LinearOrder Time] (dr : Tense.DeRe.TemporalDeReReading W E P Time) (hRigid : Intensional.Intension.IsRigid dr.concept) (alternatives : Set (Intensional.Index W Time)) (hBefore : dr.actualRes < dr.holderContext.time) : dr.IsFelicitous alternatives Tense.past

[Abu97]'s temporal de re with modal-alternative quantification (substrate-level lift of the §3 p. 9 base-world condition): the time-concept identifies the same time across an alternatives : Set (Index W Time). The substrate is modal-base-agnostic; this theorem holds for any alternative-set the consumer supplies (doxastic, metaphysical, or other). The full IsFelicitous predicate combines the value-level past constraint with this modal rigidity.

A rigid time-concept (constant intension) discharges the modal rigidity automatically — Abusch's de re reading is satisfied "for free" when the res is identified by a name-like rigid concept.

theorem Abusch1997.abusch_derives_temporal_de_re_full_metaphysical {W : Type u_1} {E : Type u_2} {P : Type u_3} {Time : Type u_4} [LinearOrder Time] (dr : Tense.DeRe.TemporalDeReReading W E P Time) (hRigid : Intensional.Intension.IsRigid dr.concept) (history : HistoricalAlternatives W Time) (hBefore : dr.actualRes < dr.holderContext.time) : dr.IsFelicitous (Tense.DeRe.TemporalDeReReading.metaphysicalAlternatives history dr) Tense.past

Metaphysical-instantiation specialization of abusch_derives_temporal_de_re_full. Recovers the legacy HistoricalAlternatives-based formulation as a corollary at the metaphysicalAlternatives instance, demonstrating backward compatibility with Klecha 2016 DOX-shaped reasoning.

theorem Abusch1997.pla_isAcquaintedWith_unifies_with_polymorphic {E : Type u_1} (individual : E) (C : Cover E) (p : PLA.Poss E) : isAcquaintedWith individual C p ↔ Semantics.Reference.Acquaintance.isAcquaintedWith individual C p

Individual ↔ temporal de re unification: the PLA-literature isAcquaintedWith alias above (entity-side, individual de re) and the polymorphic Reference.Acquaintance.isAcquaintedWith are the same predicate at the PLA index Idx := Poss E. Provable by Iff.rfl because the alias is a definitional wrapper (abbrev) of the polymorphic version.

The content of the theorem is structural — it shows the de re reading proved about individuals and the de re reading TemporalDeReReading exposes for times are instantiations of the same acquaintance substrate, making true [Abu97]'s p. 6 prose claim ("To apply the same machinery to de re belief, a further constraint is required") via the Acquaintance polymorphism.

Reichenbach frames for the canonical Abusch-tradition SOT diagnostics: past-under-past (simultaneous + shifted), present- under-past (double-access), future-under-past (would), the ULC foil (forward-shifted), and temporal de re. Each embedded frame is constructed via the embeddedFrame / simultaneousFrame substrate operators (per CLAUDE.md "Theory-hub denotation as study-file constraint") rather than hand-stipulating S/P/R/E records.

def Abusch1997.matrixSaid : Time.ReichenbachFrame ℤ

Matrix frame for "John said..." (past tense, perfective). Speech time S = 0, saying event at t = -2. Root clause: P = S; perfective: E = R.

Equations

• Abusch1997.matrixSaid = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

def Abusch1997.embeddedSickSimultaneous : Time.ReichenbachFrame ℤ

"Mary was sick" — SIMULTANEOUS reading. Embedded P = matrix E = -2, R' = E_matrix = -2: Mary is sick at the time of the saying.

Equations

• Abusch1997.embeddedSickSimultaneous = Tense.simultaneousFrame Abusch1997.matrixSaid (-2)

def Abusch1997.embeddedSickShifted : Time.ReichenbachFrame ℤ

"Mary was sick" — SHIFTED reading. R' = -5 < E_matrix: Mary was sick before the saying.

Equations

• Abusch1997.embeddedSickShifted = Tense.embeddedFrame Abusch1997.matrixSaid (-5) (-5)

def Abusch1997.embeddedSickPresent : Time.ReichenbachFrame ℤ

"Mary is sick" (present-under-past) — DOUBLE-ACCESS reading. Embedded P = matrix E = -2, R' = -2, E = 0 (speech time): Mary is sick now AND the sickness is relevant at the time of saying.

Equations

• Abusch1997.embeddedSickPresent = Tense.embeddedFrame Abusch1997.matrixSaid (-2) 0

def Abusch1997.embeddedWouldLeave : Time.ReichenbachFrame ℤ

"Mary would leave" (future-under-past). "Would" = PAST + FUTURE: the leaving is after the saying. R' = -1 > E_matrix.

Equations

• Abusch1997.embeddedWouldLeave = Tense.embeddedFrame Abusch1997.matrixSaid (-1) (-1)

def Abusch1997.embeddedSickForwardShifted : Time.ReichenbachFrame ℤ

Hypothetical FORWARD-SHIFTED frame (ULC foil, §7). R' = -1 > E_matrix = -2: sick AFTER the saying. Predicted not to exist as a reading per Abusch's Upper Limit Constraint. Structurally coincides with embeddedWouldLeave's record — the Reichenbach encoding cannot distinguish "ULC violation" from "valid future reading"; only the analyst's intent and the sentence's actual meaning do.

Equations

• Abusch1997.embeddedSickForwardShifted = Tense.embeddedFrame Abusch1997.matrixSaid (-1) (-1)

def Abusch1997.temporalDeRe : Time.ReichenbachFrame ℤ

"John believed it was raining" — TEMPORAL DE RE. The rain event is located at -3 via the actual world (de re), not in John's belief worlds (de dicto). Embedded P = -2, R = E = -3.

Equations

• Abusch1997.temporalDeRe = Tense.embeddedFrame Abusch1997.matrixSaid (-3) (-3)

theorem Abusch1997.abusch_derives_embeddedSickSimultaneous : embeddedSickSimultaneous.isPresent

The simultaneous frame is isPresent (R = P). Per Abusch: a bound variable receives matrix E.

theorem Abusch1997.abusch_derives_embeddedSickShifted : embeddedSickShifted.isPast

The shifted frame is isPast (R < P). Per Abusch: a free past variable below the matrix event time.

theorem Abusch1997.matrixSaid_is_perfective : matrixSaid.isPerfective

The matrix "said" frame is perfective (E = R).

theorem Abusch1997.embeddedShifted_is_perfective : embeddedSickShifted.isPerfective

The shifted embedded frame is perfective (E = R).

theorem Abusch1997.forwardShifted_violates_ulc : ¬Tense.upperLimitConstraint embeddedSickForwardShifted.referenceTime matrixSaid.eventTime

Forward-shifted reading violates ULC: R' > E_matrix is not allowed.

theorem Abusch1997.simultaneous_satisfies_ulc : Tense.upperLimitConstraint embeddedSickSimultaneous.referenceTime matrixSaid.eventTime

Simultaneous reading satisfies ULC: R' ≤ E_matrix.

theorem Abusch1997.shifted_satisfies_ulc : Tense.upperLimitConstraint embeddedSickShifted.referenceTime matrixSaid.eventTime

Shifted reading satisfies ULC: R' < E_matrix.