Configurational Point-of-View Roles

Pragmatic roles (SPEAKER, HEARER, SEAT OF KNOWLEDGE) are configurationally determined by structural position in SAP, not primitive. Four moods derived from 2 binary features: [±finite] on utterance content × whether HEARER c-commands 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 shifts by mood (speaker in decl, hearer in interrog)
4. SAP is the highest phase → P-roles root-only

Connections

• Core/Context.lean: KContext.agent = SPEAKER, KContext.addressee = HEARER
• Phase.lean: isPhaseHeadOf .SA — SAP is highest phase
• Allocutivity.lean: sa_based_aa_root_only — root-only from SAP phase
• LeftPeriphery.lean: rogativeSAP — "ask" selects full SAP with P-roles
• ExtendedProjection/Basic.lean: fValue.SA = 7 > fValue.C = 6
• RSA/YoonEtAl2020: HEARER (structural) ↔ addressee in social utility

inductive Minimalist.SpeechActs.PRole : Type

Pragmatic roles determined by structural position in SAP.

@cite{speas-tenny-2003}: 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

@[implicit_reducible]

instance Minimalist.SpeechActs.instReprPRole : Repr PRole

Equations

• Minimalist.SpeechActs.instReprPRole = { reprPrec := Minimalist.SpeechActs.instReprPRole.repr }

def Minimalist.SpeechActs.instReprPRole.repr : PRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.SpeechActs.instDecidableEqPRole : DecidableEq PRole

Equations

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

inductive Minimalist.SpeechActs.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

def Minimalist.SpeechActs.instReprSAPMood.repr : SAPMood → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.SpeechActs.instReprSAPMood : Repr SAPMood

Equations

• Minimalist.SpeechActs.instReprSAPMood = { reprPrec := Minimalist.SpeechActs.instReprSAPMood.repr }

@[implicit_reducible]

instance Minimalist.SpeechActs.instDecidableEqSAPMood : DecidableEq SAPMood

Equations

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

def Minimalist.SpeechActs.deriveMood (contentFinite hearerCCommandsContent : Bool) : SAPMood

Derive mood from the two binary features.

Equations

• Minimalist.SpeechActs.deriveMood true false = Minimalist.SpeechActs.SAPMood.declarative
• Minimalist.SpeechActs.deriveMood true true = Minimalist.SpeechActs.SAPMood.interrogative
• Minimalist.SpeechActs.deriveMood false true = Minimalist.SpeechActs.SAPMood.imperative
• Minimalist.SpeechActs.deriveMood false false = Minimalist.SpeechActs.SAPMood.subjunctive

def Minimalist.SpeechActs.SAPMood.toClauseType : SAPMood → Core.Mood.ClauseType

Map configurational mood to a framework-agnostic ClauseType (illocutionary force × grammatical mood). S&T's .subjunctive is configurational [-finite, hearer does NOT c-command content]; its closest framework-agnostic match is a declarative-subjunctive clause, NOT the illocutionary .promissive (a previous mapping that conflated S&T's terminology with Searle's commissive class).

The four mappings:

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

.exclamative has no SAPMood counterpart (exclamatives are not derived in S&T's 2×2 matrix).

Equations

• Minimalist.SpeechActs.SAPMood.declarative.toClauseType = { force := Core.Mood.IllocutionaryMood.declarative, mood := Core.Mood.GramMood.indicative }
• Minimalist.SpeechActs.SAPMood.interrogative.toClauseType = { force := Core.Mood.IllocutionaryMood.interrogative, mood := Core.Mood.GramMood.indicative }
• Minimalist.SpeechActs.SAPMood.imperative.toClauseType = { force := Core.Mood.IllocutionaryMood.imperative, mood := Core.Mood.GramMood.indicative }
• Minimalist.SpeechActs.SAPMood.subjunctive.toClauseType = { force := Core.Mood.IllocutionaryMood.declarative, mood := Core.Mood.GramMood.subjunctive }

def Minimalist.SpeechActs.SAPMood.toForce (m : SAPMood) : Core.Mood.IllocutionaryMood

Convenience projection: SAPMood's illocutionary force component.

Equations

• m.toForce = m.toClauseType.force

def Minimalist.SpeechActs.seatOfKnowledge : SAPMood → PRole

The SEAT OF KNOWLEDGE role shifts by mood.

In declaratives, the speaker holds knowledge of the content. In interrogatives, the hearer is assumed to have knowledge. In imperatives and subjunctives, the speaker determines the desired action.

Equations

• Minimalist.SpeechActs.seatOfKnowledge Minimalist.SpeechActs.SAPMood.declarative = Minimalist.SpeechActs.PRole.speaker
• Minimalist.SpeechActs.seatOfKnowledge Minimalist.SpeechActs.SAPMood.interrogative = Minimalist.SpeechActs.PRole.hearer
• Minimalist.SpeechActs.seatOfKnowledge Minimalist.SpeechActs.SAPMood.imperative = Minimalist.SpeechActs.PRole.speaker
• Minimalist.SpeechActs.seatOfKnowledge Minimalist.SpeechActs.SAPMood.subjunctive = Minimalist.SpeechActs.PRole.speaker

def Minimalist.SpeechActs.PRole.toDiscourseRole : PRole → Core.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

• Minimalist.SpeechActs.PRole.speaker.toDiscourseRole = Core.Discourse.DiscourseRole.speaker
• Minimalist.SpeechActs.PRole.hearer.toDiscourseRole = Core.Discourse.DiscourseRole.addressee
• Minimalist.SpeechActs.PRole.seatOfKnowledge.toDiscourseRole = Core.Discourse.DiscourseRole.speaker

theorem Minimalist.SpeechActs.seat_of_knowledge_agrees_with_mood_authority (m : SAPMood) : (seatOfKnowledge m).toDiscourseRole = m.toClauseType.authority

seatOfKnowledge (Speas & Tenny, configurational) agrees with ClauseType.authority (Core/Mood/ClauseType.lean, framework-agnostic) via the toClauseType bridge. Both encode the same generalization: declarative/imperative/subjunctive → speaker, interrogative → addressee.

def Minimalist.SpeechActs.resolveRole {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : PRole → E

Resolve a P-role to a discourse participant via KContext.

SPEAKER = context agent, HEARER = context addressee. SEAT OF KNOWLEDGE defaults to agent (use resolveRoleInMood for mood-sensitive resolution).

Equations

• Minimalist.SpeechActs.resolveRole ctx Minimalist.SpeechActs.PRole.speaker = ctx.agent
• Minimalist.SpeechActs.resolveRole ctx Minimalist.SpeechActs.PRole.hearer = ctx.addressee
• Minimalist.SpeechActs.resolveRole ctx Minimalist.SpeechActs.PRole.seatOfKnowledge = ctx.agent

def Minimalist.SpeechActs.resolveRoleInMood {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.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 KContext participant.

Equations

• Minimalist.SpeechActs.resolveRoleInMood ctx m Minimalist.SpeechActs.PRole.seatOfKnowledge = Minimalist.SpeechActs.resolveRole ctx (Minimalist.SpeechActs.seatOfKnowledge m)
• Minimalist.SpeechActs.resolveRoleInMood ctx m x✝ = Minimalist.SpeechActs.resolveRole ctx x✝

theorem Minimalist.SpeechActs.deriveMood_exhaustive (f h : Bool) : deriveMood f h = SAPMood.declarative ∨ deriveMood f h = SAPMood.interrogative ∨ deriveMood f h = SAPMood.imperative ∨ deriveMood f h = SAPMood.subjunctive

theorem Minimalist.SpeechActs.declarative_speaker_knows : seatOfKnowledge SAPMood.declarative = PRole.speaker

theorem Minimalist.SpeechActs.interrogative_hearer_knows : seatOfKnowledge SAPMood.interrogative = PRole.hearer

theorem Minimalist.SpeechActs.speaker_is_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : resolveRole ctx PRole.speaker = ctx.agent

theorem Minimalist.SpeechActs.hearer_is_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : resolveRole ctx PRole.hearer = ctx.addressee

theorem Minimalist.SpeechActs.deriveMood_finite : deriveMood true false = SAPMood.declarative ∧ deriveMood true true = SAPMood.interrogative

theorem Minimalist.SpeechActs.sa_is_phase_head (so : SyntacticObject) (h : HeadFunction.leftSpine.outerCat so = Cat.SA) : isPhaseHeadOf Cat.SA so = true

theorem Minimalist.SpeechActs.hearer_is_addressee_in_context {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : resolveRole ctx PRole.hearer = ctx.addressee ∧ resolveRole ctx PRole.speaker = ctx.agent

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

theorem Minimalist.SpeechActs.fValue_injective_on_canonical_verbal_spine (c1 c2 : Cat) (h1 : c1 ∈ Minimalist.SpeechActs.canonicalVerbalSpine✝) (h2 : c2 ∈ Minimalist.SpeechActs.canonicalVerbalSpine✝) (hf : fValue c1 = fValue c2) : c1 = c2

theorem Minimalist.SpeechActs.seat_of_knowledge_declarative {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : resolveRoleInMood ctx SAPMood.declarative PRole.seatOfKnowledge = ctx.agent

theorem Minimalist.SpeechActs.seat_of_knowledge_interrogative {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ctx : Core.Context.KContext W E P T) : resolveRoleInMood ctx SAPMood.interrogative PRole.seatOfKnowledge = ctx.addressee

def Minimalist.SpeechActs.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

• Minimalist.SpeechActs.personToRole UD.Person.first = some Minimalist.SpeechActs.PRole.speaker
• Minimalist.SpeechActs.personToRole UD.Person.second = some Minimalist.SpeechActs.PRole.hearer
• Minimalist.SpeechActs.personToRole UD.Person.third = none
• Minimalist.SpeechActs.personToRole UD.Person.zero = none

def Minimalist.SpeechActs.pronounDiscourseRole (p : Fragments.English.Pronouns.PronounEntry) : Option PRole

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

Equations

• Minimalist.SpeechActs.pronounDiscourseRole p = p.person.bind Minimalist.SpeechActs.personToRole

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

theorem Minimalist.SpeechActs.second_person_are_hearers : pronounDiscourseRole Fragments.English.Pronouns.you = some PRole.hearer ∧ pronounDiscourseRole Fragments.English.Pronouns.you_pl = some PRole.hearer

theorem Minimalist.SpeechActs.third_person_no_role : pronounDiscourseRole Fragments.English.Pronouns.he = none ∧ pronounDiscourseRole Fragments.English.Pronouns.she = none ∧ pronounDiscourseRole Fragments.English.Pronouns.it = none

theorem Minimalist.SpeechActs.discourse_role_from_person (p : Fragments.English.Pronouns.PronounEntry) (per : Person) (hp : p.person = some per) : pronounDiscourseRole p = personToRole per

Discourse role is determined entirely by person feature.

inductive Minimalist.SpeechActs.SentienceProjection : Type

Functional projections in the Sentience Domain.

Below SAP, the Sentience Domain mediates between the speech act layer and the 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.

Hierarchy (structure 34 in S&T):

SAP > EvalP > EvidP > episP (= TP)

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

• EvidP : SentienceProjection
• EvalP : SentienceProjection

@[implicit_reducible]

instance Minimalist.SpeechActs.instDecidableEqSentienceProjection : DecidableEq SentienceProjection

Equations

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

@[implicit_reducible]

instance Minimalist.SpeechActs.instReprSentienceProjection : Repr SentienceProjection

Equations

• Minimalist.SpeechActs.instReprSentienceProjection = { reprPrec := Minimalist.SpeechActs.instReprSentienceProjection.repr }

def Minimalist.SpeechActs.instReprSentienceProjection.repr : SentienceProjection → ℕ → Std.Format

Equations

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

def Minimalist.SpeechActs.SentienceProjection.rank : SentienceProjection → ℕ

Rank ordering of Sentience Domain projections. EvidP < EvalP < SAP (the SAP itself is above the Sentience Domain).

Equations

• Minimalist.SpeechActs.SentienceProjection.EvidP.rank = 0
• Minimalist.SpeechActs.SentienceProjection.EvalP.rank = 1

theorem Minimalist.SpeechActs.rank_injective : Function.Injective SentienceProjection.rank

The rank function on the Sentience Domain is injective: distinct projections (EvidP, EvalP) have distinct ranks (0, 1).

def Minimalist.SpeechActs.evalPSpecifier : SAPMood → PRole

The specifier of EvalP hosts a P-role: SEAT OF KNOWLEDGE.

This is the sentient mind performing the evaluation. In declaratives, this is the SPEAKER; in interrogatives, the HEARER (same as seatOfKnowledge, since EvalP is where the seat is structurally projected).

Equations

• Minimalist.SpeechActs.evalPSpecifier = Minimalist.SpeechActs.seatOfKnowledge

@[reducible, inline]

abbrev Minimalist.SpeechActs.EvidPSpecifier : Type

The specifier of EvidP hosts the evidence type.

Maps S&T's EVIDENCE argument to the framework-agnostic EvidentialSource from Features/Evidentiality.lean:

• direct → sensory observation
• inference → reasoning from effects
• hearsay → reported evidence

Equations

• Minimalist.SpeechActs.EvidPSpecifier = Features.Evidentiality.EvidentialSource

theorem Minimalist.SpeechActs.sentience_domain_bridges_to_epistemicity : evalPSpecifier SAPMood.declarative = PRole.speaker ∧ evalPSpecifier SAPMood.interrogative = PRole.hearer

Bridge to Core/Epistemicity.lean: the Sentience Domain's two specifiers (SEAT OF KNOWLEDGE + EVIDENCE) correspond to EpistemicProfile's two main fields (authority + source).

S&T Sentience Domain	Core.Epistemicity
EvalP spec (Seat)	EpistemicProfile.authority
EvidP spec (Evidence)	EpistemicProfile.source

The structural hierarchy (EvalP > EvidP) corresponds to authority scoping over source: WHO evaluates is determined before HOW they know.