Krifka (2020): Layers of Assertive Clauses: Propositions, Judgements, Commitments, Acts

This file formalizes [Kri20]'s decomposition of an assertive clause into a proposition (TP), a private judgement of it (JP), a public commitment to that judgement (ComP), and the act that updates the common ground (ActP). A judgement phrase abstracts over the judge of a judge-relative proposition (Judgement); the commitment phrase turns it into the proposition that the judge is publicly responsible for its truth (comP); the assertive act performs a performative update, which does not restrict the common ground but moves each of its indices to a successor at which the speaker's commitment holds (performative), in contrast to the informative update of [Sta78] (informative). Commitment closure, the pragmatic step licensed once every index records a trustworthy speaker's commitment, then adds the judgement itself (assertClosed), and judgement closure adds the proposition judged. On this account a subjective epistemic adverb like sicherlich commits the speaker only to their own certainty, a proposition easier to defend than the one communicated (commits_certainly), and a reportative like laut Eva commits the speaker to Eva's commitment. The layers are ordered, and clause-embedding predicates select a layer: abhängen a proposition, glauben and wissen a judgement, sagen a commitment, so which modifiers a complement clause admits follows from the layer selected (Licensed).

Implementation notes

• The branching successor relation i ⊶ i′[φ] is a primitive with its one axiom, that φ holds at the successor; a model supplies it together with the commitment and certainty relations. Judgements and commitments share the type of functions from judges to propositions, the paper's sortal distinction being carried by the operators that build them.
• The closures are informative updates under their conditions, the trustworthiness and the absence of objection being left to the discourse.
• Commitment strength (§3.2) is not modelled: the paper argues it has no discrete values on a single dimension. The report readings under which wissen and glauben embed commitment modifiers are noted, not modelled.

References

• [Kri20]
• [Kri15a] — commitment spaces, the framework the layers refine
• [Sta78] — informative update
• [FB10] — assertions that stick to the common ground even when rejected

Propositions, judgements, commitments, acts

@[reducible, inline]

abbrev Krifka2020.Judgement (Judge : Type u_3) (Index : Type u_4) : Type (max u_3 u_4)

A judge-relative proposition, the meaning of a TP (19), or of a judgement phrase (20), which makes the judge accessible.

Equations

• Krifka2020.Judgement Judge Index = (Judge → Index → Prop)

structure Krifka2020.Model (Judge : Type u_3) (Index : Type u_4) : Type (max u_3 u_4)

The primitives of the semantics: public commitment x ⊢ᵢ φ, the certainty operator of (42), and the branching successor i ⊶ i′[φ], at which φ holds.

• commits : Judge → Index → (Index → Prop) → Prop
• cert : Judge → Index → (Index → Prop) → Prop
• succ : Index → (Index → Prop) → Index → Prop
• succ_holds (i : Index) (φ : Index → Prop) (i' : Index) : self.succ i φ i' → φ i'

def Krifka2020.comP {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (J : Judgement Judge Index) : Judgement Judge Index

The commitment phrase (21): the judge is publicly responsible for the truth of the judgement.

Equations

• Krifka2020.comP M J j i = M.commits j i (J j)

def Krifka2020.informative {Index : Type u_2} (c : Set Index) (φ : Index → Prop) : Set Index

Informative update (22): restriction of the common ground.

Equations

• Krifka2020.informative c φ = {i : Index | i ∈ c ∧ φ i}

def Krifka2020.performative {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (c : Set Index) (φ : Index → Prop) : Set Index

Performative update (23): each index moves to a successor at which the proposition holds.

Equations

• Krifka2020.performative M c φ = {i' : Index | ∃ i ∈ c, M.succ i φ i'}

def Krifka2020.assert {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (s : Judge) (c : Set Index) (J : Judgement Judge Index) : Set Index

The assertive act (24): the performative update with the commitment phrase applied to the speaker.

Equations

• Krifka2020.assert M s c J = Krifka2020.performative M c (Krifka2020.comP M J s)

def Krifka2020.assertClosed {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (s : Judge) (c : Set Index) (J : Judgement Judge Index) : Set Index

Commitment closure (25) after an assertion ((26), (27)): the judgement the speaker is committed to is added to the common ground.

Equations

• Krifka2020.assertClosed M s c J = Krifka2020.informative (Krifka2020.assert M s c J) (J s)

def Krifka2020.certainly {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (J : Judgement Judge Index) : Judgement Judge Index

A subjective epistemic adverb (42): the judge is certain of the judgement.

Equations

• Krifka2020.certainly M J j i = M.cert j i (J j)

def Krifka2020.according {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (x : Judge) (J : Judgement Judge Index) : Judgement Judge Index

A reportative evidential (53): another authority is committed to the judgement.

Equations

• Krifka2020.according M x J x✝ i = M.commits x i (J x)

def Krifka2020.allegedly {Judge : Type u_1} {Index : Type u_2} (M : Model Judge Index) (J : Judgement Judge Index) : Judgement Judge Index

Allegedly (55): some authority is committed to the judgement.

Equations

• Krifka2020.allegedly M J x✝ i = ∃ (x : Judge), M.commits x i (J x)

theorem Krifka2020.informative_subset {Index : Type u_2} (c : Set Index) (φ : Index → Prop) : informative c φ ⊆ c

theorem Krifka2020.commits_of_mem_assert {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} {i : Index} (h : i ∈ assert M s c J) : M.commits s i (J s)

After an assertion every index records the speaker's commitment: the condition of commitment closure holds.

theorem Krifka2020.mem_assertClosed_iff {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} {i : Index} : i ∈ assertClosed M s c J ↔ (∃ i₀ ∈ c, M.succ i₀ (comP M J s) i) ∧ J s i

The communicated meaning (27): the commitment and, by closure, the judgement.

theorem Krifka2020.assertClosed_subset_assert {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} : assertClosed M s c J ⊆ assert M s c J

An assertion is rejected without loss: the commitment stays in the common ground even when closure is withheld ([FB10]).

Judgement modifiers

theorem Krifka2020.commits_certainly {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} {i : Index} (h : i ∈ assert M s c (certainly M J)) : M.commits s i fun (i : Index) => M.cert s i (J s)

Asserting a hedged judgement (46) commits the speaker to their certainty, not to the proposition.

theorem Krifka2020.cert_of_mem_assertClosed {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} {i : Index} (h : i ∈ assertClosed M s c (certainly M J)) : M.cert s i (J s)

After commitment closure the certainty holds, which is the condition of judgement closure (44), the step that introduces the proposition itself.

theorem Krifka2020.commits_according {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {s : Judge} {c : Set Index} {J : Judgement Judge Index} {i : Index} {x : Judge} (h : i ∈ assert M s c (according M x J)) : M.commits s i fun (i : Index) => M.commits x i (J x)

Asserting a reportative (53) commits the speaker to the authority's commitment, a dependent commitment that leaves the authority to blame.

theorem Krifka2020.according_certainly {Judge : Type u_1} {Index : Type u_2} {M : Model Judge Index} {J : Judgement Judge Index} (x : Judge) : (according M x (certainly M J) = fun (x_1 : Judge) (i : Index) => M.commits x i fun (i : Index) => M.cert x i (J x)) ∧ certainly M (according M x J) = fun (j : Judge) (i : Index) => M.cert j i fun (i : Index) => M.commits x i (J x)

Evidentials scope over epistemics (91): laut Eva sicherlich has Eva certain, sicherlich laut Eva has the speaker certain of Eva's commitment.

A model

def Krifka2020.steps : Model Unit ℕ

Indices as times, a commitment or a judgement being on record from the first step on, and the successor the next step.

Equations

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

def Krifka2020.snores : Judgement Unit ℕ

Max snores loudly from the first step on.

Equations

• Krifka2020.snores x✝ i = (0 < i)

theorem Krifka2020.assert_steps : assert steps () {0} snores = {1} ∧ assertClosed steps () {0} snores = {1}

The assertion from the initial index moves the common ground to the next step, where the speaker's commitment is on record, and closure keeps it, since the proposition holds there.

Layers and embedding

inductive Krifka2020.Layer : Type

The layers of an assertive clause, in the order of (88).

• tp : Layer
• jp : Layer
• comP : Layer
• actP : Layer

@[instance_reducible]

instance Krifka2020.instDecidableEqLayer : DecidableEq Layer

Equations

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

@[instance_reducible]

instance Krifka2020.instFintypeLayer : Fintype Layer

Equations

• Krifka2020.instFintypeLayer = { elems := { val := ↑Krifka2020.Layer.enumList, nodup := Krifka2020.Layer.enumList_nodup }, complete := Krifka2020.instFintypeLayer._proof_1 }

def Krifka2020.instReprLayer.repr : Layer → ℕ → Std.Format

Equations

• Krifka2020.instReprLayer.repr Krifka2020.Layer.tp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2020.Layer.tp")).group prec✝
• Krifka2020.instReprLayer.repr Krifka2020.Layer.jp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2020.Layer.jp")).group prec✝
• Krifka2020.instReprLayer.repr Krifka2020.Layer.comP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2020.Layer.comP")).group prec✝
• Krifka2020.instReprLayer.repr Krifka2020.Layer.actP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2020.Layer.actP")).group prec✝

@[instance_reducible]

instance Krifka2020.instReprLayer : Repr Layer

Equations

• Krifka2020.instReprLayer = { reprPrec := Krifka2020.instReprLayer.repr }

def Krifka2020.Layer.rank : Layer → ℕ

The height of a layer.

Equations

• Krifka2020.Layer.tp.rank = 0
• Krifka2020.Layer.jp.rank = 1
• Krifka2020.Layer.comP.rank = 2
• Krifka2020.Layer.actP.rank = 3

@[instance_reducible]

instance Krifka2020.instLinearOrderLayer : LinearOrder Layer

Equations

• Krifka2020.instLinearOrderLayer = LinearOrder.lift' Krifka2020.Layer.rank Krifka2020.instLinearOrderLayer._proof_1

inductive Krifka2020.Modifier : Type

Modifiers of §3, with the layer they modify: subjective epistemics and evidentials the judgement, affirmatives the commitment, offen gesagt the act.

• sicherlich : Modifier
• wahrscheinlich : Modifier
• lautEva : Modifier
• echt : Modifier
• ungelogen : Modifier
• wirklich : Modifier
• ehrlich : Modifier
• offenGesagt : Modifier

@[instance_reducible]

instance Krifka2020.instDecidableEqModifier : DecidableEq Modifier

Equations

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

@[instance_reducible]

instance Krifka2020.instFintypeModifier : Fintype Modifier

Equations

• Krifka2020.instFintypeModifier = { elems := { val := ↑Krifka2020.Modifier.enumList, nodup := Krifka2020.Modifier.enumList_nodup }, complete := Krifka2020.instFintypeModifier._proof_1 }

@[instance_reducible]

instance Krifka2020.instReprModifier : Repr Modifier

Equations

• Krifka2020.instReprModifier = { reprPrec := Krifka2020.instReprModifier.repr }

def Krifka2020.instReprModifier.repr : Modifier → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2020.instReprModifier.repr Krifka2020.Modifier.echt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2020.Modifier.echt")).group prec✝

def Krifka2020.Modifier.layer : Modifier → Layer

Equations

• Krifka2020.Modifier.sicherlich.layer = Krifka2020.Layer.jp
• Krifka2020.Modifier.wahrscheinlich.layer = Krifka2020.Layer.jp
• Krifka2020.Modifier.lautEva.layer = Krifka2020.Layer.jp
• Krifka2020.Modifier.echt.layer = Krifka2020.Layer.comP
• Krifka2020.Modifier.ungelogen.layer = Krifka2020.Layer.comP
• Krifka2020.Modifier.wirklich.layer = Krifka2020.Layer.comP
• Krifka2020.Modifier.ehrlich.layer = Krifka2020.Layer.comP
• Krifka2020.Modifier.offenGesagt.layer = Krifka2020.Layer.actP

inductive Krifka2020.Predicate : Type

Clause-embedding predicates of §4.1 with the layer they select: a proposition (96), a judgement (101), a commitment (111), or an act (112).

• abhaengen : Predicate
• glauben : Predicate
• wissen : Predicate
• sagen : Predicate
• mitteilen : Predicate

@[instance_reducible]

instance Krifka2020.instDecidableEqPredicate : DecidableEq Predicate

Equations

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

@[instance_reducible]

instance Krifka2020.instReprPredicate : Repr Predicate

Equations

• Krifka2020.instReprPredicate = { reprPrec := Krifka2020.instReprPredicate.repr }

def Krifka2020.instReprPredicate.repr : Predicate → ℕ → Std.Format

Equations

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

def Krifka2020.Predicate.selects : Predicate → Layer

Equations

• Krifka2020.Predicate.abhaengen.selects = Krifka2020.Layer.tp
• Krifka2020.Predicate.glauben.selects = Krifka2020.Layer.jp
• Krifka2020.Predicate.wissen.selects = Krifka2020.Layer.jp
• Krifka2020.Predicate.sagen.selects = Krifka2020.Layer.comP
• Krifka2020.Predicate.mitteilen.selects = Krifka2020.Layer.actP

def Krifka2020.Licensed (m : Modifier) (p : Predicate) : Prop

A modifier occurs in a complement clause when the predicate selects its layer or a higher one.

Equations

• Krifka2020.Licensed m p = (m.layer ≤ p.selects)

@[instance_reducible]

instance Krifka2020.instDecidableLicensed (m : Modifier) (p : Predicate) : Decidable (Licensed m p)

Equations

• Krifka2020.instDecidableLicensed m p = { decide := m.layer.rank.ble p.selects.rank, reflects_decide := ⋯ }

theorem Krifka2020.licensed_iff : (∀ (m : Modifier), ¬Licensed m Predicate.abhaengen) ∧ (∀ (m : Modifier), Licensed m Predicate.glauben ↔ m.layer = Layer.jp) ∧ ∀ (m : Modifier), Licensed m Predicate.sagen ↔ m.layer ≠ Layer.actP

No modifier under abhängen (95); judgement modifiers but no affirmatives under glauben (100); both under sagen (110).