Documentation

Linglib.Theories.Semantics.Tense.TemporalConnectives.OST

@cite{ogihara-steinert-threlkeld-2024}: Event-Level Temporal Connectives #

@cite{ogihara-steinert-threlkeld-2024}

An interval-based semantics for before and after that operates at Level 3 (event predicates), replacing point-level (Anscombe) and interval-set-level (Rett) approaches with direct quantification over events and their runtime intervals.

Core Insight: Quantificational Asymmetry #

before and after differ in quantificational force over the complement:

This asymmetry derives the veridicality contrast: after entails its complement (∃e₂ asserts Q happened); before doesn't (∀e₂ is vacuously true when no Q-event exists).

Level #

Level 3 (event predicates): operates on EvPred Time. Projects to Level 2 via eventDenotation (EventBridge.lean).

Cross-Level Comparison #

OST.after P Q → Anscombe.after (eventDenotation P) (eventDenotation Q) but the converse fails: Anscombe allows partial overlap of runtimes, while O&ST requires entire-runtime precedence (τ-precedence).

source
def Semantics.Tense.TemporalConnectives.OST.after {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
Prop

O&ST's after: ∃e₁∃e₂[P(e₁) ∧ Q(e₂) ∧ τ(e₂) ≺ τ(e₁)].

Double-existential: both the main-clause event and the subordinate-clause event must exist, and the subordinate event's runtime entirely precedes the main event's runtime.

Equations
Instances For
    source
    def Semantics.Tense.TemporalConnectives.OST.before {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
    Prop

    O&ST's before: ∃e₁[P(e₁) ∧ ∀e₂[Q(e₂) → τ(e₁) ≺ τ(e₂)]].

    Existential over the main clause, universal over the subordinate: the main event's runtime precedes that of EVERY potential subordinate event. When no Q-events exist, the universal is vacuously true — making before non-veridical.

    Equations
    Instances For
      source
      theorem Semantics.Tense.TemporalConnectives.OST.after_veridical {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
      after P Q → ∃ (e : Events.Ev Time), Q e

      After is veridical: after(P, Q) entails the complement Q.

      This follows directly from the double-existential structure: the definition asserts ∃e₂, Q(e₂), which witnesses the complement.

      source
      theorem Semantics.Tense.TemporalConnectives.OST.after_veridical_main {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
      after P Q → ∃ (e : Events.Ev Time), P e

      After is veridical w.r.t. the main clause too: both events must exist.

      source
      theorem Semantics.Tense.TemporalConnectives.OST.before_nonveridical :
      ∃ (P : Events.EvPred ℤ) (Q : Events.EvPred ℤ), before P Q ∧ ¬∃ (e : Events.Ev ℤ), Q e

      Before is non-veridical: there exist P, Q such that before(P, Q) holds but Q has no witnesses.

      Concretely: if P has a witness and Q is empty, then ∀e₂, Q(e₂) →... is vacuously true.

      source
      theorem Semantics.Tense.TemporalConnectives.OST.before_veridical_main {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
      before P Q → ∃ (e : Events.Ev Time), P e

      Before is still veridical w.r.t. its main clause: the P-event must exist.

      source
      theorem Semantics.Tense.TemporalConnectives.OST.after_implies_anscombe {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
      after P Q → Anscombe.after (eventDenotation P) (eventDenotation Q)

      O&ST's after implies Anscombe's after when projected through eventDenotation.

      Proof: from e₂.τ.precedes e₁.τ (i.e., e₂.τ.finish < e₁.τ.start), take t = e₁.τ.start and t' = e₂.τ.finish.

      source
      theorem Semantics.Tense.TemporalConnectives.OST.before_implies_anscombe {Time : Type u_1} [LinearOrder Time] (P Q : Events.EvPred Time) :
      before P Q → Anscombe.before (eventDenotation P) (eventDenotation Q)

      O&ST's before implies Anscombe's before when projected.

      Proof: from ∀e₂, Q(e₂) → e₁.τ.finish < e₂.τ.start, take t = e₁.τ.finish. For any t' ∈ timeTrace(eventDenotation Q), some e₂ has Q(e₂) and e₂.τ.start ≤ t', so t = e₁.τ.finish < e₂.τ.start ≤ t'.

      source
      theorem Semantics.Tense.TemporalConnectives.anscombe_before_not_implies_ost :
      ¬∀ (P Q : Events.EvPred ℤ), Anscombe.before (eventDenotation P) (eventDenotation Q) → OST.before P Q

      Anscombe's before does NOT imply O&ST's before: the converse of before_implies_anscombe fails.

      Counterexample: P-event at [1,5], Q-event at [3,8].

      • Anscombe: t=1 ∈ timeTrace P, and 1 < all t' ∈ [3,8]. ✓
      • O&ST: τ(e₁).finish = 5, τ(e₂).start = 3, and 5 < 3 is false. ✗

      The point-level theory sees a point in A before all of B; the event-level theory requires the entire A-runtime to precede the entire B-runtime.

      source
      theorem Semantics.Tense.TemporalConnectives.anscombe_after_not_implies_ost :
      ¬∀ (P Q : Events.EvPred ℤ), Anscombe.after (eventDenotation P) (eventDenotation Q) → OST.after P Q

      Anscombe's after does NOT imply O&ST's after: Anscombe allows the A-point to be inside B's runtime, while O&ST requires B's runtime to entirely precede A's.

      Counterexample: P-event at [5,5], Q-event at [1,8].

      • Anscombe: t=5, t'=1, 1 < 5. ✓
      • O&ST: τ(eQ).finish = 8 > 5 = τ(eP).start, so ¬precedes. ✗

      O&ST and Rett are incomparable when projected through eventDenotation:

      For after: O&ST requires only ONE Q-event to entirely precede the P-event (∃e₂, τ(e₂) ≺ τ(e₁)). Rett requires the P-event to follow the MAX of ALL Q-times (t > max(timeTrace Q)). When Q has multiple events and some extend past the P-event, O&ST.after holds but Rett.after fails.

      For before: O&ST allows vacuously true before when Q is empty (the ∀ over an empty domain). But Rett.before requires a witness in maxOnScale(timeTrace Q), which is empty when Q is empty. So O&ST.before holds vacuously but Rett.before fails. When Q has witnesses and a well-defined minimum, both agree.

      source
      theorem Semantics.Tense.TemporalConnectives.ost_after_not_implies_rett :
      ¬∀ (P Q : Events.EvPred ℤ), OST.after P Q → Rett.after (eventDenotation P) (eventDenotation Q)

      O&ST's after does NOT imply Rett's after: the existential quantifier in O&ST selects a single Q-event, but Rett's MAX aggregates over ALL Q-events.

      Counterexample: P at [5,5], Q₁ at [1,1], Q₂ at [10,10].

      • O&ST: eQ₁.τ = [1,1] precedes eP.τ = [5,5]. ✓
      • Rett: max(timeTrace Q) = 10, and 5 > 10 is false. ✗