Person Features as Presuppositions

@cite{schlenker-2003}

@cite{schlenker-2003}'s MELP (Monstrous Egli Language with Presuppositions) treats person features as presuppositions on the context:

• +author*(x): x is the agent of the utterance context c*
• +author(x, cᵢ): x is the agent of context cᵢ (at tower depth i)

Logophoric pronouns are then derived as +author(x, cᵢ) ∧ −author*(x): the referent is the agent of an embedded context but NOT the actual speaker.

Key Definitions

• PersonFeature: a presuppositional constraint parameterized by tower depth
• authorAt: +author(x, d) — x is the agent at depth d
• authorStar: +author*(x) = authorAt .origin
• isLogophoric: +author(x, cᵢ) ∧ −author*(x)

Key Results

• authorStar_root: in a root tower, +author* checks against the origin agent
• authorLocal_shifted: under attitude shift, +author(local) picks out the holder
• logophoric_refers_to_holder: logophoric pronouns refer to the attitude holder when the holder differs from the speaker
• speaker_not_logophoric: the actual speaker never satisfies the logophoric condition

structure Semantics.Reference.PersonFeatures.PersonFeature (W : Type u_5) (E : Type u_6) (P : Type u_7) (T : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

A person feature: a presuppositional constraint on which entity can serve as the referent of a pronoun, parameterized by which context layer the feature refers to.

In @cite{schlenker-2003}'s MELP, person features are presuppositions of the form "+F(x, c)" where F is a feature (author, hearer), x is the entity, and c is a context variable bound by an attitude operator.

• depth : Core.Context.DepthSpec

  Which tower depth the feature refers to

• check : E → Core.Context.KContext W E P T → Bool

  The constraint: does entity x satisfy the feature relative to context c?

def Semantics.Reference.PersonFeatures.PersonFeature.eval {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (f : PersonFeature W E P T) (x : E) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : Bool

Evaluate a person feature against a tower: resolve the depth to a concrete context layer and check the constraint.

Equations

• f.eval x t = f.check x (t.contextAt (f.depth.resolve t.depth))

def Semantics.Reference.PersonFeatures.authorAt {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] (d : Core.Context.DepthSpec) : PersonFeature W E P T

+author(x, d): x is the agent of the context at depth d.

@cite{schlenker-2003}: "+author(x, cᵢ)" presupposes that x is the agent (speaker) of context cᵢ. In the tower framework, cᵢ is resolved by contextAt (d.resolve depth).

Equations

• Semantics.Reference.PersonFeatures.authorAt d = { depth := d, check := fun (x : E) (c : Core.Context.KContext W E P T) => x == c.agent }

def Semantics.Reference.PersonFeatures.authorStar {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] : PersonFeature W E P T

+author*(x) = +author(x, c*): x is the agent of the utterance context. The star notation indicates the utterance context (origin).

Using "I" presupposes that the referent is the actual speaker.

Equations

• Semantics.Reference.PersonFeatures.authorStar = Semantics.Reference.PersonFeatures.authorAt Core.Context.DepthSpec.origin

def Semantics.Reference.PersonFeatures.hearerAt {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] (d : Core.Context.DepthSpec) : PersonFeature W E P T

+hearer(x, d): x is the addressee of the context at depth d.

Using "you" presupposes that the referent is the addressee.

Equations

• Semantics.Reference.PersonFeatures.hearerAt d = { depth := d, check := fun (x : E) (c : Core.Context.KContext W E P T) => x == c.addressee }

def Semantics.Reference.PersonFeatures.hearerStar {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] : PersonFeature W E P T

+hearer*(x) = +hearer(x, c*): x is the addressee of the utterance context.

Equations

• Semantics.Reference.PersonFeatures.hearerStar = Semantics.Reference.PersonFeatures.hearerAt Core.Context.DepthSpec.origin

def Semantics.Reference.PersonFeatures.isLogophoric {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] (x : E) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (embeddedDepth : Core.Context.DepthSpec) : Bool

Logophoric pronoun condition: +author(x, cᵢ) ∧ −author*(x).

@cite{schlenker-2003} §6: logophoric pronouns in languages like Ewe are licensed in embedded clauses where x is the agent of the embedding context (attitude holder) but NOT the agent of the utterance context (actual speaker).

This formalizes the key insight: logophoric pronouns are derived from the interaction of two person features — one referring to an embedded context variable, one to the utterance context.

Equations

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

@[simp]

theorem Semantics.Reference.PersonFeatures.authorStar_root {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] (x : E) (c : Core.Context.KContext W E P T) : authorStar.eval x (Core.Context.ContextTower.root c) = (x == c.agent)

In a root tower, +author* checks against the origin agent.

theorem Semantics.Reference.PersonFeatures.authorLocal_shifted {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] [LawfulBEq E] (holder : E) (w' : W) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : (authorAt Core.Context.DepthSpec.local).eval holder (t.push (Core.Context.attitudeShift holder w')) = true

Under an attitude shift, +author(x, local) is satisfied when x is the attitude holder.

theorem Semantics.Reference.PersonFeatures.logophoric_refers_to_holder {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] [LawfulBEq E] (holder : E) (w' : W) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (hDiff : (holder == t.origin.agent) = false) : isLogophoric holder (t.push (Core.Context.attitudeShift holder w')) Core.Context.DepthSpec.local = true

A logophoric pronoun refers to the attitude holder when the holder differs from the speaker.

Given: the speaker is the origin agent, and the holder ≠ speaker. Then under attitude shift, the holder satisfies +author(local) (they are the agent of the shifted context) and fails +author* (they are not the actual speaker).

theorem Semantics.Reference.PersonFeatures.speaker_not_logophoric {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [BEq E] [LawfulBEq E] (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (d : Core.Context.DepthSpec) : isLogophoric t.origin.agent t d = false

The actual speaker never satisfies the logophoric condition: +author* is always true for the origin agent, so −author* blocks logophoricity.

This is why logophoric pronouns are restricted to embedded contexts — the actual speaker cannot be logophoric in their own utterance.