Documentation

Linglib.Core.Discourse.IllocutionaryForce

Illocutionary Force: F in F(p) #

@cite{searle-1969} @cite{searle-1979} @cite{searle-1983} @cite{lakoff-1970} @cite{francik-clark-1985}

The pragmatic-act side of the Searlean parallel: direction of fit, the five-class taxonomy, and preparatory conditions. The Intentional-state counterpart S(r) — psychological mode, sincerity conditions, causal self-referentiality, and IntentionalState — lives in Core/Discourse/Intentionality.lean. Discourse commitments live in Core/Discourse/Commitment.lean.

The mood-category material that used to live here was split out for mathlib-style cleanliness:

Core/Discourse/Roles.lean — DiscourseRole, resolveRole
Core/Mood/IllocutionaryMood.lean — IllocutionaryMood, moodAuthority

This file extends IllocutionaryMood with searleClass/directionOfFit, which depend on the act taxonomy below.

Organization #

§ 1. Direction of Fit: Searle's key classification principle
§ 2. Illocutionary Taxonomy: the five classes derived from direction of fit
§ 3. Preparatory Conditions: Searle's felicity conditions on directives
§ 4. Verification

inductive Core.Discourse.DirectionOfFit :

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.

Instances For

@[implicit_reducible]

instance Core.Discourse.instDecidableEqDirectionOfFit :

DecidableEq DirectionOfFit

Equations

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

@[implicit_reducible]

instance Core.Discourse.instReprDirectionOfFit :

Repr DirectionOfFit

Equations

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

def Core.Discourse.instReprDirectionOfFit.repr :

DirectionOfFit → ℕ → Std.Format

Equations

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

Instances For

def Core.Discourse.instInhabitedDirectionOfFit.default :

Equations

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

Instances For

@[implicit_reducible]

instance Core.Discourse.instInhabitedDirectionOfFit :

Inhabited DirectionOfFit

Equations

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

inductive Core.Discourse.SearleClass :

@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).

Instances For

@[implicit_reducible]

instance Core.Discourse.instDecidableEqSearleClass :

DecidableEq SearleClass

Equations

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

@[implicit_reducible]

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.

Instances For

@[implicit_reducible]

instance Core.Discourse.instInhabitedSearleClass :

Inhabited SearleClass

Equations

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

def Core.Discourse.instInhabitedSearleClass.default :

Equations

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

Instances For

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

Instances For

def Core.Mood.IllocutionaryMood.searleClass :

IllocutionaryMood → Discourse.SearleClass

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

Defined in the Core.Mood.IllocutionaryMood namespace so it is available via dot notation, even though the SearleClass taxonomy lives in Core.Discourse.

Equations

Instances For

def Core.Mood.IllocutionaryMood.directionOfFit (m : IllocutionaryMood) :

Discourse.DirectionOfFit

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

Equations

m.directionOfFit = m.searleClass.directionOfFit

Instances For

inductive Core.Discourse.PreparatoryCondition :

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.

Instances For

@[implicit_reducible]

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.instReprPreparatoryCondition.repr :

PreparatoryCondition → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Core.Discourse.instReprPreparatoryCondition :

Repr PreparatoryCondition

Equations

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

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

Instances For

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 :

Mood.moodAuthority Mood.IllocutionaryMood.declarative = DiscourseRole.speaker

theorem Core.Discourse.epistemic_authority_interrogative :

Mood.moodAuthority Mood.IllocutionaryMood.interrogative = DiscourseRole.addressee

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