Free Indirect Discourse (FID) as Mixed Perspective

@cite{banfield-1982} @cite{schlenker-2004}

Free Indirect Discourse is a narrative mode where the narrator's voice and the character's perspective blend. The hallmark of FID is that different context coordinates come from different sources:

• Agent: narrator (origin) — the narrator is "telling"
• Time/World/Position: character (local) — evaluated from the character's temporal and spatial perspective

This module formalizes FID as an FIDProfile: a per-coordinate depth specification over the context tower. Classic FID, direct speech, and indirect speech are all instances of this type, differing only in which coordinates read from origin vs local.

Key Definitions

• FIDProfile: Per-coordinate depth specification
• classicFID: Agent from origin, time/world/position from local
• directSpeech: All coordinates from local (full perspective shift)
• indirectSpeech: All coordinates from origin (no perspective shift)
• fid_is_mixed: FID is neither pure origin nor pure local access

structure Semantics.Reference.FreeIndirectDiscourse.FIDProfile : Type

Per-coordinate depth specification for mixed-perspective phenomena.

Each coordinate of the context (agent, time, world, position) gets its own DepthSpec, allowing fine-grained control over which tower layer each coordinate reads.

• agentDepth : Core.Context.DepthSpec

  Which depth to read the agent from

• timeDepth : Core.Context.DepthSpec

  Which depth to read the time from

• worldDepth : Core.Context.DepthSpec

  Which depth to read the world from

• positionDepth : Core.Context.DepthSpec

  Which depth to read the position from

instance Semantics.Reference.FreeIndirectDiscourse.instDecidableEqFIDProfile : DecidableEq FIDProfile

Equations

• Semantics.Reference.FreeIndirectDiscourse.instDecidableEqFIDProfile = Semantics.Reference.FreeIndirectDiscourse.instDecidableEqFIDProfile.decEq

def Semantics.Reference.FreeIndirectDiscourse.instDecidableEqFIDProfile.decEq (x✝ x✝¹ : FIDProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Reference.FreeIndirectDiscourse.instReprFIDProfile : Repr FIDProfile

Equations

• Semantics.Reference.FreeIndirectDiscourse.instReprFIDProfile = { reprPrec := Semantics.Reference.FreeIndirectDiscourse.instReprFIDProfile.repr }

def Semantics.Reference.FreeIndirectDiscourse.instReprFIDProfile.repr : FIDProfile → ℕ → Std.Format

Equations

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

def Semantics.Reference.FreeIndirectDiscourse.instBEqFIDProfile.beq : FIDProfile → FIDProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Reference.FreeIndirectDiscourse.instBEqFIDProfile.beq x✝¹ x✝ = false

instance Semantics.Reference.FreeIndirectDiscourse.instBEqFIDProfile : BEq FIDProfile

Equations

• Semantics.Reference.FreeIndirectDiscourse.instBEqFIDProfile = { beq := Semantics.Reference.FreeIndirectDiscourse.instBEqFIDProfile.beq }

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.resolveAgent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : FIDProfile) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : E

Resolve the agent coordinate from the tower according to this profile.

Equations

• p.resolveAgent t = (t.contextAt (p.agentDepth.resolve t.depth)).agent

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.resolveTime {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : FIDProfile) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : T

Resolve the time coordinate from the tower according to this profile.

Equations

• p.resolveTime t = (t.contextAt (p.timeDepth.resolve t.depth)).time

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.resolveWorld {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : FIDProfile) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : W

Resolve the world coordinate from the tower according to this profile.

Equations

• p.resolveWorld t = (t.contextAt (p.worldDepth.resolve t.depth)).world

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.resolvePosition {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : FIDProfile) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : P

Resolve the position coordinate from the tower according to this profile.

Equations

• p.resolvePosition t = (t.contextAt (p.positionDepth.resolve t.depth)).position

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.resolve {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : FIDProfile) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : Core.Context.KContext W E P T

Resolve all coordinates into a full KContext.

Addressee tracks agentDepth — it reads from the same tower layer as the agent. This reflects the linguistic convention that addressee and agent are co-determined by the same speech-act context: if you shift who the speaker is, you also shift who they're speaking to. No attested phenomenon requires independent depth control for addressee.

Equations

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

def Semantics.Reference.FreeIndirectDiscourse.FIDProfile.isUniform (p : FIDProfile) : Bool

A profile is uniform iff all coordinates read from the same depth.

Equations

• p.isUniform = (p.agentDepth == p.timeDepth && p.timeDepth == p.worldDepth && p.worldDepth == p.positionDepth)

def Semantics.Reference.FreeIndirectDiscourse.classicFID : FIDProfile

Classic FID: narrator's voice (agent from origin) combined with character's perspective (time, world, position from local).

"She was happy now. Tomorrow she would leave."

• "she" = narrator's third-person reference (agent from origin)
• "now", "tomorrow" = character's temporal perspective (time from local)
• The world is the character's belief/experience world

Equations

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

def Semantics.Reference.FreeIndirectDiscourse.directSpeech : FIDProfile

Direct speech: all coordinates from the local (shifted) context. The embedded clause is fully evaluated from the reported speaker's perspective.

"John said: 'I am happy here now.'"

• "I" = John, "here" = John's location, "now" = John's time

Equations

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

def Semantics.Reference.FreeIndirectDiscourse.indirectSpeech : FIDProfile

Indirect speech: all coordinates from the origin (speech-act context). Standard Kaplanian interpretation — no perspective shift.

"John said that I am happy here now."

• "I" = actual speaker, "here" = actual location, "now" = actual time

Equations

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

theorem Semantics.Reference.FreeIndirectDiscourse.directSpeech_uniform : directSpeech.isUniform = true

Direct speech is uniform: all coordinates read from the same depth.

theorem Semantics.Reference.FreeIndirectDiscourse.indirectSpeech_uniform : indirectSpeech.isUniform = true

Indirect speech is uniform: all coordinates read from the same depth.

theorem Semantics.Reference.FreeIndirectDiscourse.classicFID_not_uniform : classicFID.isUniform = false

FID is NOT uniform: agent reads from a different depth than time.

theorem Semantics.Reference.FreeIndirectDiscourse.fid_is_mixed : classicFID ≠ directSpeech ∧ classicFID ≠ indirectSpeech

FID is mixed: it is neither pure origin-access nor pure local-access. The agent comes from origin but time comes from local.

theorem Semantics.Reference.FreeIndirectDiscourse.root_all_agree {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : classicFID.resolveAgent (Core.Context.ContextTower.root c) = indirectSpeech.resolveAgent (Core.Context.ContextTower.root c) ∧ classicFID.resolveAgent (Core.Context.ContextTower.root c) = directSpeech.resolveAgent (Core.Context.ContextTower.root c)

In a root tower (no embedding), all three profiles agree: they all resolve to the same context.

theorem Semantics.Reference.FreeIndirectDiscourse.fid_vs_direct_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) (character : E) (charTime : T) (charWorld : W) (hDiff : c.agent ≠ character) : have t := (Core.Context.ContextTower.root c).push (Core.Context.perspectiveShift character charTime charWorld); classicFID.resolveAgent t ≠ directSpeech.resolveAgent t

Under a perspective shift, FID's agent differs from direct speech's agent: FID reads the narrator (origin), direct speech reads the character (local).