Speech Acts and Intentional States

@cite{searle-1969} @cite{searle-1979} @cite{searle-1983} @cite{kaplan-1989} @cite{lakoff-1970} @cite{speas-tenny-2003} @cite{brandom-1994} @cite{gunlogson-2001} @cite{krifka-2015} @cite{bring-gunlogson-2000} @cite{romero-2024}

Unified infrastructure for speech acts, Intentional states, and their relationship — the parallel that @cite{searle-1983} argues is constitutive of both language and mind.

The Central Parallel

@cite{searle-1983}'s core thesis: Intentional states (beliefs, desires, intentions) and speech acts (assertions, orders, promises) share identical logical structure:

• Speech acts: F(p) — illocutionary force F + propositional content p
• Intentional states: S(r) — psychological mode S + representative content r

Four points of similarity:

1. The content/mode distinction applies to both
2. Direction of fit applies to both
3. Sincerity conditions link them: performing F(p) expresses S(r)
4. Conditions of satisfaction are determined by content + direction of fit

Organization

• § 1. Discourse Roles: speaker/addressee (framework-agnostic)
• § 2. Illocutionary Mood: the pragmatic act classification
• § 3. Direction of Fit: Searle's key classification principle
• § 4. Illocutionary Taxonomy: the five classes derived from direction of fit
• § 5. Psychological Mode: the S in S(r), linked to mood via sincerity conditions
• § 6. Causal Self-Referentiality: the "by way of" requirement on intentions
• § 7. Intentional States: S(r) as a type
• § 8. Discourse Commitments: the public trace of speech acts
• § 9. Source-Marked Commitments: Gunlogson's epistemic source tagging

inductive Core.Discourse.DiscourseRole : Type

The two fundamental discourse participants. .addressee matches KContext.addressee (not .listener as in Semantics.Dynamic).

• speaker : DiscourseRole
• addressee : DiscourseRole

instance Core.Discourse.instDecidableEqDiscourseRole : DecidableEq DiscourseRole

Equations

• Core.Discourse.instDecidableEqDiscourseRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.instReprDiscourseRole : Repr DiscourseRole

Equations

• Core.Discourse.instReprDiscourseRole = { reprPrec := Core.Discourse.instReprDiscourseRole.repr }

def Core.Discourse.instReprDiscourseRole.repr : DiscourseRole → ℕ → Std.Format

Equations

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

instance Core.Discourse.instBEqDiscourseRole : BEq DiscourseRole

Equations

• Core.Discourse.instBEqDiscourseRole = { beq := Core.Discourse.instBEqDiscourseRole.beq }

def Core.Discourse.instBEqDiscourseRole.beq : DiscourseRole → DiscourseRole → Bool

Equations

• Core.Discourse.instBEqDiscourseRole.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.instInhabitedDiscourseRole.default : DiscourseRole

Equations

• Core.Discourse.instInhabitedDiscourseRole.default = Core.Discourse.DiscourseRole.speaker

instance Core.Discourse.instInhabitedDiscourseRole : Inhabited DiscourseRole

Equations

• Core.Discourse.instInhabitedDiscourseRole = { default := Core.Discourse.instInhabitedDiscourseRole.default }

inductive Core.Discourse.IllocutionaryMood : Type

Illocutionary mood — the speech-act force of an utterance.

Distinct from GramMood (indicative/subjunctive morphology) and the Minimalist SAPMood (configurational). This classifies the pragmatic act performed — the F in F(p).

• declarative : IllocutionaryMood
• interrogative : IllocutionaryMood
• imperative : IllocutionaryMood
• promissive : IllocutionaryMood
• exclamative : IllocutionaryMood

instance Core.Discourse.instDecidableEqIllocutionaryMood : DecidableEq IllocutionaryMood

Equations

• Core.Discourse.instDecidableEqIllocutionaryMood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.instReprIllocutionaryMood : Repr IllocutionaryMood

Equations

• Core.Discourse.instReprIllocutionaryMood = { reprPrec := Core.Discourse.instReprIllocutionaryMood.repr }

def Core.Discourse.instReprIllocutionaryMood.repr : IllocutionaryMood → ℕ → Std.Format

Equations

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

def Core.Discourse.instBEqIllocutionaryMood.beq : IllocutionaryMood → IllocutionaryMood → Bool

Equations

• Core.Discourse.instBEqIllocutionaryMood.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.instBEqIllocutionaryMood : BEq IllocutionaryMood

Equations

• Core.Discourse.instBEqIllocutionaryMood = { beq := Core.Discourse.instBEqIllocutionaryMood.beq }

def Core.Discourse.instInhabitedIllocutionaryMood.default : IllocutionaryMood

Equations

• Core.Discourse.instInhabitedIllocutionaryMood.default = Core.Discourse.IllocutionaryMood.declarative

instance Core.Discourse.instInhabitedIllocutionaryMood : Inhabited IllocutionaryMood

Equations

• Core.Discourse.instInhabitedIllocutionaryMood = { default := Core.Discourse.instInhabitedIllocutionaryMood.default }

def Core.Discourse.moodAuthority : IllocutionaryMood → DiscourseRole

Which participant holds epistemic authority for a given illocutionary mood.

@cite{lakoff-1970}: in declaratives, imperatives, and promissives the speaker is the seat of knowledge; in interrogatives the addressee is.

Equations

• Core.Discourse.moodAuthority Core.Discourse.IllocutionaryMood.declarative = Core.Discourse.DiscourseRole.speaker
• Core.Discourse.moodAuthority Core.Discourse.IllocutionaryMood.interrogative = Core.Discourse.DiscourseRole.addressee
• Core.Discourse.moodAuthority Core.Discourse.IllocutionaryMood.imperative = Core.Discourse.DiscourseRole.speaker
• Core.Discourse.moodAuthority Core.Discourse.IllocutionaryMood.promissive = Core.Discourse.DiscourseRole.speaker
• Core.Discourse.moodAuthority Core.Discourse.IllocutionaryMood.exclamative = Core.Discourse.DiscourseRole.speaker

def Core.Discourse.resolveRole {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) : DiscourseRole → E

Resolve a discourse role to a concrete entity via a ContextTower, reading from the origin (speech-act context). .speaker -> tower.origin.agent, .addressee -> tower.origin.addressee.

Equations

• Core.Discourse.resolveRole tower Core.Discourse.DiscourseRole.speaker = tower.origin.agent
• Core.Discourse.resolveRole tower Core.Discourse.DiscourseRole.addressee = tower.origin.addressee

inductive Core.Discourse.DirectionOfFit : Type

Direction of fit: how responsibility for matching is distributed between the Intentional state (or speech act) and the world.

@cite{searle-1983}'s key classification principle. The metaphor: if a shopper's list doesn't match what's in the cart, the list is at fault (mind-to-world). If a builder's blueprint doesn't match the building, the building is at fault (world-to-mind).

• mindToWorld : DirectionOfFit

  Mind-to-world: the state must match independently existing reality. Beliefs, perceptions, assertions. If wrong, the state is at fault.

• worldToMind : DirectionOfFit

  World-to-mind: the world must be changed to match the state. Desires, intentions, orders, promises. If unfulfilled, the world is at fault.

• null : DirectionOfFit

  Null direction: the state presupposes the truth of its content but imposes no fit responsibility. Expressives (apologies, congratulations).

• double : DirectionOfFit

  Double direction: both mind-to-world and world-to-mind simultaneously. Declarations bring about a state of affairs by representing it as obtaining.

instance Core.Discourse.instDecidableEqDirectionOfFit : DecidableEq DirectionOfFit

Equations

• Core.Discourse.instDecidableEqDirectionOfFit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.instReprDirectionOfFit.repr : DirectionOfFit → ℕ → Std.Format

Equations

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

instance Core.Discourse.instReprDirectionOfFit : Repr DirectionOfFit

Equations

• Core.Discourse.instReprDirectionOfFit = { reprPrec := Core.Discourse.instReprDirectionOfFit.repr }

instance Core.Discourse.instBEqDirectionOfFit : BEq DirectionOfFit

Equations

• Core.Discourse.instBEqDirectionOfFit = { beq := Core.Discourse.instBEqDirectionOfFit.beq }

def Core.Discourse.instBEqDirectionOfFit.beq : DirectionOfFit → DirectionOfFit → Bool

Equations

• Core.Discourse.instBEqDirectionOfFit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.instInhabitedDirectionOfFit.default : DirectionOfFit

Equations

• Core.Discourse.instInhabitedDirectionOfFit.default = Core.Discourse.DirectionOfFit.mindToWorld

instance Core.Discourse.instInhabitedDirectionOfFit : Inhabited DirectionOfFit

Equations

• Core.Discourse.instInhabitedDirectionOfFit = { default := Core.Discourse.instInhabitedDirectionOfFit.default }

inductive Core.Discourse.SearleClass : Type

@cite{searle-1979}'s five basic categories of illocutionary acts, derived from the mind's representational capacities. These are exhaustive and mutually exclusive. Restated in @cite{searle-1983} Ch. 6: "the taxonomy is fundamentally a reflection of the various ways in which representations can have directions of fit."

• assertive : SearleClass

  We tell people how things are (assertions, statements, descriptions).

• directive : SearleClass

  We try to get people to do things (orders, commands, requests).

• commissive : SearleClass

  We commit ourselves to doing things (promises, vows, pledges).

• declaration : SearleClass

  We bring about changes by representing them as obtaining (verdicts, appointments).

• expressive : SearleClass

  We express feelings about presupposed states of affairs (apologies, congratulations).

instance Core.Discourse.instDecidableEqSearleClass : DecidableEq SearleClass

Equations

• Core.Discourse.instDecidableEqSearleClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.instReprSearleClass : Repr SearleClass

Equations

• Core.Discourse.instReprSearleClass = { reprPrec := Core.Discourse.instReprSearleClass.repr }

def Core.Discourse.instReprSearleClass.repr : SearleClass → ℕ → Std.Format

Equations

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

def Core.Discourse.instBEqSearleClass.beq : SearleClass → SearleClass → Bool

Equations

• Core.Discourse.instBEqSearleClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.instBEqSearleClass : BEq SearleClass

Equations

• Core.Discourse.instBEqSearleClass = { beq := Core.Discourse.instBEqSearleClass.beq }

def Core.Discourse.instInhabitedSearleClass.default : SearleClass

Equations

• Core.Discourse.instInhabitedSearleClass.default = Core.Discourse.SearleClass.assertive

instance Core.Discourse.instInhabitedSearleClass : Inhabited SearleClass

Equations

• Core.Discourse.instInhabitedSearleClass = { default := Core.Discourse.instInhabitedSearleClass.default }

def Core.Discourse.SearleClass.directionOfFit : SearleClass → DirectionOfFit

Direction of fit for each illocutionary class. The five classes are derived from the possible directions of fit.

Equations

• Core.Discourse.SearleClass.assertive.directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld
• Core.Discourse.SearleClass.directive.directionOfFit = Core.Discourse.DirectionOfFit.worldToMind
• Core.Discourse.SearleClass.commissive.directionOfFit = Core.Discourse.DirectionOfFit.worldToMind
• Core.Discourse.SearleClass.declaration.directionOfFit = Core.Discourse.DirectionOfFit.double
• Core.Discourse.SearleClass.expressive.directionOfFit = Core.Discourse.DirectionOfFit.null

def Core.Discourse.IllocutionaryMood.searleClass : IllocutionaryMood → SearleClass

Map IllocutionaryMood to Searle class. Not injective: both directives (imperative) and commissives (promissive) share world-to-mind fit.

Equations

• Core.Discourse.IllocutionaryMood.declarative.searleClass = Core.Discourse.SearleClass.assertive
• Core.Discourse.IllocutionaryMood.interrogative.searleClass = Core.Discourse.SearleClass.directive
• Core.Discourse.IllocutionaryMood.imperative.searleClass = Core.Discourse.SearleClass.directive
• Core.Discourse.IllocutionaryMood.promissive.searleClass = Core.Discourse.SearleClass.commissive
• Core.Discourse.IllocutionaryMood.exclamative.searleClass = Core.Discourse.SearleClass.expressive

def Core.Discourse.IllocutionaryMood.directionOfFit (m : IllocutionaryMood) : DirectionOfFit

Direction of fit for an illocutionary mood, derived via Searle class.

Equations

• m.directionOfFit = m.searleClass.directionOfFit

inductive Core.Discourse.PsychMode : Type

Named psychological modes: the "S" in @cite{searle-1983}'s S(r) notation.

Parallel to illocutionary force "F" in F(p) for speech acts. Each mode has a direction of fit and may or may not be causally self-referential.

@cite{searle-1983}, Ch. 1: belief, desire, and intention are the prototypical modes. Perception (Ch. 2) is a causally self-referential mode that plays a key role in the theory's account of how the mind relates to the world.

• belief : PsychMode

  Bel(p): satisfied iff p obtains. Not self-referential — HOW p came to obtain is irrelevant (Ch. 1, p. 8).

• desire : PsychMode

  Des(p): satisfied iff p comes about. Not self-referential — HOW p is brought about is irrelevant (Ch. 1, p. 8).

• intention : PsychMode

  Int(p): satisfied iff p is brought about BY WAY OF carrying out this intention. Self-referential: state→world (Ch. 3, pp. 85–86).

• perception : PsychMode

  Per(p): satisfied iff the object/state of affairs CAUSES this experience. Self-referential: world→state (Ch. 2; Ch. 3, p. 91).

• expressive : PsychMode

  Expressive states (pleasure, sorrow, etc.): presuppose the truth of their content but impose no fit responsibility (Ch. 1, pp. 7–8).

instance Core.Discourse.instDecidableEqPsychMode : DecidableEq PsychMode

Equations

• Core.Discourse.instDecidableEqPsychMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.instReprPsychMode : Repr PsychMode

Equations

• Core.Discourse.instReprPsychMode = { reprPrec := Core.Discourse.instReprPsychMode.repr }

def Core.Discourse.instReprPsychMode.repr : PsychMode → ℕ → Std.Format

Equations

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

instance Core.Discourse.instBEqPsychMode : BEq PsychMode

Equations

• Core.Discourse.instBEqPsychMode = { beq := Core.Discourse.instBEqPsychMode.beq }

def Core.Discourse.instBEqPsychMode.beq : PsychMode → PsychMode → Bool

Equations

• Core.Discourse.instBEqPsychMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.instInhabitedPsychMode.default : PsychMode

Equations

• Core.Discourse.instInhabitedPsychMode.default = Core.Discourse.PsychMode.belief

instance Core.Discourse.instInhabitedPsychMode : Inhabited PsychMode

Equations

• Core.Discourse.instInhabitedPsychMode = { default := Core.Discourse.instInhabitedPsychMode.default }

def Core.Discourse.PsychMode.directionOfFit : PsychMode → DirectionOfFit

Direction of fit for each psychological mode.

Beliefs and perceptions: mind-to-world (the state must match reality). Desires and intentions: world-to-mind (reality must match the state). Expressives: null (presuppose truth, no fit responsibility).

Equations

• Core.Discourse.PsychMode.belief.directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld
• Core.Discourse.PsychMode.desire.directionOfFit = Core.Discourse.DirectionOfFit.worldToMind
• Core.Discourse.PsychMode.intention.directionOfFit = Core.Discourse.DirectionOfFit.worldToMind
• Core.Discourse.PsychMode.perception.directionOfFit = Core.Discourse.DirectionOfFit.mindToWorld
• Core.Discourse.PsychMode.expressive.directionOfFit = Core.Discourse.DirectionOfFit.null

def Core.Discourse.sincerityCondition : IllocutionaryMood → PsychMode

The sincerity condition: performing a speech act with mood F necessarily expresses the corresponding Intentional state S, and the conditions of satisfaction of the speech act are identical to those of the expressed state.

@cite{searle-1983}, Ch. 1 §3: you can't say "It's snowing but I don't believe it's snowing" — the assertion eo ipso expresses the belief. Ch. 6, p. 174: "the conditions of satisfaction of the sincerity condition" are "identical with the conditions of satisfaction" of the speech act.

Equations

• Core.Discourse.sincerityCondition Core.Discourse.IllocutionaryMood.declarative = Core.Discourse.PsychMode.belief
• Core.Discourse.sincerityCondition Core.Discourse.IllocutionaryMood.interrogative = Core.Discourse.PsychMode.desire
• Core.Discourse.sincerityCondition Core.Discourse.IllocutionaryMood.imperative = Core.Discourse.PsychMode.desire
• Core.Discourse.sincerityCondition Core.Discourse.IllocutionaryMood.promissive = Core.Discourse.PsychMode.intention
• Core.Discourse.sincerityCondition Core.Discourse.IllocutionaryMood.exclamative = Core.Discourse.PsychMode.expressive

inductive Core.Discourse.CausalSelfRef : Type

Causal self-referentiality: whether the Intentional state must itself figure in the causal chain producing its conditions of satisfaction.

Beliefs: no self-referentiality — satisfied iff the state of affairs obtains. Intentions: self-referential — "my arm goes up as a result of this intention." Perceptions: self-referential in reverse — the object must cause the experience.

• none : CausalSelfRef

  Not self-referential: satisfaction depends only on the state of affairs obtaining. Example: beliefs.

• stateToWorld : CausalSelfRef

  State-to-world: the state must cause its conditions of satisfaction. Example: intentions — "by way of carrying out this intention."

• worldToState : CausalSelfRef

  World-to-state: the conditions of satisfaction must cause the state. Example: perceptions — the object causes the visual experience.

instance Core.Discourse.instDecidableEqCausalSelfRef : DecidableEq CausalSelfRef

Equations

• Core.Discourse.instDecidableEqCausalSelfRef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.instReprCausalSelfRef : Repr CausalSelfRef

Equations

• Core.Discourse.instReprCausalSelfRef = { reprPrec := Core.Discourse.instReprCausalSelfRef.repr }

def Core.Discourse.instReprCausalSelfRef.repr : CausalSelfRef → ℕ → Std.Format

Equations

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

instance Core.Discourse.instBEqCausalSelfRef : BEq CausalSelfRef

Equations

• Core.Discourse.instBEqCausalSelfRef = { beq := Core.Discourse.instBEqCausalSelfRef.beq }

def Core.Discourse.instBEqCausalSelfRef.beq : CausalSelfRef → CausalSelfRef → Bool

Equations

• Core.Discourse.instBEqCausalSelfRef.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.PsychMode.causalSelfRef : PsychMode → CausalSelfRef

Causal self-referentiality for each psychological mode.

@cite{searle-1983}, Ch. 3 (table on p. 91): self-referentiality is NOT determined by direction of fit alone. Both beliefs and perceptions have mind-to-world fit, but only perceptions are self-referential. Both desires and intentions have world-to-mind fit, but only intentions are.

• Perception: the object must cause the experience (world→state)
• Intention: the intention must cause its conditions of satisfaction (state→world)
• Belief/Desire: satisfaction depends only on whether the state of affairs obtains

Equations

• Core.Discourse.PsychMode.belief.causalSelfRef = Core.Discourse.CausalSelfRef.none
• Core.Discourse.PsychMode.desire.causalSelfRef = Core.Discourse.CausalSelfRef.none
• Core.Discourse.PsychMode.intention.causalSelfRef = Core.Discourse.CausalSelfRef.stateToWorld
• Core.Discourse.PsychMode.perception.causalSelfRef = Core.Discourse.CausalSelfRef.worldToState
• Core.Discourse.PsychMode.expressive.causalSelfRef = Core.Discourse.CausalSelfRef.none

structure Core.Discourse.IntentionalState (W : Type u_1) : Type u_1

An Intentional state: psychological mode + representative content.

@cite{searle-1983}, Ch. 1: "every Intentional state consists of a representative content in a psychological mode." Symbolized S(r).

Conditions of satisfaction are determined by the content under the direction of fit given by the mode — they are internal to the state.

• mode : PsychMode

  The psychological mode (belief, desire, intention, ...)

• content : BProp W

  The representative content

def Core.Discourse.IntentionalState.conditionsOfSatisfaction {W : Type u_1} (s : IntentionalState W) : BProp W

Conditions of satisfaction: what must obtain for the state to be satisfied. These are identical to the content — not a separate component.

Equations

• s.conditionsOfSatisfaction = s.content

structure Core.Discourse.Commitment.CommitmentSlate (W : Type u_1) : Type u_1

An agent's public discourse commitments: a list of propositions the agent has publicly committed to.

Following @cite{krifka-2015}: the commitment slate tracks what an agent is publicly committed to, which may diverge from what they privately believe (as in lying, hedging, or performing).

In @cite{searle-1983}'s terms: commitment is the public direction-of-fit obligation created by performing a speech act. Asserting p creates a mind-to-world commitment (the speaker is responsible if p is false); promising p creates a world-to-mind commitment (the speaker is responsible if p is unfulfilled).

• commitments : List (BProp W)

  The propositions the agent is publicly committed to

def Core.Discourse.Commitment.CommitmentSlate.empty {W : Type u_1} : CommitmentSlate W

The empty commitment slate: no public commitments.

Equations

• Core.Discourse.Commitment.CommitmentSlate.empty = { commitments := [] }

def Core.Discourse.Commitment.CommitmentSlate.add {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) : CommitmentSlate W

Add a commitment to the slate.

Equations

• s.add p = { commitments := p :: s.commitments }

def Core.Discourse.Commitment.CommitmentSlate.retract {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) [BEq (BProp W)] : CommitmentSlate W

Retract a commitment (remove first occurrence).

Not all theories support retraction. Stalnaker's CG model has no retraction mechanism; Krifka and Brandom do.

Equations

• s.retract p = { commitments := s.commitments.erase p }

def Core.Discourse.Commitment.CommitmentSlate.toContextSet {W : Type u_1} (s : CommitmentSlate W) : BProp W

Convert commitments to a context set: the worlds compatible with all committed propositions.

Equations

• s.toContextSet w = s.commitments.all fun (p : BProp W) => p w

def Core.Discourse.Commitment.CommitmentSlate.entails {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (worlds : List W) : Bool

Check if the slate entails a proposition (holds at all compatible worlds).

Equations

• s.entails p worlds = worlds.all fun (w : W) => (!s.commitments.all fun (q : BProp W) => q w) || p w

theorem Core.Discourse.Commitment.CommitmentSlate.empty_trivial {W : Type u_1} (w : W) : empty.toContextSet w = true

Empty slate is trivial: all worlds are compatible.

theorem Core.Discourse.Commitment.CommitmentSlate.add_restricts {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (w : W) : (s.add p).toContextSet w = true → s.toContextSet w = true

Adding a commitment restricts the context set.

theorem Core.Discourse.Commitment.CommitmentSlate.add_entails {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (w : W) : (s.add p).toContextSet w = true → p w = true

Adding a commitment entails the added proposition.

inductive Core.Discourse.Commitment.CommitmentSource : Type

The source of a discourse commitment.

@cite{gunlogson-2001}: commitments are marked by their epistemic source. The source determines challengeability: self-generated commitments can be challenged by the addressee; other-generated commitments can be challenged by the speaker.

• selfGenerated : CommitmentSource

  Commitment generated from agent's own evidence/beliefs

• otherGenerated : CommitmentSource

  Commitment attributed to another participant

instance Core.Discourse.Commitment.instDecidableEqCommitmentSource : DecidableEq CommitmentSource

Equations

• Core.Discourse.Commitment.instDecidableEqCommitmentSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.Commitment.instReprCommitmentSource.repr : CommitmentSource → ℕ → Std.Format

Equations

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

instance Core.Discourse.Commitment.instReprCommitmentSource : Repr CommitmentSource

Equations

• Core.Discourse.Commitment.instReprCommitmentSource = { reprPrec := Core.Discourse.Commitment.instReprCommitmentSource.repr }

def Core.Discourse.Commitment.instBEqCommitmentSource.beq : CommitmentSource → CommitmentSource → Bool

Equations

• Core.Discourse.Commitment.instBEqCommitmentSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.Commitment.instBEqCommitmentSource : BEq CommitmentSource

Equations

• Core.Discourse.Commitment.instBEqCommitmentSource = { beq := Core.Discourse.Commitment.instBEqCommitmentSource.beq }

def Core.Discourse.Commitment.instInhabitedCommitmentSource.default : CommitmentSource

Equations

• Core.Discourse.Commitment.instInhabitedCommitmentSource.default = Core.Discourse.Commitment.CommitmentSource.selfGenerated

instance Core.Discourse.Commitment.instInhabitedCommitmentSource : Inhabited CommitmentSource

Equations

• Core.Discourse.Commitment.instInhabitedCommitmentSource = { default := Core.Discourse.Commitment.instInhabitedCommitmentSource.default }

structure Core.Discourse.Commitment.TaggedCommitment (W : Type u_1) : Type u_1

A commitment tagged with its source.

• content : BProp W

  The propositional content

• source : CommitmentSource

  How the commitment was generated

structure Core.Discourse.Commitment.TaggedSlate (W : Type u_1) : Type u_1

A source-tagged commitment slate.

• commitments : List (TaggedCommitment W)

  The tagged commitments

def Core.Discourse.Commitment.TaggedSlate.empty {W : Type u_1} : TaggedSlate W

The empty tagged slate.

Equations

• Core.Discourse.Commitment.TaggedSlate.empty = { commitments := [] }

def Core.Discourse.Commitment.TaggedSlate.add {W : Type u_1} (s : TaggedSlate W) (p : BProp W) (src : CommitmentSource) : TaggedSlate W

Add a tagged commitment.

Equations

• s.add p src = { commitments := { content := p, source := src } :: s.commitments }

def Core.Discourse.Commitment.TaggedSlate.selfGenerated {W : Type u_1} (s : TaggedSlate W) : List (BProp W)

Get all self-generated commitments.

Equations

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

def Core.Discourse.Commitment.TaggedSlate.otherGenerated {W : Type u_1} (s : TaggedSlate W) : List (BProp W)

Get all other-generated commitments.

Equations

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

def Core.Discourse.Commitment.TaggedSlate.toSlate {W : Type u_1} (s : TaggedSlate W) : CommitmentSlate W

Convert to a plain (untagged) commitment slate.

Equations

• s.toSlate = { commitments := List.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.content) s.commitments }

def Core.Discourse.Commitment.TaggedSlate.toContextSet {W : Type u_1} (s : TaggedSlate W) : BProp W

Convert to context set (ignoring source tags).

Equations

• s.toContextSet = s.toSlate.toContextSet

inductive Core.Discourse.Commitment.ContextualEvidence : Type

Contextual evidence bias.

Expectation about p induced by evidence available in the current discourse situation (@cite{bring-gunlogson-2000}). Used as:

• A felicity condition on rising declaratives
• A bias dimension for polar questions

• forP : ContextualEvidence

  Current context provides evidence for p.

• neutral : ContextualEvidence

  No contextual evidence either way.

• againstP : ContextualEvidence

  Current context provides evidence against p.

instance Core.Discourse.Commitment.instDecidableEqContextualEvidence : DecidableEq ContextualEvidence

Equations

• Core.Discourse.Commitment.instDecidableEqContextualEvidence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.Commitment.instBEqContextualEvidence.beq : ContextualEvidence → ContextualEvidence → Bool

Equations

• Core.Discourse.Commitment.instBEqContextualEvidence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.Commitment.instBEqContextualEvidence : BEq ContextualEvidence

Equations

• Core.Discourse.Commitment.instBEqContextualEvidence = { beq := Core.Discourse.Commitment.instBEqContextualEvidence.beq }

def Core.Discourse.Commitment.instReprContextualEvidence.repr : ContextualEvidence → ℕ → Std.Format

Equations

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

instance Core.Discourse.Commitment.instReprContextualEvidence : Repr ContextualEvidence

Equations

• Core.Discourse.Commitment.instReprContextualEvidence = { reprPrec := Core.Discourse.Commitment.instReprContextualEvidence.repr }

inductive Core.Discourse.PreparatoryCondition : Type

Preparatory conditions for directive speech acts.

@cite{searle-1969}: for a request to be felicitous, the hearer must satisfy certain preconditions — ability to comply and willingness to comply. @cite{francik-clark-1985} show that speakers design indirect requests to target the specific preparatory condition most at risk, refining "ability" into a subsumption hierarchy:

ability
├── knowledge
│   ├── memory       ("Do you remember?")
│   └── perception   ("Did you see/hear/notice?")
└── permission       ("Are you allowed?")
willingness           ("Would you mind?")

More specific conditions correspond to more specific (less direct) request forms.

• ability : PreparatoryCondition

  Hearer is able to perform the requested act (general).

• knowledge : PreparatoryCondition

  Hearer knows the relevant information. Subtype of ability.

• memory : PreparatoryCondition

  Hearer remembers the information. Subtype of knowledge.

• perception : PreparatoryCondition

  Hearer has perceived the relevant source. Subtype of knowledge.

• permission : PreparatoryCondition

  Hearer is permitted to perform the act. Subtype of ability.

• willingness : PreparatoryCondition

  Hearer is willing to perform the act. Independent of ability.

instance Core.Discourse.instDecidableEqPreparatoryCondition : DecidableEq PreparatoryCondition

Equations

• Core.Discourse.instDecidableEqPreparatoryCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.instBEqPreparatoryCondition.beq : PreparatoryCondition → PreparatoryCondition → Bool

Equations

• Core.Discourse.instBEqPreparatoryCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.instBEqPreparatoryCondition : BEq PreparatoryCondition

Equations

• Core.Discourse.instBEqPreparatoryCondition = { beq := Core.Discourse.instBEqPreparatoryCondition.beq }

instance Core.Discourse.instReprPreparatoryCondition : Repr PreparatoryCondition

Equations

• Core.Discourse.instReprPreparatoryCondition = { reprPrec := Core.Discourse.instReprPreparatoryCondition.repr }

def Core.Discourse.instReprPreparatoryCondition.repr : PreparatoryCondition → ℕ → Std.Format

Equations

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

def Core.Discourse.PreparatoryCondition.subsumes : PreparatoryCondition → PreparatoryCondition → Bool

Subsumption: c₁.subsumes c₂ iff satisfying c₂ entails satisfying c₁.

Memory and perception are subtypes of knowledge; knowledge and permission are subtypes of ability. Willingness is independent.

Equations

• Core.Discourse.PreparatoryCondition.ability.subsumes Core.Discourse.PreparatoryCondition.ability = true
• Core.Discourse.PreparatoryCondition.knowledge.subsumes Core.Discourse.PreparatoryCondition.knowledge = true
• Core.Discourse.PreparatoryCondition.memory.subsumes Core.Discourse.PreparatoryCondition.memory = true
• Core.Discourse.PreparatoryCondition.perception.subsumes Core.Discourse.PreparatoryCondition.perception = true
• Core.Discourse.PreparatoryCondition.permission.subsumes Core.Discourse.PreparatoryCondition.permission = true
• Core.Discourse.PreparatoryCondition.willingness.subsumes Core.Discourse.PreparatoryCondition.willingness = true
• Core.Discourse.PreparatoryCondition.ability.subsumes Core.Discourse.PreparatoryCondition.knowledge = true
• Core.Discourse.PreparatoryCondition.ability.subsumes Core.Discourse.PreparatoryCondition.memory = true
• Core.Discourse.PreparatoryCondition.ability.subsumes Core.Discourse.PreparatoryCondition.perception = true
• Core.Discourse.PreparatoryCondition.ability.subsumes Core.Discourse.PreparatoryCondition.permission = true
• Core.Discourse.PreparatoryCondition.knowledge.subsumes Core.Discourse.PreparatoryCondition.memory = true
• Core.Discourse.PreparatoryCondition.knowledge.subsumes Core.Discourse.PreparatoryCondition.perception = true
• x✝¹.subsumes x✝ = false

theorem Core.Discourse.PreparatoryCondition.subsumes_refl (c : PreparatoryCondition) : c.subsumes c = true

theorem Core.Discourse.PreparatoryCondition.specificity_chain : ability.subsumes knowledge = true ∧ knowledge.subsumes memory = true ∧ knowledge.subsumes perception = true ∧ ability.subsumes permission = true

The specificity chain: memory/perception → knowledge → ability.

theorem Core.Discourse.PreparatoryCondition.willingness_independent : ability.subsumes willingness = false ∧ willingness.subsumes ability = false

Willingness is independent of ability: neither subsumes the other.

theorem Core.Discourse.directive_has_preparatory_conditions : SearleClass.directive.directionOfFit = DirectionOfFit.worldToMind

Directives are the speech act class that has preparatory conditions on the hearer's ability and willingness.

theorem Core.Discourse.epistemic_authority_declarative : moodAuthority IllocutionaryMood.declarative = DiscourseRole.speaker

theorem Core.Discourse.epistemic_authority_interrogative : moodAuthority IllocutionaryMood.interrogative = DiscourseRole.addressee

theorem Core.Discourse.resolve_speaker_is_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) : resolveRole tower DiscourseRole.speaker = tower.origin.agent

theorem Core.Discourse.resolve_addressee_is_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) : resolveRole tower DiscourseRole.addressee = tower.origin.addressee

theorem Core.Discourse.resolveRole_shift_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tower : Context.ContextTower (Context.KContext W E P T)) (σ : Context.ContextShift (Context.KContext W E P T)) (r : DiscourseRole) : resolveRole (tower.push σ) r = resolveRole tower r

Discourse role resolution is invariant under tower push: discourse roles reflect speech-act participants (from origin), not embedded ones.

theorem Core.Discourse.assertive_mind_to_world : SearleClass.assertive.directionOfFit = DirectionOfFit.mindToWorld

theorem Core.Discourse.directive_world_to_mind : SearleClass.directive.directionOfFit = DirectionOfFit.worldToMind

theorem Core.Discourse.commissive_world_to_mind : SearleClass.commissive.directionOfFit = DirectionOfFit.worldToMind

theorem Core.Discourse.declaration_double : SearleClass.declaration.directionOfFit = DirectionOfFit.double

theorem Core.Discourse.expressive_null : SearleClass.expressive.directionOfFit = DirectionOfFit.null

theorem Core.Discourse.sincerity_assertion : (sincerityCondition IllocutionaryMood.declarative).directionOfFit = DirectionOfFit.mindToWorld

theorem Core.Discourse.sincerity_order : (sincerityCondition IllocutionaryMood.imperative).directionOfFit = DirectionOfFit.worldToMind

theorem Core.Discourse.sincerity_promise : (sincerityCondition IllocutionaryMood.promissive).directionOfFit = DirectionOfFit.worldToMind

theorem Core.Discourse.sincerity_exclamation : (sincerityCondition IllocutionaryMood.exclamative).directionOfFit = DirectionOfFit.null

theorem Core.Discourse.sincerity_direction_matches_class (m : IllocutionaryMood) : (sincerityCondition m).directionOfFit = m.directionOfFit

@cite{searle-1983}'s central parallel: the direction of fit of the sincerity condition matches the direction of fit of the speech act class.

Asserting p expresses a mind-to-world state (belief); ordering p expresses a world-to-mind state (desire); promising p expresses a world-to-mind state (intention). This is constitutive (@cite{searle-1983}, Ch. 1 §3).

theorem Core.Discourse.beliefs_not_self_referential : PsychMode.belief.causalSelfRef = CausalSelfRef.none

theorem Core.Discourse.desires_not_self_referential : PsychMode.desire.causalSelfRef = CausalSelfRef.none

theorem Core.Discourse.intentions_self_referential : PsychMode.intention.causalSelfRef = CausalSelfRef.stateToWorld

theorem Core.Discourse.perceptions_self_referential : PsychMode.perception.causalSelfRef = CausalSelfRef.worldToState

theorem Core.Discourse.self_ref_independent_of_direction : PsychMode.belief.directionOfFit = PsychMode.perception.directionOfFit ∧ PsychMode.belief.causalSelfRef ≠ PsychMode.perception.causalSelfRef

@cite{searle-1983}'s key insight (Ch. 3, p. 91): causal self-referentiality is NOT determined by direction of fit alone. Beliefs and perceptions share mind-to-world fit, but only perceptions are self-referential.

theorem Core.Discourse.conditions_are_content {W : Type u_1} (s : IntentionalState W) : s.conditionsOfSatisfaction = s.content

Conditions of satisfaction are internal to the content — not a separate component. This rfl proof IS the formalization of @cite{searle-1983}'s claim (Ch. 1, p. 12): "the Intentional content determines the conditions of satisfaction."

instance Core.Discourse.instHasContextSetCommitmentSlate {W : Type u_1} : CommonGround.HasContextSet (Commitment.CommitmentSlate W) W

A commitment slate projects to a context set: the worlds compatible with all committed propositions.

Equations

• Core.Discourse.instHasContextSetCommitmentSlate = { toContextSet := fun (s : Core.Discourse.Commitment.CommitmentSlate W) (w : W) => s.toContextSet w = true }