[Izv97]: The Present Perfect as an Epistemic Modal — Data [Izv97]

Empirical data from [Izv97]. 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 Izvorski1997.PELanguage : Type

Languages exhibiting the Perfect of Evidentiality ([Izv97], 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 Izvorski1997.instDecidableEqPELanguage : DecidableEq PELanguage

Equations

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

def Izvorski1997.instReprPELanguage.repr : PELanguage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Izvorski1997.instReprPELanguage : Repr PELanguage

Equations

• Izvorski1997.instReprPELanguage = { reprPrec := Izvorski1997.instReprPELanguage.repr }

inductive Izvorski1997.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 Izvorski1997.instDecidableEqEvidenceBasis : DecidableEq EvidenceBasis

Equations

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

def Izvorski1997.instReprEvidenceBasis.repr : EvidenceBasis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Izvorski1997.instReprEvidenceBasis : Repr EvidenceBasis

Equations

• Izvorski1997.instReprEvidenceBasis = { reprPrec := Izvorski1997.instReprEvidenceBasis.repr }

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

@[implicit_reducible]

instance Izvorski1997.instReprEvMustDatum : Repr EvMustDatum

Equations

• Izvorski1997.instReprEvMustDatum = { reprPrec := Izvorski1997.instReprEvMustDatum.repr }

def Izvorski1997.instReprEvMustDatum.repr : EvMustDatum → ℕ → Std.Format

Equations

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

def Izvorski1997.instBEqEvMustDatum.beq : EvMustDatum → EvMustDatum → Bool

Equations

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

@[implicit_reducible]

instance Izvorski1997.instBEqEvMustDatum : BEq EvMustDatum

Equations

• Izvorski1997.instBEqEvMustDatum = { beq := Izvorski1997.instBEqEvMustDatum.beq }

def Izvorski1997.evMust_indirect : EvMustDatum

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

Equations

• Izvorski1997.evMust_indirect = { evidenceBasis := Izvorski1997.EvidenceBasis.indirect, evFelicitous := true, mustFelicitous := true, label := "(10)–(11): indirect evidence context" }

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

• Izvorski1997.evMust_direct = { evidenceBasis := Izvorski1997.EvidenceBasis.direct, evFelicitous := false, mustFelicitous := true, label := "prose p.228: direct evidence context" }

def Izvorski1997.evMustData : List EvMustDatum

All Event/must data points.

Equations

• Izvorski1997.evMustData = [Izvorski1997.evMust_indirect, Izvorski1997.evMust_direct]

inductive Izvorski1997.PresupDiagnostic : Type

Standard presupposition diagnostics applied to the evidential.

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

@[implicit_reducible]

instance Izvorski1997.instDecidableEqPresupDiagnostic : DecidableEq PresupDiagnostic

Equations

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

@[implicit_reducible]

instance Izvorski1997.instReprPresupDiagnostic : Repr PresupDiagnostic

Equations

• Izvorski1997.instReprPresupDiagnostic = { reprPrec := Izvorski1997.instReprPresupDiagnostic.repr }

def Izvorski1997.instReprPresupDiagnostic.repr : PresupDiagnostic → ℕ → Std.Format

Equations

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

structure Izvorski1997.PresupDiagnosticDatum : Type

A presupposition diagnostic datum.

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

def Izvorski1997.instReprPresupDiagnosticDatum.repr : PresupDiagnosticDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Izvorski1997.instReprPresupDiagnosticDatum : Repr PresupDiagnosticDatum

Equations

• Izvorski1997.instReprPresupDiagnosticDatum = { reprPrec := Izvorski1997.instReprPresupDiagnosticDatum.repr }

def Izvorski1997.instBEqPresupDiagnosticDatum.beq : PresupDiagnosticDatum → PresupDiagnosticDatum → Bool

Equations

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

@[implicit_reducible]

instance Izvorski1997.instBEqPresupDiagnosticDatum : BEq PresupDiagnosticDatum

Equations

• Izvorski1997.instBEqPresupDiagnosticDatum = { beq := Izvorski1997.instBEqPresupDiagnosticDatum.beq }

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

• Izvorski1997.presup_cancellation = { diagnostic := Izvorski1997.PresupDiagnostic.cancellation, evidentialSurvives := true, label := "(14): Event + 'I witnessed it' → contradictory" }

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

• Izvorski1997.presup_projection = { diagnostic := Izvorski1997.PresupDiagnostic.projection, evidentialSurvives := true, label := "(15): not-Event-p still presupposes indirect evidence" }

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

• Izvorski1997.presup_denial = { diagnostic := Izvorski1997.PresupDiagnostic.denial, evidentialSurvives := true, label := "(16): denial targets p, not evidence" }

def Izvorski1997.presupData : List PresupDiagnosticDatum

All presupposition diagnostic data.

Equations

• Izvorski1997.presupData = [Izvorski1997.presup_cancellation, Izvorski1997.presup_projection, Izvorski1997.presup_denial]

def Izvorski1997.evRequiresIndirect (d : EvMustDatum) : Bool

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

Equations

• Izvorski1997.evRequiresIndirect d = match d.evidenceBasis with | Izvorski1997.EvidenceBasis.indirect => d.evFelicitous | Izvorski1997.EvidenceBasis.direct => !d.evFelicitous

def Izvorski1997.mustAllowsBoth (d : EvMustDatum) : Bool

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

Equations

• Izvorski1997.mustAllowsBoth d = d.mustFelicitous

theorem Izvorski1997.all_evRequiresIndirect : evMustData.all evRequiresIndirect = true

All data points satisfy the indirect-evidence generalization.

theorem Izvorski1997.all_mustAllowsBoth : evMustData.all mustAllowsBoth = true

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

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

All diagnostics confirm presupposition status (not implicature).

@[reducible, inline]

abbrev Izvorski1997.World : Type

Equations

• Izvorski1997.World = Fin 4

def Izvorski1997.allWorlds : List World

Equations

• Izvorski1997.allWorlds = [0, 1, 2, 3]

def Izvorski1997.izvorskiEv (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) : Semantics.Presupposition.PartialProp World

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

Equations

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

def Izvorski1997.johnDrank : World → Prop

Equations

• Izvorski1997.johnDrank 0 = True
• Izvorski1997.johnDrank 1 = True
• Izvorski1997.johnDrank 2 = False
• Izvorski1997.johnDrank 3 = False

@[implicit_reducible]

instance Izvorski1997.instDecidablePredWorldJohnDrank : DecidablePred johnDrank

Equations

• Izvorski1997.instDecidablePredWorldJohnDrank 0 = isTrue Izvorski1997.instDecidablePredWorldJohnDrank._proof_1
• Izvorski1997.instDecidablePredWorldJohnDrank 1 = isTrue Izvorski1997.instDecidablePredWorldJohnDrank._proof_2
• Izvorski1997.instDecidablePredWorldJohnDrank 2 = isFalse Izvorski1997.instDecidablePredWorldJohnDrank._proof_3
• Izvorski1997.instDecidablePredWorldJohnDrank 3 = isFalse Izvorski1997.instDecidablePredWorldJohnDrank._proof_4

def Izvorski1997.bottlesEmpty : World → Prop

Equations

• Izvorski1997.bottlesEmpty 0 = True
• Izvorski1997.bottlesEmpty 1 = False
• Izvorski1997.bottlesEmpty 2 = True
• Izvorski1997.bottlesEmpty 3 = False

@[implicit_reducible]

instance Izvorski1997.instDecidablePredWorldBottlesEmpty : DecidablePred bottlesEmpty

Equations

• Izvorski1997.instDecidablePredWorldBottlesEmpty 0 = isTrue Izvorski1997.instDecidablePredWorldBottlesEmpty._proof_1
• Izvorski1997.instDecidablePredWorldBottlesEmpty 1 = isFalse Izvorski1997.instDecidablePredWorldBottlesEmpty._proof_2
• Izvorski1997.instDecidablePredWorldBottlesEmpty 2 = isTrue Izvorski1997.instDecidablePredWorldBottlesEmpty._proof_3
• Izvorski1997.instDecidablePredWorldBottlesEmpty 3 = isFalse Izvorski1997.instDecidablePredWorldBottlesEmpty._proof_4

def Izvorski1997.evBase : Semantics.Modality.Kratzer.ModalBase World

Equations

• Izvorski1997.evBase x✝ = [Izvorski1997.bottlesEmpty]

def Izvorski1997.mustBase : Semantics.Modality.Kratzer.ModalBase World

Equations

• Izvorski1997.mustBase x✝ = [Izvorski1997.bottlesEmpty, Izvorski1997.johnDrank]

def Izvorski1997.beliefOrdering : Semantics.Modality.Kratzer.OrderingSource World

Equations

• Izvorski1997.beliefOrdering x✝ = [Izvorski1997.johnDrank]

theorem Izvorski1997.ev_presup_satisfied (w : World) : (izvorskiEv evBase beliefOrdering johnDrank).presup w

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

theorem Izvorski1997.restricted_base_enlarges_access (f_ev f_must : Semantics.Modality.Kratzer.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 Izvorski1997.instDecidablePredWorldPOnlyW0 : DecidablePred Izvorski1997.pOnlyW0✝

Equations

• Izvorski1997.instDecidablePredWorldPOnlyW0 0 = isTrue Izvorski1997.instDecidablePredWorldPOnlyW0._proof_1
• Izvorski1997.instDecidablePredWorldPOnlyW0 1 = isFalse Izvorski1997.instDecidablePredWorldPOnlyW0._proof_2
• Izvorski1997.instDecidablePredWorldPOnlyW0 2 = isFalse Izvorski1997.instDecidablePredWorldPOnlyW0._proof_3
• Izvorski1997.instDecidablePredWorldPOnlyW0 3 = isFalse Izvorski1997.instDecidablePredWorldPOnlyW0._proof_4

theorem Izvorski1997.izvorski_koev_diverge : ∃ (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.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 Izvorski1997.izvorski_collapses_to_koev_when_realistic (f : Semantics.Modality.Kratzer.ModalBase World) (p : World → Prop) (w : World) (hTotal : Semantics.Modality.Kratzer.accessibleWorlds f w = {w}) : (izvorskiEv f Semantics.Modality.Kratzer.emptyBackground p).assertion w ↔ p w

theorem Izvorski1997.izvorski_projection (f : Semantics.Modality.Kratzer.ModalBase World) (g : Semantics.Modality.Kratzer.OrderingSource World) (p : World → Prop) : (izvorskiEv f g p).neg.presup = (izvorskiEv f g p).presup

theorem Izvorski1997.nfutL_compatible_with_izvorski : Bulgarian.Evidentials.nfutL.ep = Tense.Evidential.EPCondition.downstream