Krifka: Commitment Space Semantics and Layered Assertive Clauses #

@cite{krifka-2015} @cite{krifka-2020}

Combines two strands of Krifka's work:

Commitment spaces: the discourse state is a tree — the root (√C) is the current CG, and continuations are proposed future states from questions. Assertion narrows every state (C + S⊢φ); questions preserve the root and add branches (C + ?φ). Per-agent commitment slates track individual public commitments, enabling the commitment/belief separation (lying, hedging).
Layered assertive clauses: four syntactic layers each contributing a distinct semantic dimension:

Layer	Contribution	Example Modifier
TP	Propositional content	tense, aspect
JP (Judge Phrase)	Epistemic judgment	"I think", evidentials
ComP (Commitment Phrase)	Commitment strength	"I swear", "perhaps"
ActP (Act Phrase)	Speech act type	declarative, imperative

JP and ComP are independent: "I think I swear p" vs "I swear I think p" both involve TP content p, but with different epistemic/commitment profiles.

Commitment Space Tree #

The discourse state is a CommitmentSpace tree (§4):

CommitmentSpace = { root : List Prop, continuations : List (List Prop) }

Assert C + S⊢φ: adds φ to root AND all continuations
Question C + ?φ: preserves root, adds continuation (root ∩ φ), narrows existing continuations by φ
Accept: promotes first continuation to root
Reject: prunes first continuation

source

inductive Theories.Pragmatics.Assertion.Krifka.ClauseLayer :

Type

The four syntactic layers of an assertive clause.

Ordered from innermost (TP, propositional content) to outermost (ActP, speech act force). Each layer contributes a distinct semantic dimension that can be independently modified.

TODO: @cite{krifka-2015} §4 also posits PolP (Polarity Phrase) between ComP and TP, hosting verum (⊢) / falsum (⊣). High negation at ComP (¬⊢φ = non-commitment to φ) vs TP negation (⊢¬φ = commitment to ¬φ) explains the bias asymmetry of negative questions: "Isn't it raining?" is biased toward rain because negation scopes over ⊢, not over φ.

TP : ClauseLayer
Tense Phrase: propositional content
JP : ClauseLayer
Judge Phrase: epistemic status (certainty/uncertainty)
ComP : ClauseLayer
Commitment Phrase: commitment strength
ActP : ClauseLayer
Act Phrase: speech act type

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instDecidableEqClauseLayer :

DecidableEq ClauseLayer

Equations

Theories.Pragmatics.Assertion.Krifka.instDecidableEqClauseLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Theories.Pragmatics.Assertion.Krifka.instReprClauseLayer.repr :

ClauseLayer → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instReprClauseLayer :

Repr ClauseLayer

Equations

Theories.Pragmatics.Assertion.Krifka.instReprClauseLayer = { reprPrec := Theories.Pragmatics.Assertion.Krifka.instReprClauseLayer.repr }

source

def Theories.Pragmatics.Assertion.Krifka.instBEqClauseLayer.beq :

ClauseLayer → ClauseLayer → Bool

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqClauseLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instBEqClauseLayer :

BEq ClauseLayer

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqClauseLayer = { beq := Theories.Pragmatics.Assertion.Krifka.instBEqClauseLayer.beq }

source

instance Theories.Pragmatics.Assertion.Krifka.instInhabitedClauseLayer :

Inhabited ClauseLayer

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedClauseLayer = { default := Theories.Pragmatics.Assertion.Krifka.instInhabitedClauseLayer.default }

source

def Theories.Pragmatics.Assertion.Krifka.instInhabitedClauseLayer.default :

ClauseLayer

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedClauseLayer.default = Theories.Pragmatics.Assertion.Krifka.ClauseLayer.TP

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.ClauseLayer.rank :

ClauseLayer → ℕ

Rank ordering of clause layers (innermost = 0).

Equations

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.tp_innermost (l : ClauseLayer) :

ClauseLayer.TP.rank ≤ l.rank

TP is the innermost layer.

source

inductive Theories.Pragmatics.Assertion.Krifka.CommitmentStrength :

Type

Graded commitment strength, controlled by ComP modifiers.

weak: hedged ("I think p", "maybe p")
standard: default declarative assertion
strong: oath formulae ("I swear p", "I promise p")

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instDecidableEqCommitmentStrength :

DecidableEq CommitmentStrength

Equations

Theories.Pragmatics.Assertion.Krifka.instDecidableEqCommitmentStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Theories.Pragmatics.Assertion.Krifka.instReprCommitmentStrength.repr :

CommitmentStrength → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instReprCommitmentStrength :

Repr CommitmentStrength

Equations

Theories.Pragmatics.Assertion.Krifka.instReprCommitmentStrength = { reprPrec := Theories.Pragmatics.Assertion.Krifka.instReprCommitmentStrength.repr }

source

instance Theories.Pragmatics.Assertion.Krifka.instBEqCommitmentStrength :

BEq CommitmentStrength

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqCommitmentStrength = { beq := Theories.Pragmatics.Assertion.Krifka.instBEqCommitmentStrength.beq }

source

def Theories.Pragmatics.Assertion.Krifka.instBEqCommitmentStrength.beq :

CommitmentStrength → CommitmentStrength → Bool

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqCommitmentStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instInhabitedCommitmentStrength :

Inhabited CommitmentStrength

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedCommitmentStrength = { default := Theories.Pragmatics.Assertion.Krifka.instInhabitedCommitmentStrength.default }

source

def Theories.Pragmatics.Assertion.Krifka.instInhabitedCommitmentStrength.default :

CommitmentStrength

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedCommitmentStrength.default = Theories.Pragmatics.Assertion.Krifka.CommitmentStrength.weak

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentStrength.rank :

CommitmentStrength → ℕ

Numerical ordering of commitment strengths.

Equations

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.standard_is_default :

CommitmentStrength.standard.rank = 1

Standard is the default.

source

theorem Theories.Pragmatics.Assertion.Krifka.strength_ordering :

CommitmentStrength.weak.rank < CommitmentStrength.standard.rank ∧ CommitmentStrength.standard.rank < CommitmentStrength.strong.rank

Strong > standard > weak.

source

structure Theories.Pragmatics.Assertion.Krifka.LayeredAssertion (W : Type u_1) :

Type u_1

A fully layered assertion, decomposed into the four clause layers.

Each layer is independent: the epistemic status (JP) can vary without affecting the commitment strength (ComP), and vice versa. The actType uses IllocutionaryMood from Core/Discourse/DiscourseRole.lean.

content : BProp W
TP: the propositional content
epistemicStatus : CommitmentStrength
JP: the speaker's epistemic status toward the content
commitmentStrength : CommitmentStrength
ComP: the strength of the speaker's public commitment
actType : Core.Discourse.IllocutionaryMood
ActP: the type of speech act performed

Instances For

source

inductive Theories.Pragmatics.Assertion.Krifka.KAgent :

Type

Agent type for two-participant discourse.

speaker : KAgent
addressee : KAgent

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instDecidableEqKAgent :

DecidableEq KAgent

Equations

Theories.Pragmatics.Assertion.Krifka.instDecidableEqKAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Theories.Pragmatics.Assertion.Krifka.instReprKAgent :

Repr KAgent

Equations

Theories.Pragmatics.Assertion.Krifka.instReprKAgent = { reprPrec := Theories.Pragmatics.Assertion.Krifka.instReprKAgent.repr }

source

def Theories.Pragmatics.Assertion.Krifka.instReprKAgent.repr :

KAgent → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instBEqKAgent :

BEq KAgent

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqKAgent = { beq := Theories.Pragmatics.Assertion.Krifka.instBEqKAgent.beq }

source

def Theories.Pragmatics.Assertion.Krifka.instBEqKAgent.beq :

KAgent → KAgent → Bool

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqKAgent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instInhabitedKAgent :

Inhabited KAgent

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedKAgent = { default := Theories.Pragmatics.Assertion.Krifka.instInhabitedKAgent.default }

source

def Theories.Pragmatics.Assertion.Krifka.instInhabitedKAgent.default :

KAgent

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedKAgent.default = Theories.Pragmatics.Assertion.Krifka.KAgent.speaker

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KAgent.toDiscourseRole :

KAgent → Core.Discourse.DiscourseRole

Bridge KAgent to the framework-agnostic DiscourseRole. Both encode the same two-participant distinction.

Equations

Instances For

source

structure Theories.Pragmatics.Assertion.Krifka.CommitmentSpace (W : Type u_1) :

Type u_1

A commitment space (@cite{krifka-2015}, Definition 3, p.329).

A set of commitment states organized as root + continuations:

root (√C): the current commitment state — what is actually in the common ground. All worlds compatible with the root propositions are "live".
continuations: proposed future states, each extending the root. Added by questions, resolved by acceptance or rejection.

Krifka's key operations:

Assert C + S⊢φ = {s ∩ ⟦φ⟧ : s ∈ C}: narrow every state by φ
Question C + ?φ = {√C} ∪ (C + S₂⊢φ): preserve root, propose φ
Accept: take a continuation as the new root
Reject: prune a continuation

The tree structure captures the assertion/question asymmetry: assertions modify the root (the CG changes), while questions only add continuations (the CG is preserved until acceptance).

root : List (BProp W)
Root commitment state √C: propositions currently in the CG
continuations : List (List (BProp W))
Proposed future states. Questions add these; acceptance promotes one to root. Each continuation is a list of propositions that extends (narrows) the root.

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.empty {W : Type u_1} :

CommitmentSpace W

The empty commitment space: no commitments, no continuations.

Equations

Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.empty = { root := [], continuations := [] }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.assert {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) :

CommitmentSpace W

Assert φ: narrow every state by φ (@cite{krifka-2015}, (9), p.329).

C + S⊢φ = {s ∩ ⟦φ⟧ : s ∈ C}

Adds φ to the root AND all continuations. Any accepted continuation will also entail φ.

Equations

cs.assert φ = { root := φ :: cs.root, continuations := List.map (fun (x : List (BProp W)) => φ :: x) cs.continuations }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.question {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) :

CommitmentSpace W

Question: preserve root, propose φ (@cite{krifka-2015}, (14), p.332).

C + ?φ = {√C} ∪ (C + S₂⊢φ)

The root stays unchanged (CG preserved). A new continuation is added (root narrowed by φ), and existing continuations are also narrowed by φ. The addressee can accept (promote continuation to root) or reject (prune it).

Equations

cs.question φ = { root := cs.root, continuations := (φ :: cs.root) :: List.map (fun (x : List (BProp W)) => φ :: x) cs.continuations }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.isSettled {W : Type u_1} :

CommitmentSpace W → Bool

The space is settled: no open continuations. A settled space has no unresolved proposals.

Equations

{ root := root, continuations := [] }.isSettled = true
{ root := root, continuations := head :: tail }.isSettled = false

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.acceptFirst {W : Type u_1} :

CommitmentSpace W → CommitmentSpace W

Accept the first continuation: it becomes the new root. The CG is updated to the accepted proposal's content.

Equations

{ root := root, continuations := c :: rest }.acceptFirst = { root := c, continuations := rest }
x✝.acceptFirst = x✝

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.rejectFirst {W : Type u_1} :

CommitmentSpace W → CommitmentSpace W

Reject the first continuation: prune it. The CG is unchanged; the proposal is discarded.

Equations

{ root := root, continuations := c :: rest }.rejectFirst = { root := root, continuations := rest }
x✝.rejectFirst = x✝

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.toContextSet {W : Type u_1} (cs : CommitmentSpace W) :

Core.CommonGround.ContextSet W

Context set from root: worlds compatible with all root propositions.

Equations

cs.toContextSet w = ((cs.root.all fun (x : BProp W) => x w) = true)

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.empty_settled {W : Type u_1} :

empty.isSettled = true

Empty space is settled.

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.assert_preserves_settled {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) (h : cs.isSettled = true) :

(cs.assert φ).isSettled = true

Assertion preserves settledness.

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.question_unsettles {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) (h : cs.isSettled = true) :

(cs.question φ).isSettled = false

Question makes a settled space unsettled (adds a continuation).

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.accept_resettles_simple {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) (h : cs.isSettled = true) :

(cs.question φ).acceptFirst.isSettled = true

Accepting a simple question's sole continuation re-settles.

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.assert_in_root {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) :

φ ∈ (cs.assert φ).root

Root after assertion contains the asserted proposition.

source

theorem Theories.Pragmatics.Assertion.Krifka.CommitmentSpace.question_preserves_root {W : Type u_1} (cs : CommitmentSpace W) (φ : BProp W) :

(cs.question φ).root = cs.root

Question preserves root commitments.

source

structure Theories.Pragmatics.Assertion.Krifka.KrifkaState (W : Type u_1) :

Type u_1

Krifka's discourse state: per-agent commitment slates + shared commitment space (tree).

The commitment space tracks the shared discourse structure: what's in the CG (root) and what's been proposed (continuations). Per-agent slates track individual public commitments, enabling the commitment/belief separation central to Krifka's theory.

speakerCS : Core.Discourse.Commitment.CommitmentSlate W
Speaker's individual commitment slate
addresseeCS : Core.Discourse.Commitment.CommitmentSlate W
Addressee's individual commitment slate
space : CommitmentSpace W
Shared commitment space (tree): CG + proposed updates

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.empty {W : Type u_1} :

KrifkaState W

Initial state: no commitments, empty settled space.

Equations

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

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.commitOp {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

KrifkaState W

Krifka's commitment operator + S₁⊢p (@cite{krifka-2015}, (9)): speaker commits to p, narrowing the entire space.

Equations

s.commitOp p = { speakerCS := s.speakerCS.add p, addresseeCS := s.addresseeCS, space := s.space.assert p }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.accept {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

KrifkaState W

Accept: addressee also commits to p (after speaker's assertion).

Equations

s.accept p = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS.add p, space := s.space }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.assert {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

KrifkaState W

Assert = commit (@cite{krifka-2015}: assertion IS commitment). The space is narrowed immediately; the CG reflects the assertion.

Equations

s.assert p = s.commitOp p

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.question {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

KrifkaState W

Question: speaker proposes φ as a continuation (@cite{krifka-2015}, (14)). The CG (root) is unchanged; a new continuation is added.

Equations

s.question p = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.question p }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.acceptContinuation {W : Type u_1} (s : KrifkaState W) :

KrifkaState W

Accept the first continuation: it becomes the new CG.

Equations

s.acceptContinuation = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.acceptFirst }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.rejectContinuation {W : Type u_1} (s : KrifkaState W) :

KrifkaState W

Reject the first continuation: prune it.

Equations

s.rejectContinuation = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.rejectFirst }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.retract {W : Type u_1} (s : KrifkaState W) (p : BProp W) [BEq (BProp W)] :

KrifkaState W

Retract: remove a commitment from the speaker's slate.

Equations

s.retract p = { speakerCS := s.speakerCS.retract p, addresseeCS := s.addresseeCS, space := s.space }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.contextSet {W : Type u_1} (s : KrifkaState W) :

Core.CommonGround.ContextSet W

Context set: from the commitment space root (= CG).

Equations

s.contextSet = s.space.toContextSet

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.KrifkaState.isStable {W : Type u_1} (s : KrifkaState W) :

Bool

Stability: the space is settled (no open proposals).

Equations

s.isStable = s.space.isSettled

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.comp_preserves_content {W : Type u_1} (la : LayeredAssertion W) (str : CommitmentStrength) :

{ content := la.content, epistemicStatus := la.epistemicStatus, commitmentStrength := str, actType := la.actType }.content = la.content

ComP preserves TP content: changing commitment strength does not change the propositional content.

source

theorem Theories.Pragmatics.Assertion.Krifka.jp_comp_independent {W : Type u_1} (la : LayeredAssertion W) (ep cs : CommitmentStrength) :

{ content := la.content, epistemicStatus := ep, commitmentStrength := cs, actType := la.actType }.content = la.content ∧ { content := la.content, epistemicStatus := ep, commitmentStrength := la.commitmentStrength, actType := la.actType }.commitmentStrength = la.commitmentStrength ∧ { content := la.content, epistemicStatus := la.epistemicStatus, commitmentStrength := cs, actType := la.actType }.epistemicStatus = la.epistemicStatus

JP and ComP are independent: changing one does not affect the other.

source

theorem Theories.Pragmatics.Assertion.Krifka.actp_declarative_default {W : Type u_1} (p : BProp W) :

{ content := p }.actType = Core.Discourse.IllocutionaryMood.declarative

Krifka's ActP layer directly uses IllocutionaryMood, grounding the clause-type distinction in the speech act classification.

source

inductive Theories.Pragmatics.Assertion.Krifka.UpdateType :

Type

Update type for assertions.

Krifka distinguishes two fundamentally different ways an assertion can change the common ground:

informative (·φ): eliminates worlds incompatible with φ. c + ·φ = {i | i ∈ c ∧ φ(i)} Example: "The meeting is at 5" — reduces uncertainty.
performative (•φ): changes world indices so φ becomes true. c + •φ = {i' | ∃ i ∈ c, i ⇒_φ i'} Example: "I hereby name this ship the Queen Elizabeth" — makes φ true by the act of uttering it.

This distinction is orthogonal to commitment strength (ComP) and epistemic status (JP).

informative : UpdateType
performative : UpdateType

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instDecidableEqUpdateType :

DecidableEq UpdateType

Equations

Theories.Pragmatics.Assertion.Krifka.instDecidableEqUpdateType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Theories.Pragmatics.Assertion.Krifka.instReprUpdateType :

Repr UpdateType

Equations

Theories.Pragmatics.Assertion.Krifka.instReprUpdateType = { reprPrec := Theories.Pragmatics.Assertion.Krifka.instReprUpdateType.repr }

source

def Theories.Pragmatics.Assertion.Krifka.instReprUpdateType.repr :

UpdateType → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instBEqUpdateType :

BEq UpdateType

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqUpdateType = { beq := Theories.Pragmatics.Assertion.Krifka.instBEqUpdateType.beq }

source

def Theories.Pragmatics.Assertion.Krifka.instBEqUpdateType.beq :

UpdateType → UpdateType → Bool

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqUpdateType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instInhabitedUpdateType :

Inhabited UpdateType

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedUpdateType = { default := Theories.Pragmatics.Assertion.Krifka.instInhabitedUpdateType.default }

source

def Theories.Pragmatics.Assertion.Krifka.instInhabitedUpdateType.default :

UpdateType

Equations

Theories.Pragmatics.Assertion.Krifka.instInhabitedUpdateType.default = Theories.Pragmatics.Assertion.Krifka.UpdateType.informative

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.informativeUpdate {W : Type u_1} (cs : List W) (φ : BProp W) :

List W

Informative update: restrict context set to worlds satisfying φ. @cite{krifka-2020}, (7): c + ·φ = {i | i ∈ c ∧ φ(i)}

Equations

Theories.Pragmatics.Assertion.Krifka.informativeUpdate cs φ = List.filter φ cs

Instances For

source

structure Theories.Pragmatics.Assertion.Krifka.TypedAssertion (W : Type u_1) extends Theories.Pragmatics.Assertion.Krifka.LayeredAssertion W :

Type u_1

A fully specified assertion with update type.

content : BProp W
epistemicStatus : CommitmentStrength
commitmentStrength : CommitmentStrength
actType : Core.Discourse.IllocutionaryMood
updateType : UpdateType
Whether the update is informative or performative

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.default_assertion_informative {W : Type u_1} (p : BProp W) :

{ content := p }.updateType = UpdateType.informative

Default assertions are informative (the common case).

source

theorem Theories.Pragmatics.Assertion.Krifka.commitment_closure {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

(s.assert p).space.root = p :: s.space.root

Commitment Closure (@cite{krifka-2020}, (25)): assertion immediately narrows the commitment space. The root (CG) after asserting φ is the original root with φ prepended.

In the tree model, this is definitional: assert adds φ to all nodes including the root.

source

theorem Theories.Pragmatics.Assertion.Krifka.question_preserves_cg {W : Type u_1} (s : KrifkaState W) (p : BProp W) :

(s.question p).space.root = s.space.root

Questions don't change the CG: the root is preserved.

source

theorem Theories.Pragmatics.Assertion.Krifka.question_accept_eq_assert_root {W : Type u_1} (s : KrifkaState W) (p : BProp W) (h : s.space.isSettled = true) :

(s.question p).acceptContinuation.space.root = (s.assert p).space.root

Question then accept ≈ assert (on the root): accepting a question's sole continuation yields the same CG as a direct assertion.

This connects the two modes of updating: direct assertion (speaker imposes) and question-then-accept (speaker proposes, addressee accepts). The roots match because both produce φ :: root₀.

source

structure Theories.Pragmatics.Assertion.Krifka.ActorCommitter :

Type

The two discourse roles in a speech act.

Every speech act has an actor (who performs the act) and a committer (who undertakes the commitment). These can diverge:

Assertion: actor = speaker, committer = speaker
Monopolar question: actor = speaker, committer = addressee (the speaker proposes that the addressee commit)

This is the "one promising aspect" Krifka highlights in his conclusion: the framework naturally separates who acts from who commits, explaining why questions can be biased (the speaker chooses WHAT to propose) without being assertive (the addressee decides WHETHER to commit).

actor : KAgent
committer : KAgent

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instDecidableEqActorCommitter :

DecidableEq ActorCommitter

Equations

Theories.Pragmatics.Assertion.Krifka.instDecidableEqActorCommitter = Theories.Pragmatics.Assertion.Krifka.instDecidableEqActorCommitter.decEq

source

def Theories.Pragmatics.Assertion.Krifka.instDecidableEqActorCommitter.decEq (x✝ x✝¹ : ActorCommitter) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instReprActorCommitter :

Repr ActorCommitter

Equations

Theories.Pragmatics.Assertion.Krifka.instReprActorCommitter = { reprPrec := Theories.Pragmatics.Assertion.Krifka.instReprActorCommitter.repr }

source

def Theories.Pragmatics.Assertion.Krifka.instReprActorCommitter.repr :

ActorCommitter → ℕ → Std.Format

Equations

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

Instances For

source

instance Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter :

BEq ActorCommitter

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter = { beq := Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter.beq }

source

def Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter.beq :

ActorCommitter → ActorCommitter → Bool

Equations

Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter.beq { actor := a, committer := a_1 } { actor := b, committer := b_1 } = (a == b && a_1 == b_1)
Theories.Pragmatics.Assertion.Krifka.instBEqActorCommitter.beq x✝¹ x✝ = false

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.assertionRoles :

ActorCommitter

In assertions, speaker is both actor and committer.

Equations

Theories.Pragmatics.Assertion.Krifka.assertionRoles = { actor := Theories.Pragmatics.Assertion.Krifka.KAgent.speaker, committer := Theories.Pragmatics.Assertion.Krifka.KAgent.speaker }

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.questionRoles :

ActorCommitter

In monopolar questions, speaker acts but addressee commits. @cite{krifka-2015}, (16): C +_{S₁} [? [⊢ p]] proposes that S₂ commit to p.

Equations

Theories.Pragmatics.Assertion.Krifka.questionRoles = { actor := Theories.Pragmatics.Assertion.Krifka.KAgent.speaker, committer := Theories.Pragmatics.Assertion.Krifka.KAgent.addressee }

Instances For

source

theorem Theories.Pragmatics.Assertion.Krifka.actor_committer_diverge :

assertionRoles.actor = questionRoles.actor ∧ assertionRoles.committer ≠ questionRoles.committer

Assertions and questions differ in who commits.

source

structure Theories.Pragmatics.Assertion.Krifka.SpeechAct (W : Type u_1) :

Type u_1

A speech act in Krifka's framework: ActP content with its discourse function (assertion vs question).

@cite{krifka-2015} clause structure: ActP > ComP > TP (three layers). The 2020 paper refines this to ActP > ComP > JP > TP.

content : BProp W
Propositional content (TP layer)
actType : Core.Discourse.IllocutionaryMood
Speech act type: assertion (.) or question (?)
roles : ActorCommitter
Actor/committer assignment

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.monopolarQuestion {W : Type u_1} (φ : BProp W) :

SpeechAct W

Monopolar question: proposes a single continuation where the addressee commits to φ.

C +_{S₁} [? [⊢ φ]] = {√C} ∪ (C + S₂⊢φ)

The root is preserved ({√C}) alongside the proposed continuation (C + S₂⊢φ). The addressee can accept (take the continuation) or reject (stay at root). This is what makes it a QUESTION rather than an assertion — the commitment is proposed, not imposed.

Monopolar questions are inherently biased toward the proposed continuation.

Equations

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

Instances For

source

inductive Theories.Pragmatics.Assertion.Krifka.ComplexSpeechAct (W : Type u_1) :

Type u_1

Complex speech act: conjunction or disjunction of atomic acts.

@cite{krifka-2015}, §5: question tags involve composition of speech acts. The difference between matching and reverse tags is conjunction vs disjunction:

conj: both acts performed sequentially (matching tag)
disj: addressee chooses one continuation (reverse tag)

atom {W : Type u_1} : SpeechAct W → ComplexSpeechAct W
A single speech act.
conj {W : Type u_1} : SpeechAct W → SpeechAct W → ComplexSpeechAct W
Conjunction: perform both acts sequentially. "It's raining, isn't it?" = ASSERT(rain) ∧ ASK(rain).
disj {W : Type u_1} : SpeechAct W → SpeechAct W → ComplexSpeechAct W
Disjunction: offer alternative continuations. "It's raining, or isn't it?" = ASSERT(rain) ∨ ASK(¬rain).

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.ComplexSpeechAct.components {W : Type u_1} :

ComplexSpeechAct W → List (SpeechAct W)

Extract the component speech acts from a complex speech act.

Equations

Instances For

source

def Theories.Pragmatics.Assertion.Krifka.matchingTag {W : Type u_1} (φ : BProp W) :

ComplexSpeechAct W

A matching question tag: conjunction of assertion + monopolar question with same content.

"It's raining, isn't it?" = speaker asserts rain AND asks addressee to confirm. The speaker has already committed, so the question is biased toward the asserted content.

Equations