Epistemic Profile Layer

@cite{floyd-2018} @cite{gawne-spronck-2024} @cite{tournadre-2008}

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

@cite{gawne-spronck-2024} identify 10 concept areas forming a coherent epistemic domain. Linglib already covers evidential source (Core/Evidence.lean), epistemic modality (Modality/Kernel.lean), and mirativity (Core/Evidence.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 EvidentialSource 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.

inductive Core.Epistemicity.EpistemicAuthority : Type

Epistemic authority: WHO has privileged access to the propositional content. Egophoric systems (@cite{tournadre-2008}, @cite{floyd-2018}, 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

• ego : EpistemicAuthority
• allocutive : EpistemicAuthority
• nonparticipant : EpistemicAuthority

instance Core.Epistemicity.instDecidableEqEpistemicAuthority : DecidableEq EpistemicAuthority

Equations

• Core.Epistemicity.instDecidableEqEpistemicAuthority x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Epistemicity.instReprEpistemicAuthority.repr : EpistemicAuthority → ℕ → Std.Format

Equations

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

instance Core.Epistemicity.instReprEpistemicAuthority : Repr EpistemicAuthority

Equations

• Core.Epistemicity.instReprEpistemicAuthority = { reprPrec := Core.Epistemicity.instReprEpistemicAuthority.repr }

instance Core.Epistemicity.instBEqEpistemicAuthority : BEq EpistemicAuthority

Equations

• Core.Epistemicity.instBEqEpistemicAuthority = { beq := Core.Epistemicity.instBEqEpistemicAuthority.beq }

def Core.Epistemicity.instBEqEpistemicAuthority.beq : EpistemicAuthority → EpistemicAuthority → Bool

Equations

• Core.Epistemicity.instBEqEpistemicAuthority.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Epistemicity.instInhabitedEpistemicAuthority.default : EpistemicAuthority

Equations

• Core.Epistemicity.instInhabitedEpistemicAuthority.default = Core.Epistemicity.EpistemicAuthority.ego

instance Core.Epistemicity.instInhabitedEpistemicAuthority : Inhabited EpistemicAuthority

Equations

• Core.Epistemicity.instInhabitedEpistemicAuthority = { default := Core.Epistemicity.instInhabitedEpistemicAuthority.default }

structure Core.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)

• source : Evidence.EvidentialSource
• authority : EpistemicAuthority
• mirativity : Evidence.MirativityValue

instance Core.Epistemicity.instReprEpistemicProfile : Repr EpistemicProfile

Equations

• Core.Epistemicity.instReprEpistemicProfile = { reprPrec := Core.Epistemicity.instReprEpistemicProfile.repr }

def Core.Epistemicity.instReprEpistemicProfile.repr : EpistemicProfile → ℕ → Std.Format

Equations

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

instance Core.Epistemicity.instBEqEpistemicProfile : BEq EpistemicProfile

Equations

• Core.Epistemicity.instBEqEpistemicProfile = { beq := Core.Epistemicity.instBEqEpistemicProfile.beq }

def Core.Epistemicity.instBEqEpistemicProfile.beq : EpistemicProfile → EpistemicProfile → Bool

Equations

• Core.Epistemicity.instBEqEpistemicProfile.beq { source := a, authority := a_1, mirativity := a_2 } { source := b, authority := b_1, mirativity := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.Epistemicity.instBEqEpistemicProfile.beq x✝¹ x✝ = false

def Core.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.

def Core.Epistemicity.strongAssertion : EpistemicProfile

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

Equations

• Core.Epistemicity.strongAssertion = { source := Core.Evidence.EvidentialSource.direct, authority := Core.Epistemicity.EpistemicAuthority.ego }

def Core.Epistemicity.inferentialClaim : EpistemicProfile

Non-ego authority with inferential evidence: the canonical profile for epistemic 'must' (@cite{von-fintel-gillies-2010}). Speaker infers, no privileged access.

Equations

• Core.Epistemicity.inferentialClaim = { source := Core.Evidence.EvidentialSource.inference, authority := Core.Epistemicity.EpistemicAuthority.nonparticipant }

theorem Core.Epistemicity.ego_default_direct : strongAssertion.source = Evidence.EvidentialSource.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.

def Core.Epistemicity.allocutiveProfile (s : Evidence.EvidentialSource) : 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

• Core.Epistemicity.allocutiveProfile s = { source := s, authority := Core.Epistemicity.EpistemicAuthority.allocutive }

theorem Core.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.