@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 Ev 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. Ev vs. must ((10)–(13)): Both are epistemic necessity modals (same □ force), but Ev 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

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 ⋯

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.

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPELanguage : BEq PELanguage

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPELanguage.beq : PELanguage → PELanguage → Bool

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPELanguage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

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

• direct : EvidenceBasis
• indirect : EvidenceBasis

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 ⋯

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.

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvidenceBasis.beq : EvidenceBasis → EvidenceBasis → Bool

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvidenceBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqEvidenceBasis : BEq EvidenceBasis

Equations

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

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

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

• (10)–(11): With indirect evidence, both Ev and must are felicitous
• (12)–(13): Ev + "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), Ev 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.

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

Equations

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

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 Ev 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: Ev 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 Ev/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

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 ⋯

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

Equations

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

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

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnostic.beq : PresupDiagnostic → PresupDiagnostic → Bool

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TenseAspect.Studies.Izvorski1997.Data.instBEqPresupDiagnostic : BEq PresupDiagnostic

Equations

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

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

A presupposition diagnostic datum.

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

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.instReprPresupDiagnosticDatum.repr : PresupDiagnosticDatum → ℕ → Std.Format

Equations

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

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

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

Ev 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).

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorskiEv (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) : Core.Presupposition.PrProp Semantics.Attitudes.Intensional.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 : BProp Semantics.Attitudes.Intensional.World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank Core.Proposition.World4.w0 = true
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank Core.Proposition.World4.w1 = true
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank Core.Proposition.World4.w2 = false
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.johnDrank Core.Proposition.World4.w3 = false

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty : BProp Semantics.Attitudes.Intensional.World

Equations

• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty Core.Proposition.World4.w0 = true
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty Core.Proposition.World4.w1 = false
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty Core.Proposition.World4.w2 = true
• Phenomena.TenseAspect.Studies.Izvorski1997.Data.bottlesEmpty Core.Proposition.World4.w3 = false

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.evBase : Semantics.Modality.Kratzer.ModalBase

Equations

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

def Phenomena.TenseAspect.Studies.Izvorski1997.Data.mustBase : Semantics.Modality.Kratzer.ModalBase

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 : Semantics.Modality.Kratzer.OrderingSource

Equations

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

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.ev_presup_satisfied (w : Semantics.Attitudes.Intensional.World) : (izvorskiEv evBase beliefOrdering johnDrank).presup w = true

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.ev_asserts_drank (w : Semantics.Attitudes.Intensional.World) : (izvorskiEv evBase beliefOrdering johnDrank).assertion w = true

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.must_accessible_subset_ev (w w' : Semantics.Attitudes.Intensional.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 : Semantics.Modality.Kratzer.ModalBase) (h : ∀ (w : Semantics.Attitudes.Intensional.World), ∀ p ∈ f_ev w, p ∈ f_must w) (w w' : Semantics.Attitudes.Intensional.World) (hw' : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f_must w) : w' ∈ Semantics.Modality.Kratzer.accessibleWorlds f_ev w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.ev_and_must_agree_here (w : Semantics.Attitudes.Intensional.World) : (izvorskiEv evBase beliefOrdering johnDrank).assertion w = Semantics.Modality.Kratzer.necessity mustBase beliefOrdering johnDrank w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_koev_diverge : ∃ (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World), (izvorskiEv f g p).assertion w ≠ p w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_collapses_to_koev_when_realistic (f : Semantics.Modality.Kratzer.ModalBase) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) (hTotal : Semantics.Modality.Kratzer.accessibleWorlds f w = [w]) : (izvorskiEv f Semantics.Modality.Kratzer.emptyBackground p).assertion w = p w

theorem Phenomena.TenseAspect.Studies.Izvorski1997.Data.izvorski_projection (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) : (izvorskiEv f g p).neg.presup = (izvorskiEv f g p).presup

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