Linglib.Theories.Syntax.Minimalism.SpeechActs

Map configurational mood to framework-agnostic illocutionary mood. The mapping is injective: all four SAPMood constructors embed into IllocutionaryMood, but .exclamative has no SAPMood counterpart (exclamatives are not derived in S&T's 2×2 matrix). S&T's "subjunctive" maps to the illocutionary promissive — both encode [-finite, speaker-oriented] speech acts.

Equations

Instances For

source

def Minimalism.Phenomena.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

Instances For

source

def Minimalism.Phenomena.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

Instances For

source

theorem Minimalism.Phenomena.SpeechActs.seat_of_knowledge_agrees_with_mood_authority (m : SAPMood) :

(seatOfKnowledge m).toDiscourseRole = Core.Discourse.moodAuthority m.toIllocutionaryMood

seatOfKnowledge (Speas & Tenny, configurational) agrees with moodAuthority (SpeechActs.lean, framework-agnostic) via the toIllocutionaryMood bridge. Both encode the same generalization: declarative/imperative/subjunctive → speaker, interrogative → addressee.

source

def Minimalism.Phenomena.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

Instances For

source

def Minimalism.Phenomena.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

One or more equations did not get rendered due to their size.
Minimalism.Phenomena.SpeechActs.resolveRoleInMood ctx m x✝ = Minimalism.Phenomena.SpeechActs.resolveRole ctx x✝

Instances For

source

theorem Minimalism.Phenomena.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

source

theorem Minimalism.Phenomena.SpeechActs.declarative_speaker_knows :

seatOfKnowledge SAPMood.declarative = PRole.speaker

source

theorem Minimalism.Phenomena.SpeechActs.interrogative_hearer_knows :

seatOfKnowledge SAPMood.interrogative = PRole.hearer

source

theorem Minimalism.Phenomena.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

source

theorem Minimalism.Phenomena.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

source

theorem Minimalism.Phenomena.SpeechActs.deriveMood_finite :

deriveMood true false = SAPMood.declarative ∧ deriveMood true true = SAPMood.interrogative

source

theorem Minimalism.Phenomena.SpeechActs.sa_is_phase_head (so : SyntacticObject) (h : labelCat so = some Cat.SA) :

isSAPhaseHead so = true

source

theorem Minimalism.Phenomena.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

source

theorem Minimalism.Phenomena.SpeechActs.sa_phase_derivation_final :

isSAPhaseHead (mkLeaf Cat.SA [] 0) = true

source

theorem Minimalism.Phenomena.SpeechActs.sa_above_c_in_ep :

fValue Cat.SA > fValue Cat.C

source

theorem Minimalism.Phenomena.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

source

theorem Minimalism.Phenomena.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

source

def Minimalism.Phenomena.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

Instances For

source

def Minimalism.Phenomena.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

Minimalism.Phenomena.SpeechActs.pronounDiscourseRole p = p.person.bind Minimalism.Phenomena.SpeechActs.personToRole

Instances For

source

theorem Minimalism.Phenomena.SpeechActs.second_person_are_hearers :

pronounDiscourseRole Fragments.English.Pronouns.you = some PRole.hearer ∧ pronounDiscourseRole Fragments.English.Pronouns.you_pl = some PRole.hearer

source

theorem Minimalism.Phenomena.SpeechActs.third_person_no_role :

pronounDiscourseRole Fragments.English.Pronouns.he = none ∧ pronounDiscourseRole Fragments.English.Pronouns.she = none ∧ pronounDiscourseRole Fragments.English.Pronouns.it = none

source

theorem Minimalism.Phenomena.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.

source

inductive Minimalism.Phenomena.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

Instances For

source

instance Minimalism.Phenomena.SpeechActs.instDecidableEqSentienceProjection :

DecidableEq SentienceProjection

Equations

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

source

instance Minimalism.Phenomena.SpeechActs.instReprSentienceProjection :

Repr SentienceProjection

Equations

Minimalism.Phenomena.SpeechActs.instReprSentienceProjection = { reprPrec := Minimalism.Phenomena.SpeechActs.instReprSentienceProjection.repr }

source

def Minimalism.Phenomena.SpeechActs.instReprSentienceProjection.repr :

SentienceProjection → ℕ → Std.Format

Equations

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

Instances For

source

instance Minimalism.Phenomena.SpeechActs.instBEqSentienceProjection :

BEq SentienceProjection

Equations

Minimalism.Phenomena.SpeechActs.instBEqSentienceProjection = { beq := Minimalism.Phenomena.SpeechActs.instBEqSentienceProjection.beq }

source

def Minimalism.Phenomena.SpeechActs.instBEqSentienceProjection.beq :

SentienceProjection → SentienceProjection → Bool

Equations

Minimalism.Phenomena.SpeechActs.instBEqSentienceProjection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Minimalism.Phenomena.SpeechActs.SentienceProjection.rank :

SentienceProjection → ℕ

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

Equations

Instances For

source

theorem Minimalism.Phenomena.SpeechActs.evalp_above_evidp :

SentienceProjection.EvalP.rank > SentienceProjection.EvidP.rank

EvalP dominates EvidP in the Sentience Domain.

source

def Minimalism.Phenomena.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

Minimalism.Phenomena.SpeechActs.evalPSpecifier = Minimalism.Phenomena.SpeechActs.seatOfKnowledge

Instances For

source

@[reducible, inline]

abbrev Minimalism.Phenomena.SpeechActs.EvidPSpecifier :

Type

The specifier of EvidP hosts the evidence type.

Maps S&T's EVIDENCE argument to the framework-agnostic EvidentialSource from Core/Discourse/Evidence.lean:

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

Equations

Minimalism.Phenomena.SpeechActs.EvidPSpecifier = Core.Evidence.EvidentialSource

Instances For

source

theorem Minimalism.Phenomena.SpeechActs.sentience_domain_bridges_to_epistemicity :

evalPSpecifier SAPMood.declarative = PRole.speaker ∧ evalPSpecifier SAPMood.interrogative = PRole.hearer

Bridge to Core/Discourse/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.