Temporal since

import Linglib.Semantics.Tense.Since · namespace Tense

This file defines Iatridou's temporal since, in the form von Fintel gives it: it has been five years since p presupposes that p held at the time five years before the evaluation time and asserts that it has not held since. It is Strawson anti-additive in p, but not classically downward entailing, since its presupposition can fail at a stronger argument, and not Strawson upward entailing.

References

von Fintel 1999, NPI Licensing, Strawson Entailment, and Context Dependency formalized

Declarations

L31–35

theorem isStrawsonAntiAdditive_since L37–40

{T : Type u_1} [LinearOrder T] (ago : T → T) :

Presupposition.IsStrawsonAntiAdditive (since ago)

Built from

L42–43

theorem not_antitone_posSupport_since L45–48

¬Antitone fun (p : Set ℤ) => posSupport (since (fun (x : ℤ) => x - 5) p)

Built from

It's been five years since I saw an eagle does not Strawson-entail it's been five years since I saw a bird, defined and false when a sparrow was seen since.

theorem not_isStrawsonUE_since L50–55

¬Presupposition.IsStrawsonUE (since fun (x : ℤ) => x - 5)

Built from