Documentation

Linglib.Theories.Dialogue.LayeredAssertion

Layered Assertive Clauses #

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

Four-layer decomposition of an assertive clause from @cite{krifka-2020}: TP (propositional content), JP (epistemic judgement), ComP (commitment strength), ActP (speech act type). JP terminology and the layered idea trace to @cite{speas-2004} and @cite{wiltschko-2014}; @cite{krifka-2020} synthesises them with the commitment-space framework.

LayerContributionExample Modifier
TPPropositional contenttense, aspect
JP (Judge Phrase)Epistemic judgment"I think", evidentials
ComP (Commitment Phrase)Commitment strength"I swear", "perhaps"
ActP (Act Phrase)Speech act typedeclarative, 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 Theories/Dialogue/CommitmentSpace.lean (the 2015 commitment-space framework). The two are independent — neither imports the other — and study files target whichever is appropriate:

source
inductive Dialogue.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
    @[implicit_reducible]
    instance Dialogue.Krifka.instDecidableEqCommitmentStrength :
    DecidableEq CommitmentStrength
    Equations
    source
    def Dialogue.Krifka.instReprCommitmentStrength.repr :
    CommitmentStrength → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Dialogue.Krifka.instReprCommitmentStrength :
      Repr CommitmentStrength
      Equations
      source
      @[implicit_reducible]
      instance Dialogue.Krifka.instInhabitedCommitmentStrength :
      Inhabited CommitmentStrength
      Equations
      source
      def Dialogue.Krifka.instInhabitedCommitmentStrength.default :
      CommitmentStrength
      Equations
      Instances For
        source
        def Dialogue.Krifka.CommitmentStrength.rank :
        CommitmentStrength → ℕ

        Numerical ordering of commitment strengths.

        Equations
        Instances For
          source
          theorem Dialogue.Krifka.standard_is_default :
          CommitmentStrength.standard.rank = 1

          Standard is the default.

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

          Strong > standard > weak.

          source
          structure Dialogue.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/IllocutionaryForce.lean.

          Instances For
            source
            inductive Dialogue.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).

            Instances For
              source
              @[implicit_reducible]
              instance Dialogue.Krifka.instDecidableEqUpdateType :
              DecidableEq UpdateType
              Equations
              source
              def Dialogue.Krifka.instReprUpdateType.repr :
              UpdateType → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                instance Dialogue.Krifka.instReprUpdateType :
                Repr UpdateType
                Equations
                source
                @[implicit_reducible]
                instance Dialogue.Krifka.instInhabitedUpdateType :
                Inhabited UpdateType
                Equations
                source
                def Dialogue.Krifka.instInhabitedUpdateType.default :
                UpdateType
                Equations
                Instances For
                  source
                  def Dialogue.Krifka.informativeUpdate {W : Type u_1} (cs : List W) (φ : W → Prop) [DecidablePred φ] :
                  List W

                  Informative update: restrict context set to worlds satisfying φ.

                  -- UNVERIFIED: @cite{krifka-2020} 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
                  Instances For
                    source
                    structure Dialogue.Krifka.TypedAssertion (W : Type u_1) extends Dialogue.Krifka.LayeredAssertion W :
                    Type u_1

                    A fully specified assertion with update type.

                    Instances For
                      source
                      theorem Dialogue.Krifka.default_assertion_informative {W : Type u_1} (p : Set W) :
                      { content := p }.updateType = UpdateType.informative

                      Default assertions are informative (the common case).