De re attitudes by acquaintance

This file defines the centered-world rule for de re attitude ascription. The object of an attitude is a centered proposition — a property of the holder's self, now, and world — and a de re construal replaces the res by whatever the self is uniquely acquainted with, through a contextually given acquaintance relation, at the now of each alternative; the res itself enters only through the base-world condition that the holder actually bears the relation to it. With the identity relation on times the rule collapses to evaluation at the now, which is what makes the simultaneous reading of a past tense embedded under a past attitude a de re reading.

Main definitions

• Acquaintance.CenteredProp, Acquaintance.Rel: centered propositions and acquaintance relations to a res of any type.
• Acquaintance.deRe: the centered proposition ascribed by a de re construal.
• Acquaintance.BaseCondition: the base-world condition on the res.

Main statements

• Acquaintance.deRe_identity: de re construal through identity with the now evaluates the property at the now.

References

• [lewis-1979-attitudes]
• [cresswell-vonstechow-1982]
• [abusch-1997]

@[reducible, inline]

abbrev Acquaintance.CenteredProp (E : Type u_5) (T : Type u_6) (W : Type u_7) : Type (max (max u_5 u_6) u_7)

A centered proposition: a property of the holder's self, now, and world.

Equations

• Acquaintance.CenteredProp E T W = (E → T → W → Prop)

@[reducible, inline]

abbrev Acquaintance.Rel (α : Type u_5) (E : Type u_6) (T : Type u_7) (W : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

An acquaintance relation: R y x t w holds when the self x at t in w is acquainted with the res y.

Equations

• Acquaintance.Rel α E T W = (α → E → T → W → Prop)

def Acquaintance.deRe {α : Type u_1} {E : Type u_2} {T : Type u_3} {W : Type u_4} (R : Rel α E T W) (P : α → T → W → Prop) : CenteredProp E T W

The centered proposition that the res the self is uniquely acquainted with at the now has the property P there.

Equations

• Acquaintance.deRe R P x t w = ∃ (y : α), (∀ (y' : α), R y' x t w ↔ y' = y) ∧ P y t w

def Acquaintance.BaseCondition {α : Type u_1} {E : Type u_2} {T : Type u_3} {W : Type u_4} (R : Rel α E T W) (res : α) (x : E) (t : T) (w : W) : Prop

The base-world condition of a de re construal: the holder actually bears the acquaintance relation to the res.

Equations

• Acquaintance.BaseCondition R res x t w = R res x t w

def Acquaintance.identity {E : Type u_2} {T : Type u_3} {W : Type u_4} : Rel T E T W

Acquaintance with a time by identity with the now.

Equations

• Acquaintance.identity y x✝¹ t x✝ = (y = t)

theorem Acquaintance.deRe_identity {E : Type u_2} {T : Type u_3} {W : Type u_4} (P : T → T → W → Prop) : deRe identity P = fun (x : E) (t : T) (w : W) => P t t w