Documentation

Linglib.Semantics.Epistemicity

Epistemic Profile Layer #

[Flo18] [GS24] [Tou08]

Connective layer bundling evidential source, epistemic authority (egophoricity), and mirativity into a unified EpistemicProfile. Bridges these feature-geometric dimensions to the model-theoretic level (KContext / ContextTower).

Motivation #

[GS24] identify 10 concept areas forming a coherent epistemic domain. Linglib already covers evidential source (Features/Evidentiality.lean), epistemic modality (Modality/Kernel.lean), and mirativity (Features/Mirativity.lean), but these are scattered with no connective tissue. The main gap is egophoricity -- the dimension of WHO has privileged epistemic access (speaker vs addressee vs third party), which the glossary argues is independent of evidential source.

Design #

EpistemicAuthority fills the egophoricity gap. EpistemicProfile bundles it with CoarseSource and MirativityValue for unified epistemic specification. epistemicAuthority bridges epistemic authority to ContextTower by resolving from the origin (speech-act context), since egophoric marking reflects the actual speech-act participants, not reported ones.

Not Yet Formalized #

Engagement, logophoricity, and epistemic vigilance would require substantial new infrastructure (discourse model, binding theory extension, RSA listener model extension respectively) and are left for future work.

source
inductive Semantics.Epistemicity.EpistemicAuthority :
Type

Epistemic authority: WHO has privileged access to the propositional content. Egophoric systems ([Tou08], [Flo18], Gawne & Spronck glossary 2) grammaticalize the distinction between:

  • ego: speaker has privileged access (1st person knowledge, volition, intention)
  • allocutive: addressee has privileged access (2nd person questions)
  • nonparticipant: neither speech-act participant has special access
Instances For
    source
    @[implicit_reducible]
    instance Semantics.Epistemicity.instDecidableEqEpistemicAuthority :
    DecidableEq EpistemicAuthority
    Equations
    source
    def Semantics.Epistemicity.instReprEpistemicAuthority.repr :
    EpistemicAuthority → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Epistemicity.instReprEpistemicAuthority :
      Repr EpistemicAuthority
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Epistemicity.instInhabitedEpistemicAuthority :
      Inhabited EpistemicAuthority
      Equations
      source
      structure Semantics.Epistemicity.EpistemicProfile :
      Type

      Epistemic profile: bundles the three orthogonal epistemic dimensions that the glossary identifies as cross-linguistically relevant.

      • source: WHAT kind of evidence (Aikhenvald's 3-way)
      • authority: WHO has privileged access (egophoric dimension)
      • mirativity: WHETHER the content is expected (DeLancey's dimension)
      Instances For
        source
        def Semantics.Epistemicity.instReprEpistemicProfile.repr :
        EpistemicProfile → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Semantics.Epistemicity.instReprEpistemicProfile :
          Repr EpistemicProfile
          Equations
          source
          @[implicit_reducible]
          instance Semantics.Epistemicity.instBEqEpistemicProfile :
          BEq EpistemicProfile
          Equations
          source
          def Semantics.Epistemicity.instBEqEpistemicProfile.beq :
          EpistemicProfile → EpistemicProfile → Bool
          Equations
          Instances For
            source
            def Semantics.Epistemicity.epistemicAuthority {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [DecidableEq E] (tower : Context.ContextTower (Context.KContext W E P T)) (knower : E) :
            EpistemicAuthority

            Determine epistemic authority from a ContextTower, resolving from the origin (speech-act context). Egophoric marking reflects the actual speech-act participants: ego if the knower is the speaker, allocutive if the knower is the addressee, nonparticipant otherwise.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Semantics.Epistemicity.strongAssertion :
              EpistemicProfile

              Ego authority with direct evidence: the canonical "strong assertion" profile. The speaker saw it themselves -- maximally authoritative.

              Equations
              Instances For
                source
                def Semantics.Epistemicity.inferentialClaim :
                EpistemicProfile

                Non-ego authority with inferential evidence: the canonical profile for epistemic 'must' ([vFG10]). Speaker infers, no privileged access.

                Equations
                Instances For
                  source
                  theorem Semantics.Epistemicity.ego_default_direct :
                  strongAssertion.source = Features.Evidentiality.CoarseSource.direct

                  In ego-authority contexts, direct evidence is the default source. This captures the generalization that 1st-person volitional claims ("I'm going to leave") use ego marking, not evidential marking.

                  source
                  def Semantics.Epistemicity.allocutiveProfile (s : Features.Evidentiality.CoarseSource) :
                  EpistemicProfile

                  In allocutive contexts, evidential source is typically irrelevant -- the addressee's authority overrides source distinctions. (Tibetan -payin ego vs -pa'dug non-ego; Akhvakh -eri ego vs -ari non-ego)

                  Equations
                  Instances For
                    source
                    theorem Semantics.Epistemicity.epistemicAuthority_shift_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [DecidableEq E] (tower : Context.ContextTower (Context.KContext W E P T)) (σ : Context.ContextShift (Context.KContext W E P T)) (knower : E) :
                    epistemicAuthority (tower.push σ) knower = epistemicAuthority tower knower

                    Epistemic authority is invariant under tower push: egophoric marking reflects speech-act participants (from origin), not embedded ones.