@cite{izvorski-1997}: The Present Perfect as an Epistemic Modal — Data @cite{izvorski-1997}

Empirical data from @cite{izvorski-1997}. In Bulgarian, Turkish, Norwegian, and other languages, present perfect morphology doubles as an indirect evidential (the "Perfect of Evidentiality" = PE). The paper's central proposal (8):

The indirect evidential Event is an epistemic modal which: (i) has universal quantificational force, (ii) has a presupposition that the evidence for the core proposition is indirect.

The key empirical contrasts establishing (8):

1. Event vs. must ((10)–(13)): Both are epistemic necessity modals (same □ force), but Event restricts the modal base to indirect evidence only. Must allows any epistemic base. The difference is in the base, not the force.
2. Presupposition diagnostics ((14)–(16)): The indirect-evidence requirement is a presupposition (not an implicature) — it resists cancellation (14), projects past negation (15), and denial targets the assertion (16).

inductive Phenomena.TenseAspect.Studies.Izvorski1997.Data.PELanguage : Type

Languages exhibiting the Perfect of Evidentiality (@cite{izvorski-1997}, fn. 1). The paper's body text discusses Bulgarian, Turkish, and Norwegian; footnote 1 lists ~25 languages across 6 families.

• bulgarian : PELanguage
• turkish : PELanguage
• norwegian : PELanguage
• macedonian : PELanguage
• albanian : PELanguage

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqPELanguage : DecidableEq PELanguage

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqPELanguage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPELanguage : Repr PELanguage

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPELanguage = { reprPrec := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPELanguage.repr }

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPELanguage.repr : PELanguage → ℕ → Std.Format

Equations

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

inductive Phenomena.TenseAspect.Studies.Izvorski1997.Data.EvidenceBasis : Type

Binary evidence basis: Izvorski's central contrast variable. The paper argues that Event and must have the same quantificational force (□) but differ in whether the modal base is restricted to indirect evidence only.

• direct : EvidenceBasis
• indirect : EvidenceBasis

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqEvidenceBasis : DecidableEq EvidenceBasis

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqEvidenceBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvidenceBasis : Repr EvidenceBasis

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvidenceBasis = { reprPrec := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvidenceBasis.repr }

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvidenceBasis.repr : EvidenceBasis → ℕ → Std.Format

Equations

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

structure Phenomena.TenseAspect.Studies.Izvorski1997.Data.EvMustDatum : Type

A data point from the Event/must paradigm. The paper's argument (§3, pp. 227–229):

• (10)–(11): With indirect evidence, both Event and must are felicitous
• (12)–(13): Event + "I have no evidence" → contradictory; must + "I have no evidence" → acceptable (must doesn't presuppose indirect evidence)
• Prose (p. 228): With direct evidence (speaker witnessed the event), Event is infelicitous; must is fine

• evidenceBasis : EvidenceBasis
• evFelicitous : Bool
• mustFelicitous : Bool
• label : String

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvMustDatum.repr : EvMustDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvMustDatum : Repr EvMustDatum

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvMustDatum = { reprPrec := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprEvMustDatum.repr }

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvMustDatum : BEq EvMustDatum

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvMustDatum = { beq := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvMustDatum.beq }

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvMustDatum.beq : EvMustDatum → EvMustDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvMustDatum.beq x✝¹ x✝ = false

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMust_indirect : EvMustDatum

Indirect evidence context: both Event and must felicitous. Paper (10)–(11): "Knowing how much John likes wine..."

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMust_direct : EvMustDatum

Direct evidence context: Event infelicitous, must fine. Paper prose (p. 228): when speaker has direct evidence (witnessed the event), PE is infelicitous but must is acceptable.

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMustData : List EvMustDatum

All Event/must data points.

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMustData = [Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMust_indirect, Phenomena.TenseAspect.Studies.Izvorski1997.Data.evMust_direct]

inductive Phenomena.TenseAspect.Studies.Izvorski1997.Data.PresupDiagnostic : Type

Standard presupposition diagnostics applied to the evidential.

• cancellation : PresupDiagnostic
• projection : PresupDiagnostic
• denial : PresupDiagnostic

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqPresupDiagnostic : DecidableEq PresupDiagnostic

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidableEqPresupDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnostic.repr : PresupDiagnostic → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnostic : Repr PresupDiagnostic

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnostic = { reprPrec := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnostic.repr }

structure Phenomena.TenseAspect.Studies.Izvorski1997.Data.PresupDiagnosticDatum : Type

A presupposition diagnostic datum.

• diagnostic : PresupDiagnostic
• evidentialSurvives : Bool
• label : String

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnosticDatum.repr : PresupDiagnosticDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnosticDatum : Repr PresupDiagnosticDatum

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnosticDatum = { reprPrec := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instReprPresupDiagnosticDatum.repr }

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnosticDatum.beq : PresupDiagnosticDatum → PresupDiagnosticDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnosticDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnosticDatum : BEq PresupDiagnosticDatum

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnosticDatum = { beq := Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnosticDatum.beq }

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.presup_cancellation : PresupDiagnosticDatum

(14): Cancellation fails — "Maria apparently kissed Ivan. # I witnessed it." The indirect-evidence requirement cannot be cancelled, so it is a presupposition, not an implicature.

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.presup_projection : PresupDiagnosticDatum

(15): Projection under negation — "Apparently, Ivan didn't pass the exam." The indirect-evidence requirement projects past negation: the speaker still has indirect evidence; what's negated is that Ivan passed.

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.presup_denial : PresupDiagnosticDatum

(16): Denial targets assertion — "Ivan passed-PE the exam. That's not true." The denial targets p (Ivan passed), not the evidential content (that the speaker has indirect evidence).

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.presupData : List PresupDiagnosticDatum

All presupposition diagnostic data.

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evRequiresIndirect (d : EvMustDatum) : Bool

Event requires indirect evidence: felicitous with indirect, infelicitous with direct. This captures (8ii).

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.mustAllowsBoth (d : EvMustDatum) : Bool

Must allows both evidence bases — no presupposition on evidence type.

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.mustAllowsBoth d = d.mustFelicitous

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.all_evRequiresIndirect : evMustData.all evRequiresIndirect = true

All data points satisfy the indirect-evidence generalization.

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.all_mustAllowsBoth : evMustData.all mustAllowsBoth = true

All data points satisfy the must-allows-both generalization.

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.all_evidentialSurvives : (presupData.all fun (x : PresupDiagnosticDatum) => x.evidentialSurvives) = true

All diagnostics confirm presupposition status (not implicature).

@[reducible, inline]

abbrev Phenomena.TenseAspect.Studies.Izvorski1997.Data.World : Type

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.World = Fin 4

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.allWorlds : List World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.allWorlds = [0, 1, 2, 3]

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorskiEv (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) : Core.Presupposition.PrProp World

Izvorski's EV operator (formalization of (17)–(19) + (8ii)).

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank : World → Prop

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank 0 = True
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank 1 = True
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank 2 = False
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank 3 = False

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank : DecidablePred johnDrank

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank 0 = isTrue Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank._proof_1
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank 1 = isTrue Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank._proof_2
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank 2 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank._proof_3
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank 3 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldJohnDrank._proof_4

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty : World → Prop

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty 0 = True
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty 1 = False
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty 2 = True
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty 3 = False

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty : DecidablePred bottlesEmpty

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty 0 = isTrue Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty._proof_1
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty 1 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty._proof_2
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty 2 = isTrue Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty._proof_3
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty 3 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldBottlesEmpty._proof_4

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evBase : Core.Logic.Intensional.ModalBase World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.evBase x✝ = [Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty]

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.mustBase : Core.Logic.Intensional.ModalBase World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.mustBase x✝ = [Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty, Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank]

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.beliefOrdering : Core.Logic.Intensional.OrderingSource World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.beliefOrdering x✝ = [Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank]

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.ev_presup_satisfied (w : World) : (izvorskiEv evBase beliefOrdering johnDrank).presup w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.must_accessible_subset_ev (w w' : World) (hw' : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds mustBase w) : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds evBase w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.restricted_base_enlarges_access (f_ev f_must : Core.Logic.Intensional.ModalBase World) (h : ∀ (w : World), ∀ p ∈ f_ev w, p ∈ f_must w) (w w' : World) (hw' : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f_must w) : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f_ev w

@[implicit_reducible]

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0 : DecidablePred Phenomena.TenseAspect.Studies.Izvorski1997.Data.pOnlyW0✝

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0 0 = isTrue Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0._proof_1
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0 1 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0._proof_2
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0 2 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0._proof_3
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0 3 = isFalse Phenomena.TenseAspect.Studies.Izvorski1997.Data.instDecidablePredWorldPOnlyW0._proof_4

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_koev_diverge : ∃ (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World), ¬(izvorskiEv f g p).assertion w ∧ p w

The izvorski operator can diverge from the bare prejacent: at w0, pOnlyW0 w0 = True, but the necessity claim is False (since w1, w2, w3 are also accessible under universal access and don't satisfy pOnlyW0).

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_collapses_to_koev_when_realistic (f : Core.Logic.Intensional.ModalBase World) (p : World → Prop) (w : World) (hTotal : Semantics.Modality.Kratzer.accessibleWorlds f w = {w}) : (izvorskiEv f Core.Logic.Intensional.emptyBackground p).assertion w ↔ p w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_projection (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) : (izvorskiEv f g p).neg.presup = (izvorskiEv f g p).presup

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.nfutL_compatible_with_izvorski : Fragments.Slavic.Bulgarian.Evidentials.nfutL.ep = Semantics.Tense.Evidential.EPCondition.downstream