Configurational Point-of-View Roles

Formalizes [ST03]. Pragmatic roles (SPEAKER, HEARER, SEAT OF KNOWLEDGE) are configurationally determined by structural position in the Speech Act Phrase (SAP), not primitive. Four moods are derived from two binary features: [±finite] on the utterance content × whether the HEARER c-commands the content.

Key Claims

1. P-roles (SPEAKER, HEARER) are structural positions in SAP, not primitives.
2. 4 moods = 2×2 feature matrix: [±finite] × [±hearer-c-commands-content].
3. SEAT OF KNOWLEDGE is the highest argument of the Point-of-View domain (p.335): the HEARER exactly when the hearer c-commands the content. It is therefore derived from the same feature that drives deriveMood, not stipulated independently — so the matrix and the seat cannot disagree.
4. SAP is the highest phase → P-role resolution is root-only (invariant under context shift). Proved as resolvePRole_shift_invariant.

Connections

• Semantics/Context/Tower.lean: KContext.agent = SPEAKER, KContext.addressee = HEARER; P-roles resolve through the canonical Discourse.resolveRole over a ContextTower.
• Phase.lean: isPhaseHeadOf .SA — SAP is the highest phase.
• ExtendedProjection/Basic.lean: fValue .SA = 7 > fValue .C = 6.
• Semantics/Mood/ClauseType.lean: the configurational seat-of-knowledge diverges from Lakoff's deontic moodAuthority on imperatives (seatOfKnowledge_diverges_from_authority_on_imperative).
• Semantics/Epistemicity.lean: EvalP-spec → EpistemicProfile.authority, EvidP-spec → EpistemicProfile.source; S&T's seat is the speech-act- participant restriction of EpistemicAuthority (seat_never_nonparticipant).

S&T call SAP "the maximal structure"; the "highest phase" framing here is the formaliser's modernization.

Pragmatic roles

inductive SpeasTenny2003.PRole : Type

Pragmatic roles determined by structural position in SAP.

[ST03]: these are NOT primitives — they are configurationally assigned by position in the Speech Act Phrase:

• SPEAKER = Spec-SAP (external argument of SA)
• HEARER = complement of SA (internal argument)
• SEAT OF KNOWLEDGE = varies by mood

• speaker : PRole
• hearer : PRole
• seatOfKnowledge : PRole

def SpeasTenny2003.instReprPRole.repr : PRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SpeasTenny2003.instReprPRole : Repr PRole

Equations

• SpeasTenny2003.instReprPRole = { reprPrec := SpeasTenny2003.instReprPRole.repr }

@[implicit_reducible]

instance SpeasTenny2003.instDecidableEqPRole : DecidableEq PRole

Equations

• SpeasTenny2003.instDecidableEqPRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

SAP mood — the 2×2 feature matrix

inductive SpeasTenny2003.SAPMood : Type

Speas & Tenny's central result: 4 sentence moods from 2 binary features.

contentFinite	hearerCCommands	Mood
true	false	declarative
true	true	interrogative
false	true	imperative
false	false	subjunctive

• declarative : SAPMood
• interrogative : SAPMood
• imperative : SAPMood
• subjunctive : SAPMood

@[implicit_reducible]

instance SpeasTenny2003.instReprSAPMood : Repr SAPMood

Equations

• SpeasTenny2003.instReprSAPMood = { reprPrec := SpeasTenny2003.instReprSAPMood.repr }

def SpeasTenny2003.instReprSAPMood.repr : SAPMood → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SpeasTenny2003.instDecidableEqSAPMood : DecidableEq SAPMood

Equations

• SpeasTenny2003.instDecidableEqSAPMood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SpeasTenny2003.deriveMood (contentFinite hearerCCommandsContent : Bool) : SAPMood

Derive mood from the two binary features.

Equations

• SpeasTenny2003.deriveMood true false = SpeasTenny2003.SAPMood.declarative
• SpeasTenny2003.deriveMood true true = SpeasTenny2003.SAPMood.interrogative
• SpeasTenny2003.deriveMood false true = SpeasTenny2003.SAPMood.imperative
• SpeasTenny2003.deriveMood false false = SpeasTenny2003.SAPMood.subjunctive

def SpeasTenny2003.SAPMood.contentFinite : SAPMood → Bool

Feature 1 (subcategorization-like): is the utterance content finite? (A genuine two-valued morphosyntactic feature value, not a predicate.)

Equations

• SpeasTenny2003.SAPMood.declarative.contentFinite = true
• SpeasTenny2003.SAPMood.interrogative.contentFinite = true
• SpeasTenny2003.SAPMood.imperative.contentFinite = false
• SpeasTenny2003.SAPMood.subjunctive.contentFinite = false

def SpeasTenny2003.SAPMood.hearerCCommandsContent : SAPMood → Bool

Feature 2 (spec-head / promotion): does the HEARER c-command the content? True for interrogatives/imperatives (hearer promoted), false otherwise.

Equations

• SpeasTenny2003.SAPMood.interrogative.hearerCCommandsContent = true
• SpeasTenny2003.SAPMood.imperative.hearerCCommandsContent = true
• SpeasTenny2003.SAPMood.declarative.hearerCCommandsContent = false
• SpeasTenny2003.SAPMood.subjunctive.hearerCCommandsContent = false

theorem SpeasTenny2003.deriveMood_features (m : SAPMood) : deriveMood m.contentFinite m.hearerCCommandsContent = m

The 2×2 matrix is a genuine bijection (left inverse): recovering the two features of a mood and re-deriving returns the same mood.

theorem SpeasTenny2003.features_deriveMood (f h : Bool) : (deriveMood f h).contentFinite = f ∧ (deriveMood f h).hearerCCommandsContent = h

The 2×2 matrix is a genuine bijection (right inverse): every feature pair is recovered from its derived mood. Together with deriveMood_features this shows the four moods exhaust Bool × Bool bijectively (replacing the vacuous "exhaustiveness" claim — every total map into a 4-constructor type is "exhaustive").

Bridge to ClauseType

def SpeasTenny2003.SAPMood.toClauseType : SAPMood → Semantics.Mood.ClauseType

Map configurational mood to a framework-agnostic ClauseType (illocutionary force × grammatical mood).

The four mappings:

• .declarative → ⟨declarative, indicative⟩
• .interrogative → ⟨interrogative, indicative⟩
• .imperative → ⟨imperative, indicative⟩ (mood often neutralized)
• .subjunctive → ⟨declarative, subjunctive⟩

The subjunctive mapping is a lossy placeholder: IllocutionaryMood has no token for S&T's configurational subjunctive (Latin promise/wish/jussive; the speaker is "responsible for choosing the preferred world", p.335), so the force component falls back to .declarative. (The earlier .promissive mapping was wrong in the other direction — it conflated S&T's terminology with Searle's commissive class.) .exclamative has no SAPMood counterpart (exclamatives are not derived in the 2×2 matrix).

Equations

• SpeasTenny2003.SAPMood.declarative.toClauseType = { force := Semantics.Mood.IllocutionaryMood.declarative, mood := Semantics.Mood.GramMood.indicative }
• SpeasTenny2003.SAPMood.interrogative.toClauseType = { force := Semantics.Mood.IllocutionaryMood.interrogative, mood := Semantics.Mood.GramMood.indicative }
• SpeasTenny2003.SAPMood.imperative.toClauseType = { force := Semantics.Mood.IllocutionaryMood.imperative, mood := Semantics.Mood.GramMood.indicative }
• SpeasTenny2003.SAPMood.subjunctive.toClauseType = { force := Semantics.Mood.IllocutionaryMood.declarative, mood := Semantics.Mood.GramMood.subjunctive }

def SpeasTenny2003.SAPMood.toForce (m : SAPMood) : Semantics.Mood.IllocutionaryMood

Convenience projection: SAPMood's illocutionary force component.

Equations

• m.toForce = m.toClauseType.force

Seat of knowledge (derived)

def SpeasTenny2003.seatOfKnowledge (m : SAPMood) : PRole

The SEAT OF KNOWLEDGE is the highest argument of the Point-of-View domain ([ST03] p.335: "the seat of knowledge is controlled by the highest argument"), which is the HEARER exactly when the hearer c-commands the utterance content. Derived from hearerCCommandsContent — the same feature that drives deriveMood — so the seat cannot disagree with the matrix:

• declarative → speaker (content c-commands hearer)
• interrogative → hearer (hearer promoted, c-commands content)
• imperative → hearer (passive-like promotion; the hearer is responsible for realizing the unrealized proposition, p.335)
• subjunctive → speaker (speaker is highest; responsible for the preferred world)

Equations

• SpeasTenny2003.seatOfKnowledge m = if m.hearerCCommandsContent = true then SpeasTenny2003.PRole.hearer else SpeasTenny2003.PRole.speaker

def SpeasTenny2003.PRole.toDiscourseRole : PRole → Discourse.DiscourseRole

Map P-roles to framework-agnostic discourse roles. SPEAKER → speaker, HEARER → addressee, SEAT OF KNOWLEDGE → speaker (default; use seatOfKnowledge for mood-sensitive resolution).

Equations

• SpeasTenny2003.PRole.speaker.toDiscourseRole = Discourse.DiscourseRole.speaker
• SpeasTenny2003.PRole.hearer.toDiscourseRole = Discourse.DiscourseRole.addressee
• SpeasTenny2003.PRole.seatOfKnowledge.toDiscourseRole = Discourse.DiscourseRole.speaker

def SpeasTenny2003.PRole.toEpistemicAuthority : PRole → Semantics.Epistemicity.EpistemicAuthority

Map P-roles to egophoric EpistemicAuthority ([Tou08], [Flo18]): SPEAKER → ego, HEARER → allocutive, SEAT OF KNOWLEDGE → ego (default). The image never includes .nonparticipant.

Equations

• SpeasTenny2003.PRole.speaker.toEpistemicAuthority = Semantics.Epistemicity.EpistemicAuthority.ego
• SpeasTenny2003.PRole.hearer.toEpistemicAuthority = Semantics.Epistemicity.EpistemicAuthority.allocutive
• SpeasTenny2003.PRole.seatOfKnowledge.toEpistemicAuthority = Semantics.Epistemicity.EpistemicAuthority.ego

theorem SpeasTenny2003.seatOfKnowledge_diverges_from_authority_on_imperative : (seatOfKnowledge SAPMood.imperative).toDiscourseRole ≠ SAPMood.imperative.toClauseType.authority

Divergence (the empirical content). S&T's configurational seat-of-knowledge and Lakoff's deontic moodAuthority ([Lak70], via ClauseType.authority) DISAGREE on imperatives: S&T locate the seat with the HEARER (who must realize the unrealized proposition, p.335), Lakoff with the SPEAKER (who has authority to command).

theorem SpeasTenny2003.seatOfKnowledge_agrees_with_authority_off_imperative (m : SAPMood) (h : m ≠ SAPMood.imperative) : (seatOfKnowledge m).toDiscourseRole = m.toClauseType.authority

Off imperatives the two notions agree: declarative/subjunctive → speaker, interrogative → addressee. The disagreement is isolated to imperatives.

Context grounding

def SpeasTenny2003.resolvePRole {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (r : PRole) : E

Resolve a P-role to a discourse participant through a ContextTower, reusing the canonical Discourse.resolveRole (which reads from the speech-act origin). SEAT OF KNOWLEDGE resolves through its default discourse role; use resolvePRoleInMood for mood-sensitive resolution.

Equations

• SpeasTenny2003.resolvePRole tower r = Discourse.resolveRole tower r.toDiscourseRole

def SpeasTenny2003.resolvePRoleInMood {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (m : SAPMood) : PRole → E

Mood-sensitive role resolution: SEAT OF KNOWLEDGE is resolved through seatOfKnowledge before mapping to a participant.

Equations

• SpeasTenny2003.resolvePRoleInMood tower m SpeasTenny2003.PRole.seatOfKnowledge = SpeasTenny2003.resolvePRole tower (SpeasTenny2003.seatOfKnowledge m)
• SpeasTenny2003.resolvePRoleInMood tower m x✝ = SpeasTenny2003.resolvePRole tower x✝

theorem SpeasTenny2003.resolvePRole_speaker {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolvePRole tower PRole.speaker = tower.origin.agent

SPEAKER resolves to the speech-act origin's agent.

theorem SpeasTenny2003.resolvePRole_hearer {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolvePRole tower PRole.hearer = tower.origin.addressee

HEARER resolves to the speech-act origin's addressee.

theorem SpeasTenny2003.resolvePRole_shift_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (σ : Semantics.Context.ContextShift (Semantics.Context.KContext W E P T)) (r : PRole) : resolvePRole (tower.push σ) r = resolvePRole tower r

Key Claim 4 as a theorem. P-roles are resolved from the SPEECH-ACT context (SAP is the highest phase), so resolution is invariant under context shift / embedding — inherited from Discourse.resolveRole_shift_invariant.

theorem SpeasTenny2003.seatOfKnowledge_declarative_resolves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolvePRoleInMood tower SAPMood.declarative PRole.seatOfKnowledge = tower.origin.agent

In declaratives the seat of knowledge resolves to the speaker (agent).

theorem SpeasTenny2003.seatOfKnowledge_interrogative_resolves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolvePRoleInMood tower SAPMood.interrogative PRole.seatOfKnowledge = tower.origin.addressee

In interrogatives the seat of knowledge resolves to the hearer (addressee).

theorem SpeasTenny2003.seatOfKnowledge_imperative_resolves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : resolvePRoleInMood tower SAPMood.imperative PRole.seatOfKnowledge = tower.origin.addressee

In imperatives the seat of knowledge resolves to the hearer (addressee) — the corrected value (p.335), where the hearer realizes the proposition.

SAP as a phase, and the F-hierarchy

theorem SpeasTenny2003.sa_is_phase_head (so : Minimalist.SyntacticObject) (h : Minimalist.SO.outerCatC so = some Minimalist.Cat.SA) : Minimalist.isPhaseHeadOf Minimalist.Cat.SA so = true

SA is a phase head: if the syntactic object's head category is SA, then isPhaseHeadOf .SA holds.

theorem SpeasTenny2003.sa_phase_derivation_final : Minimalist.isPhaseHeadOf Minimalist.Cat.SA (Minimalist.SO.mkLeaf Minimalist.Cat.SA [] 0) = true

SAP is derivation-final (the highest phase).

theorem SpeasTenny2003.sa_outranks_c : Minimalist.fValue Minimalist.Cat.SA > Minimalist.fValue Minimalist.Cat.C

SAP outranks CP on the extended-projection F-hierarchy (fValue .SA = 7 > fValue .C = 6): the speech-act layer sits above the complementizer layer. (fValue is globally non-injective — T/Neg/Pol all share F2 — so the only S&T-relevant fact is this pairwise inequality.)

Person → P-role mapping

def SpeasTenny2003.personToRole : Person → Option PRole

Map grammatical person to SAP P-role.

1st person → SPEAKER (Spec-SAP) 2nd person → HEARER (complement of SA) 3rd person / zero → neither (referential, not a discourse role)

Equations

• SpeasTenny2003.personToRole Person.first = some SpeasTenny2003.PRole.speaker
• SpeasTenny2003.personToRole Person.firstInclusive = some SpeasTenny2003.PRole.speaker
• SpeasTenny2003.personToRole Person.firstExclusive = some SpeasTenny2003.PRole.speaker
• SpeasTenny2003.personToRole Person.second = some SpeasTenny2003.PRole.hearer
• SpeasTenny2003.personToRole Person.third = none
• SpeasTenny2003.personToRole Person.zero = none

def SpeasTenny2003.pronounDiscourseRole (p : PersonalPronoun) : Option PRole

Discourse role of a pronoun entry (theory-side, not baked into fragment). Determined entirely by the person feature.

Equations

• SpeasTenny2003.pronounDiscourseRole p = p.person.bind SpeasTenny2003.personToRole

theorem SpeasTenny2003.first_person_are_speakers : pronounDiscourseRole English.Pronouns.i = some PRole.speaker ∧ pronounDiscourseRole English.Pronouns.me = some PRole.speaker ∧ pronounDiscourseRole English.Pronouns.we = some PRole.speaker ∧ pronounDiscourseRole English.Pronouns.us = some PRole.speaker

theorem SpeasTenny2003.second_person_are_hearers : pronounDiscourseRole English.Pronouns.you = some PRole.hearer ∧ pronounDiscourseRole English.Pronouns.you_pl = some PRole.hearer

theorem SpeasTenny2003.third_person_no_role : pronounDiscourseRole English.Pronouns.he = none ∧ pronounDiscourseRole English.Pronouns.she = none ∧ pronounDiscourseRole English.Pronouns.it = none

theorem SpeasTenny2003.discourse_role_from_person (p : PersonalPronoun) (per : Person) (hp : p.person = some per) : pronounDiscourseRole p = personToRole per

Discourse role is determined entirely by the person feature.

Sentience domain ([ST03] §2)

inductive SpeasTenny2003.SentienceProjection : Type

Functional projections in the Sentience Domain.

Below SAP, the Sentience Domain mediates between the speech-act layer and propositional content. It hosts two projections:

• EvalP (Evaluation Phrase): specifier = SEAT OF KNOWLEDGE, the sentient mind that evaluates the proposition's truth.
• EvidP (Evidential Phrase): specifier = EVIDENCE, the type of evidence supporting the evaluation.

Sentience Phrase (structure 34): EvalP > EvidP > S(episP); the SAP scopes above it (p.333), so overall SAP > EvalP > EvidP > S. (S&T label the base S(episP); equating it with TP is the formaliser's gloss.)

The Sentience Domain captures "judgements and evaluations by a sentient mind on the truth-value of the proposition" (p.333).

Cross-framework note: the canonical Cat.Evid of the extended projection is Cinque's evaluative/evidential head at F-level 2 (above T, below Fin) — structurally lower than S&T's EvidP, which sits in the Sentience Domain just above TP. Two cited evidential projections at different heights.

• EvidP : SentienceProjection
• EvalP : SentienceProjection

@[implicit_reducible]

instance SpeasTenny2003.instDecidableEqSentienceProjection : DecidableEq SentienceProjection

Equations

• SpeasTenny2003.instDecidableEqSentienceProjection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance SpeasTenny2003.instReprSentienceProjection : Repr SentienceProjection

Equations

• SpeasTenny2003.instReprSentienceProjection = { reprPrec := SpeasTenny2003.instReprSentienceProjection.repr }

def SpeasTenny2003.instReprSentienceProjection.repr : SentienceProjection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance SpeasTenny2003.instFintypeSentienceProjection : Fintype SentienceProjection

Equations

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

def SpeasTenny2003.SentienceProjection.rank : SentienceProjection → ℕ

Rank ordering of Sentience Domain projections: EvidP < EvalP < SAP.

Equations

• SpeasTenny2003.SentienceProjection.EvidP.rank = 0
• SpeasTenny2003.SentienceProjection.EvalP.rank = 1

theorem SpeasTenny2003.rank_injective : Function.Injective SentienceProjection.rank

The rank function is injective: distinct projections have distinct ranks.

@[reducible, inline]

abbrev SpeasTenny2003.evalPSpecifier : SAPMood → PRole

The specifier of EvalP hosts a P-role: SEAT OF KNOWLEDGE (the sentient mind performing the evaluation), same as seatOfKnowledge.

Equations

• SpeasTenny2003.evalPSpecifier = SpeasTenny2003.seatOfKnowledge

@[reducible, inline]

abbrev SpeasTenny2003.EvidPSpecifier : Type

The specifier of EvidP hosts the evidence type, mapped to the framework-agnostic CoarseSource of Features/Evidentiality.lean (direct / inference / hearsay). NB this three-way coarsening merges S&T's top tier (personal experience) into "direct"; the paper's full evidence hierarchy is personal experience ≫ direct ≫ indirect ≫ hearsay (p.327).

Equations

• SpeasTenny2003.EvidPSpecifier = Features.Evidentiality.CoarseSource

def SpeasTenny2003.sentienceProfile (m : SAPMood) (ev : EvidPSpecifier) : Semantics.Epistemicity.EpistemicProfile

Real bridge to Semantics/Epistemicity.lean. The Sentience Domain's two specifiers ARE the two main fields of an EpistemicProfile: EvalP-spec (SEAT OF KNOWLEDGE) → authority, EvidP-spec (EVIDENCE) → source. The structural hierarchy EvalP > EvidP corresponds to authority scoping over source.

Equations

• SpeasTenny2003.sentienceProfile m ev = { source := ev, authority := (SpeasTenny2003.evalPSpecifier m).toEpistemicAuthority }

@[simp]

theorem SpeasTenny2003.sentienceProfile_source (m : SAPMood) (ev : EvidPSpecifier) : (sentienceProfile m ev).source = ev

The EvidP specifier IS the profile's evidential source (shared CoarseSource).

@[simp]

theorem SpeasTenny2003.sentienceProfile_authority (m : SAPMood) (ev : EvidPSpecifier) : (sentienceProfile m ev).authority = (evalPSpecifier m).toEpistemicAuthority

The EvalP specifier's epistemic authority IS the profile's authority.

theorem SpeasTenny2003.seat_never_nonparticipant (m : SAPMood) : (evalPSpecifier m).toEpistemicAuthority ≠ Semantics.Epistemicity.EpistemicAuthority.nonparticipant

Asymmetry made visible. S&T's two-participant seat-of-knowledge never projects .nonparticipant authority, which the egophoric inventory ([Tou08], [Flo18]) carries for third-party access. S&T's role space is the speech-act-participant restriction of EpistemicAuthority.