Searlean Speech Acts: F(p) and S(r)

[Sea69]'s speech-act theory as elaborated in [Sea79] and [Sea83]: an illocutionary act F(p) performed sincerely expresses the corresponding Intentional state S(r) — the sincerity-condition law — and conditions of satisfaction transfer between them. Also the preparatory conditions for directives, in the inventory of [FC85].

Main declarations

• DirectionOfFit — how responsibility for matching state and world is distributed.
• SearleClass — [Sea79]'s five illocutionary classes.
• PsychMode — the psychological modes (the S in S(r)).
• IllocutionaryMood.searleClass, IllocutionaryMood.sincerityCondition — the per-mood illocutionary class and the F → S bridge.
• CausalSelfRef, PsychMode.causalSelfRef — whether a mode must figure in the causal chain producing its own conditions of satisfaction.
• PreparatoryCondition — felicity preconditions for directives, ordered by the subsumes specificity relation.
• IllocutionaryMood.sincerityCondition_directionOfFit — the sincerity condition's direction of fit matches the speech act's.
• PsychMode.causalSelfRef_not_determined_by_directionOfFit — causal self-referentiality is not a function of direction of fit.

Implementation notes

PsychMode.expressive collapses [Sea69]'s heterogeneous expressive sincerity states (gratitude, pleasure, regret, ...) into a single mode; its null direction of fit is [Sea79]'s claim about the expressive class. Commitment-based accounts (CommitmentForce.doxastic "act-as-if-believe", per [CL12] and [Lau13]; Brandom's commitment-without-entitlement) deliberately weaken IllocutionaryMood.sincerityCondition .declarative = .belief from sincere belief to public commitment.

References

• [Sea69], [Sea79], [Sea83], [FC85]

Direction of fit

inductive DirectionOfFit : Type

Direction of fit: how responsibility for matching the state and the world is distributed ([Sea83]).

• mindToWorld : DirectionOfFit

  State must match reality (beliefs, assertions).

• worldToMind : DirectionOfFit

  World must change to match the state (desires, orders).

• null : DirectionOfFit

  Presupposed truth, no fit responsibility (expressives).

• double : DirectionOfFit

  Both directions simultaneously (declarations).

@[implicit_reducible]

instance instDecidableEqDirectionOfFit : DecidableEq DirectionOfFit

Equations

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

@[implicit_reducible]

instance instReprDirectionOfFit : Repr DirectionOfFit

Equations

• instReprDirectionOfFit = { reprPrec := instReprDirectionOfFit.repr }

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

Equations

• instReprDirectionOfFit.repr DirectionOfFit.mindToWorld prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DirectionOfFit.mindToWorld")).group prec✝
• instReprDirectionOfFit.repr DirectionOfFit.worldToMind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DirectionOfFit.worldToMind")).group prec✝
• instReprDirectionOfFit.repr DirectionOfFit.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DirectionOfFit.null")).group prec✝
• instReprDirectionOfFit.repr DirectionOfFit.double prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DirectionOfFit.double")).group prec✝

@[implicit_reducible]

instance instInhabitedDirectionOfFit : Inhabited DirectionOfFit

Equations

• instInhabitedDirectionOfFit = { default := instInhabitedDirectionOfFit.default }

Illocutionary taxonomy — F(p)

inductive SearleClass : Type

[Sea79]'s five basic categories of illocutionary acts; exhaustive and mutually exclusive.

• assertive : SearleClass

  Assertions, statements, descriptions.

• directive : SearleClass

  Orders, commands, requests.

• commissive : SearleClass

  Promises, vows, pledges.

• declaration : SearleClass

  Verdicts, appointments (bring about by declaring).

• expressive : SearleClass

  Apologies, congratulations (express feelings about presupposed states).

@[implicit_reducible]

instance instDecidableEqSearleClass : DecidableEq SearleClass

Equations

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

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

Equations

• instReprSearleClass.repr SearleClass.assertive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SearleClass.assertive")).group prec✝
• instReprSearleClass.repr SearleClass.directive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SearleClass.directive")).group prec✝
• instReprSearleClass.repr SearleClass.commissive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SearleClass.commissive")).group prec✝
• instReprSearleClass.repr SearleClass.declaration prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SearleClass.declaration")).group prec✝
• instReprSearleClass.repr SearleClass.expressive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SearleClass.expressive")).group prec✝

@[implicit_reducible]

instance instReprSearleClass : Repr SearleClass

Equations

• instReprSearleClass = { reprPrec := instReprSearleClass.repr }

@[implicit_reducible]

instance instInhabitedSearleClass : Inhabited SearleClass

Equations

• instInhabitedSearleClass = { default := instInhabitedSearleClass.default }

def SearleClass.directionOfFit : SearleClass → DirectionOfFit

Direction of fit for each illocutionary class.

Equations

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

Psychological mode — S(r)

inductive PsychMode : Type

Psychological modes: the "S" in [Sea83]'s S(r).

• belief : PsychMode

  Bel(p): satisfied iff p obtains.

• desire : PsychMode

  Des(p): satisfied iff p comes about.

• intention : PsychMode

  Int(p): satisfied iff p is brought about by carrying out the intention.

• perception : PsychMode

  Per(p): satisfied iff the object causes this experience.

• expressive : PsychMode

  Stand-in for [Sea69]'s heterogeneous expressive states (gratitude, pleasure, regret, ...); truth presupposed, no fit responsibility ([Sea79]).

@[implicit_reducible]

instance instDecidableEqPsychMode : DecidableEq PsychMode

Equations

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

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

Equations

• instReprPsychMode.repr PsychMode.belief prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PsychMode.belief")).group prec✝
• instReprPsychMode.repr PsychMode.desire prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PsychMode.desire")).group prec✝
• instReprPsychMode.repr PsychMode.intention prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PsychMode.intention")).group prec✝
• instReprPsychMode.repr PsychMode.perception prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PsychMode.perception")).group prec✝
• instReprPsychMode.repr PsychMode.expressive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PsychMode.expressive")).group prec✝

@[implicit_reducible]

instance instReprPsychMode : Repr PsychMode

Equations

• instReprPsychMode = { reprPrec := instReprPsychMode.repr }

@[implicit_reducible]

instance instInhabitedPsychMode : Inhabited PsychMode

Equations

• instInhabitedPsychMode = { default := instInhabitedPsychMode.default }

def PsychMode.directionOfFit : PsychMode → DirectionOfFit

Direction of fit for each psychological mode.

Equations

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

Mood bridges — class and sincerity condition

def Semantics.Mood.IllocutionaryMood.searleClass : IllocutionaryMood → SearleClass

The [Sea79] illocutionary class of each mood.

Equations

• Semantics.Mood.IllocutionaryMood.declarative.searleClass = SearleClass.assertive
• Semantics.Mood.IllocutionaryMood.interrogative.searleClass = SearleClass.directive
• Semantics.Mood.IllocutionaryMood.imperative.searleClass = SearleClass.directive
• Semantics.Mood.IllocutionaryMood.promissive.searleClass = SearleClass.commissive
• Semantics.Mood.IllocutionaryMood.exclamative.searleClass = SearleClass.expressive

def Semantics.Mood.IllocutionaryMood.directionOfFit (m : IllocutionaryMood) : DirectionOfFit

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

Equations

• m.directionOfFit = m.searleClass.directionOfFit

def Semantics.Mood.IllocutionaryMood.sincerityCondition : IllocutionaryMood → PsychMode

Sincerity condition ([Sea69]): performing a speech act with mood F expresses the corresponding Intentional state S.

Equations

• Semantics.Mood.IllocutionaryMood.declarative.sincerityCondition = PsychMode.belief
• Semantics.Mood.IllocutionaryMood.interrogative.sincerityCondition = PsychMode.desire
• Semantics.Mood.IllocutionaryMood.imperative.sincerityCondition = PsychMode.desire
• Semantics.Mood.IllocutionaryMood.promissive.sincerityCondition = PsychMode.intention
• Semantics.Mood.IllocutionaryMood.exclamative.sincerityCondition = PsychMode.expressive

theorem Semantics.Mood.IllocutionaryMood.sincerityCondition_directionOfFit (m : IllocutionaryMood) : m.sincerityCondition.directionOfFit = m.directionOfFit

The sincerity condition's direction of fit matches the speech act's: [Sea83]'s central F(p) / S(r) parallel.

Causal self-referentiality

inductive CausalSelfRef : Type

Whether an Intentional state must figure in the causal chain producing its own conditions of satisfaction ([Sea83]).

• none : CausalSelfRef

  Not self-referential (beliefs, desires).

• stateToWorld : CausalSelfRef

  The state must cause its conditions of satisfaction (intentions).

• worldToState : CausalSelfRef

  The conditions of satisfaction must cause the state (perceptions).

@[implicit_reducible]

instance instDecidableEqCausalSelfRef : DecidableEq CausalSelfRef

Equations

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

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

Equations

• instReprCausalSelfRef.repr CausalSelfRef.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausalSelfRef.none")).group prec✝
• instReprCausalSelfRef.repr CausalSelfRef.stateToWorld prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausalSelfRef.stateToWorld")).group prec✝
• instReprCausalSelfRef.repr CausalSelfRef.worldToState prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausalSelfRef.worldToState")).group prec✝

@[implicit_reducible]

instance instReprCausalSelfRef : Repr CausalSelfRef

Equations

• instReprCausalSelfRef = { reprPrec := instReprCausalSelfRef.repr }

@[implicit_reducible]

instance instInhabitedCausalSelfRef : Inhabited CausalSelfRef

Equations

• instInhabitedCausalSelfRef = { default := instInhabitedCausalSelfRef.default }

def PsychMode.causalSelfRef : PsychMode → CausalSelfRef

Causal self-referentiality for each psychological mode. Perception's direction of causation (world-to-state) runs opposite its direction of fit (mind-to-world): the two axes are independent.

Equations

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

theorem PsychMode.causalSelfRef_not_determined_by_directionOfFit : ∃ (a : PsychMode) (b : PsychMode), a.directionOfFit = b.directionOfFit ∧ a.causalSelfRef ≠ b.causalSelfRef

Causal self-referentiality is not determined by direction of fit: belief and perception share mind-to-world fit but differ in self-referentiality.

Preparatory conditions

inductive PreparatoryCondition : Type

Preparatory conditions for directive speech acts. [Sea69] introduces the notion; the ability/knowledge/memory/perception/permission/willingness inventory and the specificity subsumption used below are consolidated in the analysis of [FC85] on indirect requests. -- UNVERIFIED: the precise subsumption ordering attribution.

• ability : PreparatoryCondition

  The hearer is able to perform the act.

• knowledge : PreparatoryCondition

  The hearer knows the relevant information.

• memory : PreparatoryCondition

  The hearer remembers the relevant information.

• perception : PreparatoryCondition

  The hearer can perceive the relevant object.

• permission : PreparatoryCondition

  The relevant permission obtains.

• willingness : PreparatoryCondition

  The hearer is willing to perform the act.

@[implicit_reducible]

instance instDecidableEqPreparatoryCondition : DecidableEq PreparatoryCondition

Equations

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

@[implicit_reducible]

instance instReprPreparatoryCondition : Repr PreparatoryCondition

Equations

• instReprPreparatoryCondition = { reprPrec := instReprPreparatoryCondition.repr }

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

Equations

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

@[implicit_reducible]

instance instInhabitedPreparatoryCondition : Inhabited PreparatoryCondition

Equations

• instInhabitedPreparatoryCondition = { default := instInhabitedPreparatoryCondition.default }

def PreparatoryCondition.subsumes : PreparatoryCondition → PreparatoryCondition → Prop

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

Equations

• PreparatoryCondition.ability.subsumes PreparatoryCondition.ability = True
• PreparatoryCondition.knowledge.subsumes PreparatoryCondition.knowledge = True
• PreparatoryCondition.memory.subsumes PreparatoryCondition.memory = True
• PreparatoryCondition.perception.subsumes PreparatoryCondition.perception = True
• PreparatoryCondition.permission.subsumes PreparatoryCondition.permission = True
• PreparatoryCondition.willingness.subsumes PreparatoryCondition.willingness = True
• PreparatoryCondition.ability.subsumes PreparatoryCondition.knowledge = True
• PreparatoryCondition.ability.subsumes PreparatoryCondition.memory = True
• PreparatoryCondition.ability.subsumes PreparatoryCondition.perception = True
• PreparatoryCondition.ability.subsumes PreparatoryCondition.permission = True
• PreparatoryCondition.knowledge.subsumes PreparatoryCondition.memory = True
• PreparatoryCondition.knowledge.subsumes PreparatoryCondition.perception = True
• x✝¹.subsumes x✝ = False

@[implicit_reducible]

instance instDecidableRelPreparatoryConditionSubsumes : DecidableRel PreparatoryCondition.subsumes

Equations

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

theorem PreparatoryCondition.subsumes_refl (c : PreparatoryCondition) : c.subsumes c

theorem PreparatoryCondition.specificity_chain : ability.subsumes knowledge ∧ knowledge.subsumes memory ∧ knowledge.subsumes perception ∧ ability.subsumes permission

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

theorem PreparatoryCondition.willingness_independent : ¬ability.subsumes willingness ∧ ¬willingness.subsumes ability

Willingness is independent of ability: neither subsumes the other.