Izvorski (1997): The Present Perfect as an Epistemic Modal

This file formalizes the analysis by Izvorski of the perfect of evidentiality, the indirect evidential that present perfect morphology expresses in Bulgarian, Turkish, Norwegian and other languages, (1). The evidential is an epistemic modal, (8): it asserts that the proposition holds in every accessible world closest to the speaker's beliefs about the evidence, in the possible-worlds semantics of Kratzer with a modal base of indirect evidence and an ordering source of beliefs about it, (17) to (19), and it presupposes that the speaker has indirect evidence for the proposition, evidence that exists and does not establish it (Ev). Epistemic must has the same force and no such presupposition (must), which is why an avowal of having no evidence, (12) and (13), or of having witnessed the event, (14), is consistent with must and not with the evidential; the presupposition projects through negation, (15), so that a denial targets the proposition, (16). The variability between the report and inference readings comes from the ordering source (necessity_of_beliefs), and the evidential does not entail its prejacent, as must does not, (9). Section 5 derives the presupposition from the present perfect: the consequent state of the event is known at speech time, giving the evidence, and the event itself is not, giving its indirectness (ev_ne_zero_of_perfect), and the domain of quantification lies within the epistemically accessible worlds, so that unlike the counterfactual inference of the past the evidential meaning is no implicature (bestWorlds_subset_accessible).

Implementation notes

• The presupposition "speaker has indirect evidence for p" is rendered as a nonempty evidence background whose worlds do not all verify p; the report and inference readings are not distinguished in the operator, as the paper intends.
• Section 4's temporal and aspectual diagnostics, (20) to (24), are recorded as rows; the evidential takes the temporal interpretation of the indicative, which the operator does not represent.

References

• R. Izvorski, The Present Perfect as an Epistemic Modal (1997)
• A. Kratzer, Modality (1991)

def Izvorski1997.Known {W : Type u_1} (f : Modality.Background W) (w : W) (p : W → Prop) : Prop

The speaker knows p relative to the background f when p holds throughout the worlds compatible with it.

Equations

• Izvorski1997.Known f w p = ∀ u ∈ f.accessibleWorlds w, p u

noncomputable def Izvorski1997.Ev {W : Type u_1} (f g : Modality.Background W) (p : W → Prop) : W → SignType

The indirect evidential of (8) and (17) to (19). The background f assigns each world the propositions the speaker counts as indirect evidence, and g assigns the speaker's beliefs about that evidence. The presupposition is that there is such evidence and that it does not establish p, and the assertion is that p holds in every accessible world closest to the beliefs.

Equations

• Izvorski1997.Ev f g p = {w : W | (f w).Nonempty ∧ ¬Izvorski1997.Known f w p}.indicator fun (w : W) => SignType.ofProp (Modality.necessity f g p w)

noncomputable def Izvorski1997.must {W : Type u_1} (f g : Modality.Background W) (p : W → Prop) : W → SignType

Epistemic must is the same necessity over what is known, with no presupposition about the kind of evidence.

Equations

• Izvorski1997.must f g p w = SignType.ofProp (Modality.necessity f g p w)

theorem Izvorski1997.ev_eq_must_of_ne_zero {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} {w : W} (h : Ev f g p w ≠ 0) : Ev f g p w = must f g p w

The evidential and must assert the same universal claim (8a), so wherever the evidential is defined it has the value of must.

theorem Izvorski1997.accessible_must_subset {W : Type u_1} {f f' : Modality.Background W} {w : W} (h : f w ⊆ f' w) : f'.accessibleWorlds w ⊆ f.accessibleWorlds w

must quantifies over what is known, a background at least as rich as the indirect evidence, so its accessible worlds are among the evidential's, (10) and (11).

theorem Izvorski1997.ev_eq_zero_of_no_evidence {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} {w : W} (h : f w = ∅) : Ev f g p w = 0

With no evidence the evidential is undefined where must is not, as in (12) and (13).

theorem Izvorski1997.ev_eq_zero_of_known {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} {w : W} (h : Known f w p) : Ev f g p w = 0

Evidence establishing p, as witnessing it does, is not indirect (14).

theorem Izvorski1997.support_neg_ev {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} : Function.support (-Ev f g p) = Function.support (Ev f g p)

The presupposition projects through negation, so negating or denying an evidential statement targets the proposition and not the evidence, as in (15) and (16).

theorem Izvorski1997.necessity_of_beliefs {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} {w : W} (hex : ∃ u ∈ f.accessibleWorlds w, ∀ q ∈ g w, q u) (h : ∀ u ∈ f.accessibleWorlds w, (∀ q ∈ g w, q u) → p u) : Modality.necessity f g p w

The force of the evidential is set by the beliefs about the evidence. When some accessible world verifies every belief and all such worlds verify p, the assertion holds. A reliable report or a sound inference makes the reading close to universal, and an unreliable source leaves it weak.

theorem Izvorski1997.bestWorlds_subset_accessible {W : Type u_1} {f g : Modality.Background W} {w : W} : Modality.bestWorlds f g w ⊆ f.accessibleWorlds w

The domain of quantification lies within the epistemically accessible worlds, where the counterfactual's lies outside them, so the evidential meaning is asserted of the actual epistemic state and is no implicature (Section 5.3).

theorem Izvorski1997.ev_ne_zero_of_perfect {W : Type u_1} {f g : Modality.Background W} {p : W → Prop} {w : W} {p' : W → Prop} (hp' : p' ∈ f w) (hnot : ¬Known f w p) : Ev f g p w ≠ 0

The present perfect supplies the presupposition (Section 5.2). The consequent state of the event holding at speech time is a proposition the speaker knows, the indirect evidence, and the event not holding at speech time is p not being known.

theorem Izvorski1997.ev_not_entails : ∃ (f : Modality.Background (Fin 2)) (g : Modality.Background (Fin 2)) (p : Fin 2 → Prop) (w : Fin 2), Ev f g p w = 1 ∧ ¬p w

Like must, the evidential does not entail its prejacent (9). In a two-world model the evidence excludes nothing, the speaker's beliefs single out the world where p holds, and the evidential is defined and true at the other world.