Layered Assertive Clauses: JP/ComP modifiers

@cite{krifka-2020} @cite{speas-2004} @cite{wiltschko-2014}

Worked examples for @cite{krifka-2020}'s four-layer clause structure (TP > JP > ComP > ActP). The JP layer originates with @cite{speas-2004} and is developed crosslinguistically by @cite{wiltschko-2014}; @cite{krifka-2020} synthesises them with the commitment-space framework of @cite{krifka-2015} (see sibling Phenomena/Assertion/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 — Data bridges to Phenomena/Assertion/Basic.lean empirical data

Out of scope

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

def Phenomena.Assertion.Studies.Krifka2020.hedgeAsJP {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : Dialogue.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

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

theorem Phenomena.Assertion.Studies.Krifka2020.hedgeAsJP_content_eq {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : (hedgeAsJP la).content = la.content

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

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

Hedging sets epistemic status to weak.

theorem Phenomena.Assertion.Studies.Krifka2020.hedgeAsJP_commitmentStrength_eq {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : (hedgeAsJP la).commitmentStrength = la.commitmentStrength

Hedging does not affect commitment strength.

def Phenomena.Assertion.Studies.Krifka2020.oathAsComP {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : Dialogue.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

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

theorem Phenomena.Assertion.Studies.Krifka2020.oathAsComP_content_eq {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : (oathAsComP la).content = la.content

Oaths preserve content.

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

Oaths set commitment strength to strong.

theorem Phenomena.Assertion.Studies.Krifka2020.oathAsComP_epistemicStatus_eq {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : (oathAsComP la).epistemicStatus = la.epistemicStatus

Oaths do not affect epistemic status.

def Phenomena.Assertion.Studies.Krifka2020.hedgedOath {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : Dialogue.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 Phenomena.Assertion.Studies.Krifka2020.hedgeAsJP_oathAsComP_comm {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : hedgeAsJP (oathAsComP la) = oathAsComP (hedgeAsJP la)

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

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

Hedged oath has weak epistemic + strong commitment.

theorem Phenomena.Assertion.Studies.Krifka2020.hedgedOath_content_eq {W : Type u_1} (la : Dialogue.Krifka.LayeredAssertion W) : (hedgedOath la).content = la.content

Both layered modifications preserve TP content.

theorem Phenomena.Assertion.Studies.Krifka2020.hedge_data_bridge : (hedgeExamples.all fun (x : HedgedAssertionDatum) => x.reducesCommitment) = true ∧ Dialogue.Krifka.CommitmentStrength.weak.rank < Dialogue.Krifka.CommitmentStrength.standard.rank

All hedges reduce commitment, AND the JP-modifier mechanism produces a strictly lower-rank epistemic status than .standard. The data side is all_hedges_reduce from Phenomena/Assertion/Basic.lean; the mechanism side is the JP-modifier rank ordering.

theorem Phenomena.Assertion.Studies.Krifka2020.oath_data_bridge : (oathExamples.all fun (x : OathFormulaDatum) => x.increasesCommitment) = true ∧ Dialogue.Krifka.CommitmentStrength.strong.rank > Dialogue.Krifka.CommitmentStrength.standard.rank

All oaths increase commitment, AND the ComP-modifier mechanism produces a strictly higher-rank commitment strength than .standard. The data side is all_oaths_increase from Basic.lean; the mechanism side is the ComP-modifier rank ordering.