Layered Assertive Clauses: JP/ComP modifiers

[Kri20] [Spe04] [Wil14]

Worked examples for [Kri20]'s four-layer clause structure (TP > JP > ComP > ActP). The JP layer originates with [Spe04] and is developed crosslinguistically by [Wil14]; [Kri20] synthesises them with the commitment-space framework of [Kri15a] (see sibling Studies/Krifka2015.lean).

Coverage

• §1 — Hedges as JP modifiers ("I think p" → epistemicStatus := weak)
• §2 — Oaths as ComP modifiers ("I swear p" → commitmentStrength := strong)
• §3 — JP/ComP independence (commute, layer non-interaction)
• §4 — Rank orderings: hedges weaken, oaths strengthen, relative to the .standard default

Out of scope

• The actual commitment-space dynamics — see Krifka2015.lean.
• Proxy assertions ("Mary says p") — flagged in [Kri15a] conclusion, not exercised here.
• Conjunct/disjunct systems (Newari etc.) — typological extension noted in [Kri15a] conclusion but separate study.

Layered Assertive Clauses

[Kri20] [Spe04] [Wil14]

Four-layer decomposition of an assertive clause from [Kri20]: TP (propositional content), JP (epistemic judgement), ComP (commitment strength), ActP (speech act type). JP terminology and the layered idea trace to [Spe04] and [Wil14]; [Kri20] synthesises them with the commitment-space framework.

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.

This file is sibling to Discourse/Commitment/Space.lean (the 2015 commitment-space framework). The two are independent — neither imports the other — and study files target whichever is appropriate:

• Studies/Krifka2015.lean consumes CommitmentSpace
• Studies/Krifka2020.lean consumes this file

inductive Discourse.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")

• weak : CommitmentStrength
• standard : CommitmentStrength
• strong : CommitmentStrength

@[implicit_reducible]

instance Discourse.Krifka.instDecidableEqCommitmentStrength : DecidableEq CommitmentStrength

Equations

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

@[implicit_reducible]

instance Discourse.Krifka.instReprCommitmentStrength : Repr CommitmentStrength

Equations

• Discourse.Krifka.instReprCommitmentStrength = { reprPrec := Discourse.Krifka.instReprCommitmentStrength.repr }

def Discourse.Krifka.instReprCommitmentStrength.repr : CommitmentStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.Krifka.instInhabitedCommitmentStrength : Inhabited CommitmentStrength

Equations

• Discourse.Krifka.instInhabitedCommitmentStrength = { default := Discourse.Krifka.instInhabitedCommitmentStrength.default }

def Discourse.Krifka.CommitmentStrength.rank : CommitmentStrength → ℕ

Numerical ordering of commitment strengths.

Equations

• Discourse.Krifka.CommitmentStrength.weak.rank = 0
• Discourse.Krifka.CommitmentStrength.standard.rank = 1
• Discourse.Krifka.CommitmentStrength.strong.rank = 2

theorem Discourse.Krifka.standard_is_default : CommitmentStrength.standard.rank = 1

Standard is the default.

theorem Discourse.Krifka.strength_ordering : CommitmentStrength.weak.rank < CommitmentStrength.standard.rank ∧ CommitmentStrength.standard.rank < CommitmentStrength.strong.rank

Strong > standard > weak.

structure Discourse.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 Discourse/SpeechAct.lean.

• content : Set 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 : Semantics.Mood.IllocutionaryMood

  ActP: the type of speech act performed

inductive Discourse.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 φ. Example: "The meeting is at 5" — reduces uncertainty.

• performative (•φ): changes world indices so φ becomes true. 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

@[implicit_reducible]

instance Discourse.Krifka.instDecidableEqUpdateType : DecidableEq UpdateType

Equations

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

def Discourse.Krifka.instReprUpdateType.repr : UpdateType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.Krifka.instReprUpdateType : Repr UpdateType

Equations

• Discourse.Krifka.instReprUpdateType = { reprPrec := Discourse.Krifka.instReprUpdateType.repr }

@[implicit_reducible]

instance Discourse.Krifka.instInhabitedUpdateType : Inhabited UpdateType

Equations

• Discourse.Krifka.instInhabitedUpdateType = { default := Discourse.Krifka.instInhabitedUpdateType.default }

def Discourse.Krifka.informativeUpdate {W : Type u_1} (cs : List W) (φ : W → Prop) [DecidablePred φ] : List W

Informative update: restrict context set to worlds satisfying φ.

-- UNVERIFIED: [Kri20] eq. number for the informative-update -- definition (the 2020 paper PDF was not available for this audit; -- the underlying concept is clearly Krifka's, but the equation tag -- needs human verification before promoting to a precise citation).

Equations

• Discourse.Krifka.informativeUpdate cs φ = List.filter (fun (w : W) => decide (φ w)) cs

structure Discourse.Krifka.TypedAssertion (W : Type u_1) extends Discourse.Krifka.LayeredAssertion W : Type u_1

A fully specified assertion with update type.

• content : Set W
• epistemicStatus : CommitmentStrength
• commitmentStrength : CommitmentStrength
• actType : Semantics.Mood.IllocutionaryMood
• updateType : UpdateType

  Whether the update is informative or performative

theorem Discourse.Krifka.default_assertion_informative {W : Type u_1} (p : Set W) : { content := p }.updateType = UpdateType.informative

Default assertions are informative (the common case).

def Krifka2020.hedgeAsJP {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : Discourse.Krifka.LayeredAssertion W

A hedge modifies the JP layer (epistemic status) to weak.

"I think p" = assertion with epistemicStatus := .weak. The TP content (p) is unchanged; only the JP layer is modified.

Equations

• Krifka2020.hedgeAsJP la = { content := la.content, epistemicStatus := Discourse.Krifka.CommitmentStrength.weak, commitmentStrength := la.commitmentStrength, actType := la.actType }

theorem Krifka2020.hedgeAsJP_content_eq {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgeAsJP la).content = la.content

Hedging preserves content (TP is untouched by JP modification).

theorem Krifka2020.hedgeAsJP_epistemicStatus_eq_weak {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgeAsJP la).epistemicStatus = Discourse.Krifka.CommitmentStrength.weak

Hedging sets epistemic status to weak.

theorem Krifka2020.hedgeAsJP_commitmentStrength_eq {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgeAsJP la).commitmentStrength = la.commitmentStrength

Hedging does not affect commitment strength.

def Krifka2020.oathAsComP {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : Discourse.Krifka.LayeredAssertion W

An oath modifies the ComP layer (commitment strength) to strong.

"I swear p" = assertion with commitmentStrength := .strong. The TP content (p) is unchanged; only the ComP layer is modified.

Equations

• Krifka2020.oathAsComP la = { content := la.content, epistemicStatus := la.epistemicStatus, commitmentStrength := Discourse.Krifka.CommitmentStrength.strong, actType := la.actType }

theorem Krifka2020.oathAsComP_content_eq {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (oathAsComP la).content = la.content

Oaths preserve content.

theorem Krifka2020.oathAsComP_commitmentStrength_eq_strong {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (oathAsComP la).commitmentStrength = Discourse.Krifka.CommitmentStrength.strong

Oaths set commitment strength to strong.

theorem Krifka2020.oathAsComP_epistemicStatus_eq {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (oathAsComP la).epistemicStatus = la.epistemicStatus

Oaths do not affect epistemic status.

def Krifka2020.hedgedOath {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : Discourse.Krifka.LayeredAssertion W

JP and ComP can co-occur: hedging + oath on the same assertion.

"I think I swear p": epistemicStatus = weak, commitmentStrength = strong. "I swear I think p": same result (layers are independent).

Equations

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

theorem Krifka2020.hedgeAsJP_oathAsComP_comm {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : hedgeAsJP (oathAsComP la) = oathAsComP (hedgeAsJP la)

Order doesn't matter: hedge(oath(la)) = oath(hedge(la)).

theorem Krifka2020.hedgedOath_profile {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgedOath la).epistemicStatus = Discourse.Krifka.CommitmentStrength.weak ∧ (hedgedOath la).commitmentStrength = Discourse.Krifka.CommitmentStrength.strong

Hedged oath has weak epistemic + strong commitment.

theorem Krifka2020.hedgedOath_content_eq {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgedOath la).content = la.content

Both layered modifications preserve TP content.

theorem Krifka2020.hedgeAsJP_rank_lt_standard {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (hedgeAsJP la).epistemicStatus.rank < Discourse.Krifka.CommitmentStrength.standard.rank

Hedging produces a strictly lower-rank epistemic status than the .standard default: "I think p" weakens the assertion.

theorem Krifka2020.oathAsComP_rank_gt_standard {W : Type u_1} (la : Discourse.Krifka.LayeredAssertion W) : (oathAsComP la).commitmentStrength.rank > Discourse.Krifka.CommitmentStrength.standard.rank

Oaths produce a strictly higher-rank commitment strength than the .standard default: "I swear p" strengthens the assertion.