Docs / Semantics / Attitudes / Acquaintance

De re attitudes by acquaintance

import Linglib.Semantics.Attitudes.Acquaintance · namespace Acquaintance

For Lewis the objects of attitudes are properties of centers, a subject at a time in a world, and a relation the subject bears to things serves as a description: at each center it picks out the unique thing the center bears it to, when there is one. A relation thus determines a partial concept, of which a concept, a value at every center, is the total case. A subject ascribes a property to a res under a partial concept when its value at her center is the res and every alternative has the property of its value there; a de re belief is such an ascription under a relation of acquaintance, and identity, the concept of the self, makes belief de se the case of belief de re through identity.

Main definitions

Acquaintance.relatum: the partial concept of a relation, through the iota operator.
Acquaintance.deRe: the property of having a value of a partial concept that has a property.
Acquaintance.AscribesUnder: ascription of a property to a res under a partial concept.

Main statements

Acquaintance.relatum_eq_some_iff: a center's relatum is what it bears the relation to and nothing else to.
Acquaintance.mem_deRe_relatum_iff: the de re property of a relation is the property of bearing it uniquely to something that has the property.
Acquaintance.relatum_eq: a concept is the partial concept of the relation of identity with its values.
Acquaintance.ascribesUnder_comp_some, Acquaintance.ascribesUnder_comp_some_apply: ascription under a concept, and ascription under identity as self-ascription.

References

Lewis 1979, Attitudes De Dicto and De Se
Cresswell & von Stechow 1982, De re belief generalized
Heim 1994, Comments on Abusch’s Theory of Tense
Abusch 1997, Sequence of Tense and Temporal De Re formalized

Declarations

The relatum of the center p under R is the unique thing p bears R to, and none when there is no such thing or several.

relatum L49–51

noncomputable def Acquaintance.relatum {α : Type u_1} {C : Type u_2} (R : α → C → Prop) (p : C) :

Option α

relatum R p = iota fun (x : α) => R x p

Used by relatum_eq_some_iff, relatum_eq, mem_deRe_relatum_iff

Used in Pearson2015

The property of having a value under the partial concept k that has P, the centers that do.

def deRe L53–55

{α : Type u_1} {C : Type u_2} (k : C → Option α) (P : α → Set C) :

Set C

deRe k P = {p : C | ∃ y ∈ k p, p ∈ P y}

Used by AscribesUnder, mem_deRe_iff_of_eq_some, mem_deRe_relatum_iff, mem_deRe_comp_some

At the center p, with attitude alternatives A, the subject ascribes P to y under k when k picks out y at her center and she self-ascribes the property of having a value under k that has P, every alternative having it.

def AscribesUnder L57–61

{α : Type u_1} {C : Type u_2} (A : Set C) (p : C) (k : C → Option α) (y : α) (P : α → Set C) :

Prop

AscribesUnder A p k y P = (k p = some y ∧ A ⊆ deRe k P)

Built from

Used by ascribesUnder_comp_some, ascribesUnder_comp_some_apply

Used in Abusch1997, Aloni2001

theorem relatum_eq_some_iff L63–64

{α : Type u_1} {C : Type u_2} {R : α → C → Prop} {p : C} {y : α} :

relatum R p = some y ↔ R y p ∧ ∀ (z : α), R z p → z = y

Built from

A concept is the partial concept of the relation each center bears to its value there.

theorem relatum_eq L66–68

{α : Type u_1} {C : Type u_2} (c : C → α) :

(relatum fun (y : α) (p : C) => y = c p) = some ∘ c

Built from

L70–71

The de re property of a relation is the property of bearing it uniquely to something that has the property.

theorem mem_deRe_relatum_iff L73–77

{α : Type u_1} {C : Type u_2} {R : α → C → Prop} {P : α → Set C} {p : C} :

p ∈ deRe (relatum R) P ↔ ∃ (y : α), (R y p ∧ ∀ (z : α), R z p → z = y) ∧ p ∈ P y

Built from ,

L79–80

theorem ascribesUnder_comp_some L82–85

{α : Type u_1} {C : Type u_2} {c : C → α} {P : α → Set C} {A : Set C} {p : C} {y : α} :

AscribesUnder A p (some ∘ c) y P ↔ y = c p ∧ ∀ q ∈ A, q ∈ P (c q)

Built from

Ascribing P under a concept to its value at the subject's own center is self-ascribing the property of the concept's value. With the self of each center as the concept, identity, this is Lewis's reduction of belief de se to belief de re.

theorem ascribesUnder_comp_some_apply L87–92

{α : Type u_1} {C : Type u_2} {c : C → α} {P : α → Set C} {A : Set C} {p : C} :

AscribesUnder A p (some ∘ c) (c p) P ↔ ∀ q ∈ A, q ∈ P (c q)

Built from