Acquaintance and Conceptual Covers

@cite{lewis-1979-attitudes} (de se / de re reduction via centered worlds); @cite{cresswell-vonstechow-1982} (de re belief generalized); @cite{aloni-2001} (conceptual covers); @cite{abusch-1997} (the temporal analogue: a "way of identifying a time" is the temporal time-concept licensing temporal de re).

A polymorphic substrate for acquaintance-relation semantics: a Cover Idx Res is a set of intensions over an evaluation index Idx that picks out values in Res; an entity is acquainted (at index p) when some concept in the cover identifies it at p.

Instantiated at Idx := Assignment E × WitnessSeq E, Res := E this is the PLA cover system in Theories/Semantics/Dynamic/PLA/Belief.lean. Instantiated at Idx := KContext W E P T, Res := T this is the Abusch 1997 time-concept (def. 13). The polymorphic substrate makes the individual ↔ temporal de re parallel that Abusch's prose asserts true by construction.

Reuse

Built on Core.Intension W τ (Core/Logic/Intensional/Rigidity.lean) — no parallel Concept type is introduced. The acquaintance predicate is Set.image-membership; cover exhaustiveness is Set.SurjOn. Both are mathlib idioms — the only genuinely new content here is naming.

@[reducible, inline]

abbrev Semantics.Reference.Acquaintance.Cover (Idx : Type u_1) (Res : Type u_2) : Type (max u_2 u_1)

A conceptual cover (@cite{aloni-2001} §3.2): a set of intensions over an evaluation index Idx representing the agent's available "ways of identifying" values of type Res.

The Abusch 1997 §3 acquaintance relation R : eeiwt is the temporal instance with Idx := KContext W E P T, Res := T.

Equations

• Semantics.Reference.Acquaintance.Cover Idx Res = Set (Core.Intension Idx Res)

def Semantics.Reference.Acquaintance.Cover.isExhaustiveOn {Idx : Type u_1} {Res : Type u_2} (C : Cover Idx Res) (dom : Set Res) : Prop

A cover is exhaustive on a domain when, at every index, every value in the domain is picked out by some concept in the cover.

Mathlib idiom: Set.SurjOn (· p) C dom.

Equations

• C.isExhaustiveOn dom = ∀ (p : Idx), Set.SurjOn (fun (x : Core.Intension Idx Res) => x p) C dom

def Semantics.Reference.Acquaintance.isAcquaintedWith {Idx : Type u_1} {Res : Type u_2} (r : Res) (C : Cover Idx Res) (p : Idx) : Prop

@cite{lewis-1979-attitudes}'s acquaintance relation, generalized: r is acquainted-with at index p (relative to C) when some concept in C picks out r at p.

Mathlib idiom: r ∈ ((· p) '' C) — set-image membership.

Equations

• Semantics.Reference.Acquaintance.isAcquaintedWith r C p = (r ∈ (fun (c : Core.Intension Idx Res) => c p) '' C)

def Semantics.Reference.Acquaintance.nameCover {Idx : Type u_1} {Res : Type u_2} (dom : Set Res) : Cover Idx Res

@cite{aloni-2001}'s name cover: rigid concepts (one per entity). Each entity is identified by its constant intension Intension.rigid. This is the "de re" cover — entities thought of as themselves.

Equations

• Semantics.Reference.Acquaintance.nameCover dom = {c : Core.Intension Idx Res | ∃ (r : Res), r ∈ dom ∧ c = Core.Intension.rigid r}

theorem Semantics.Reference.Acquaintance.nameCover_rigid {Idx : Type u_1} {Res : Type u_2} (dom : Set Res) (c : Core.Intension Idx Res) : c ∈ nameCover dom → c.IsRigid

Every concept in a name cover is rigid.

theorem Semantics.Reference.Acquaintance.nameCover_isExhaustiveOn {Idx : Type u_1} {Res : Type u_2} (dom : Set Res) : (nameCover dom).isExhaustiveOn dom

The name cover is exhaustive over its domain.

theorem Semantics.Reference.Acquaintance.nameCover_isAcquaintedWith_of_mem {Idx : Type u_1} {Res : Type u_2} (dom : Set Res) (r : Res) (hr : r ∈ dom) (p : Idx) : isAcquaintedWith r (nameCover dom) p

An entity in the name cover's domain is acquainted-with via the name cover at every index — names are rigid, so they identify entities at all evaluation points.