[Ans64] / [Kri10]: Under-specification Semantics

[Ans64] [Kri10] [Lad80] [BC03]

Single lexical entry per connective. Both before and after are predicates on time points; multiple readings arise from which point of B is relevant, determined pragmatically by telicity.

• before B = λt. ∀t' ∈ B, t < t' (all of B follows the reference time)
• after B = λt. ∃t' ∈ B, t' < t (some of B precedes the reference time)

The quantificational asymmetry (∀ in before, ∃ in after) is already present here at Level 1 (point sets), though Anscombe did not highlight it as the source of the veridicality contrast.

Level

Level 1 (point sets): operates on timeTrace projections of SentDenotation.

def Tense.TemporalConnectives.Anscombe.before {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Anscombe's before B as a predicate on times ([Kri10], eq. 13a): λt. ∀t' ∈ times(B), t < t'. All times at which B holds follow t.

"A before B" then holds when some time in A satisfies this predicate.

Equations

• Tense.TemporalConnectives.Anscombe.before A B = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, ∀ t' ∈ Tense.TemporalConnectives.timeTrace B, t < t'

def Tense.TemporalConnectives.Anscombe.after {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : Prop

Anscombe's after B as a predicate on times ([Kri10], eq. 13b): λt. ∃t' ∈ times(B), t' < t. Some time at which B holds precedes t.

"A after B" then holds when some time in A satisfies this predicate.

Equations

• Tense.TemporalConnectives.Anscombe.after A B = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, ∃ t' ∈ Tense.TemporalConnectives.timeTrace B, t' < t

Heinämäki's analysis and equivalence with Anscombe

[Hei74]'s analysis uses a reference interval I(B) — the temporal interval associated with B — and defines before/after by comparison with that interval's boundary. This is the most standard textbook analysis.

[BC03]: Under two conditions — left-boundedness (B has a leftmost point) and instantiation (B is nonempty) — Anscombe and Heinämäki are truth-conditionally equivalent.

We formalize the reference point as leftBound (= inf of timeTrace B) and prove the equivalence. This completes the Level 4 → Level 1 projection: B&C's earliest unifies both classical Level 1 analyses.

def Tense.TemporalConnectives.Heinamaki.before {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (lb : Time) : Prop

Heinämäki's before: A happens before the reference point of B. The reference point lb is the left bound (minimum) of B's time trace. "A before B" iff some time in A precedes B's left bound.

Equations

• Tense.TemporalConnectives.Heinamaki.before A lb = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, t < lb

def Tense.TemporalConnectives.Heinamaki.after {Time : Type u_1} [LinearOrder Time] (A : SentDenotation Time) (lb : Time) : Prop

Heinämäki's after: A happens after the reference point of B. The reference point lb is the left bound (minimum) of B's time trace. "A after B" iff some time in A follows B's left bound.

Equations

• Tense.TemporalConnectives.Heinamaki.after A lb = ∃ t ∈ Tense.TemporalConnectives.timeTrace A, lb < t

def Tense.TemporalConnectives.isMinTime {Time : Type u_1} [LinearOrder Time] (B : SentDenotation Time) (lb : Time) : Prop

Left-boundedness (attained): lb is the minimum of timeTrace B — it belongs to B's time trace and is ≤ every element.

B&C use the infimum, but for SentDenotation (sets of closed intervals) the infimum is always attained (intervals include their endpoints via ≤). Using the minimum makes the equivalence proof constructive.

Equations

• Tense.TemporalConnectives.isMinTime B lb = (lb ∈ Tense.TemporalConnectives.timeTrace B ∧ ∀ t ∈ Tense.TemporalConnectives.timeTrace B, lb ≤ t)

theorem Tense.TemporalConnectives.anscombe_heinamaki_equiv_before {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (lb : Time) (hlb : isMinTime B lb) : Anscombe.before A B ↔ Heinamaki.before A lb

B&C Theorem 1 (before direction): Under left-boundedness (attained minimum), Anscombe's before ↔ Heinämäki's before.

Forward: a < all of B, lb ∈ B, so a < lb. Backward: a < lb, lb ≤ all of B, so a < all of B.

theorem Tense.TemporalConnectives.anscombe_heinamaki_equiv_after {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (lb : Time) (hlb : isMinTime B lb) : Anscombe.after A B ↔ Heinamaki.after A lb

B&C Theorem 1 (after direction): Under left-boundedness (attained minimum), Anscombe's after ↔ Heinämäki's after.

Forward: t' ∈ B with t' < a, lb ≤ t', so lb < a. Backward: lb < a, lb ∈ B, so lb witnesses the existential.

Before is a strict order (antisymmetric and transitive)

The ∃∀ quantifier pattern of before gives it strict-order-like properties. Antisymmetry: if some point in A precedes all of B, then no point in B can precede all of A (because A contains such a point). Transitivity: chaining through the ∀-quantified middle term.

theorem Tense.TemporalConnectives.Anscombe.before_antisymmetric {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) : before A B → ¬before B A

Before is antisymmetric: if A before B, then not B before A.

Proof: A before B gives a₀ ∈ A with a₀ < all of B. B before A would give b₀ ∈ B with b₀ < all of A. But a₀ < b₀ (from first) and b₀ < a₀ (from second). Contradiction.

theorem Tense.TemporalConnectives.Anscombe.before_transitive {Time : Type u_1} [LinearOrder Time] (A B C : SentDenotation Time) : before A B → before B C → before A C

Before is transitive: if A before B and B before C, then A before C.

Proof: A before B gives a₀ ∈ A with a₀ < all of B. B before C gives b₀ ∈ B with b₀ < all of C. Since a₀ < b₀ (from first, b₀ ∈ B) and b₀ < c for any c ∈ C, we have a₀ < c by transitivity of <.

After has neither property

The ∃∃ quantifier pattern of after is too weak: overlapping intervals give mutual after (breaking antisymmetry), and a gap in the middle term breaks transitivity.

theorem Tense.TemporalConnectives.Anscombe.after_not_antisymmetric : ∃ (A : SentDenotation ℤ) (B : SentDenotation ℤ), after A B ∧ after B A

After is NOT antisymmetric: overlapping time traces give A after B and B after A simultaneously.

Counterexample: A = {point 0, point 2}, B = {point 1, point 3}. A after B: t=2 ∈ A, t'=1 ∈ B, 1 < 2. B after A: t=3 ∈ B, t'=0 ∈ A, 0 < 3.

theorem Tense.TemporalConnectives.Anscombe.after_not_transitive : ∃ (A : SentDenotation ℤ) (B : SentDenotation ℤ) (C : SentDenotation ℤ), after A B ∧ after B C ∧ ¬after A C

After is NOT transitive: A after B and B after C need not give A after C.

Counterexample: A = {point 2}, B = {point 1, point 4}, C = {point 3}. A after B: t=2 ∈ A, t'=1 ∈ B, 1 < 2. B after C: t=4 ∈ B, t'=3 ∈ C, 3 < 4. Not A after C: only time in A is 2, only time in C is 3, and 3 ≮ 2.

Before is DE; after is UE in the complement position

The complement position of a temporal connective is the B argument in "A connective B." The quantifier structure of each connective determines its monotonicity, which in turn determines NPI licensing:

• before (∃∀): the ∀ over B reverses subset inclusion → DE → licenses NPIs
• after (∃∃): the ∃ over B preserves subset inclusion → UE → blocks NPIs

This is the same insight [BC03] express through earliest: the universal force of earliest (selecting the minimum, which R-dominates all other elements) creates a downward-entailing environment.

theorem Tense.TemporalConnectives.Anscombe.before_complement_DE {Time : Type u_1} [LinearOrder Time] (A B B' : SentDenotation Time) (h : timeTrace B' ⊆ timeTrace B) : before A B → before A B'

The complement position of before is downward-entailing: strengthening B (shrinking its time trace) preserves "A before B." This is why before licenses NPIs: "before anyone left" ⊨ "before any man left."

theorem Tense.TemporalConnectives.Anscombe.after_complement_UE {Time : Type u_1} [LinearOrder Time] (A B B' : SentDenotation Time) (h : timeTrace B ⊆ timeTrace B') : after A B → after A B'

The complement position of after is upward-entailing: weakening B (expanding its time trace) preserves "A after B." This is why after does NOT license NPIs.

theorem Tense.TemporalConnectives.npi_licensing_from_monotonicity {Time : Type u_1} [LinearOrder Time] (A B B' : SentDenotation Time) : (timeTrace B' ⊆ timeTrace B → Anscombe.before A B → Anscombe.before A B') ∧ (timeTrace B ⊆ timeTrace B' → Anscombe.after A B → Anscombe.after A B')

DE + UE are in the right direction: before entails downward in the complement (licenses NPIs), after entails upward (blocks NPIs). Stated as a single theorem for the contrast.

theorem Tense.TemporalConnectives.Anscombe.before_overgenerates {Time : Type u_1} [LinearOrder Time] (A B : SentDenotation Time) (hB : timeTrace B = ∅) (hA : (timeTrace A).Nonempty) : before A B

The Anscombe analysis overgenerates ([BC03] (32)-(33), the "ketchup" / "squares had four sides" examples): because before universally quantifies over B, "A before B" holds whenever A is instantiated and B never is. This vacuous truth — e.g. "David ate ketchup before he won all the gold medals" predicted true even if he never won — motivates B&C's modal refinement (BeaverCondoravdi.BC.before, relativized to historical alternatives, §3).

Event-Level Temporal Connectives

[Ans64] [Kri10]

[Ans64]'s point-level semantics and [Kri10]'s under-specification analysis lifted to Level 3 (event predicates), with direct quantification over events and their runtime intervals.

Core Insight: Quantificational Asymmetry at the Event Level

before and after differ in quantificational force over the complement:

• after(P, Q) = ee[P(e) Q(e) (e) (e)] Double-existential: both events must exist.

• before(P, Q) = e[P(e) e[Q(e) (e) (e`)]] Existential over P, universal over Q.

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). The same / pattern present in [Ans64] at Level 1 is preserved here at Level 3.

Level

Level 3 (event predicates): operates on Event Time → Prop. Projects to Level 2 via eventDenotation (Projection.lean).

Cross-Level Comparison

AnscombeEvent.after P Q Anscombe.after (eventDenotation P) (eventDenotation Q) but the converse fails: Anscombe allows partial overlap of runtimes, while the event-level version requires entire-runtime precedence (-precedence).

def Tense.TemporalConnectives.AnscombeEvent.after {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : Prop

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

This is [Ans64]'s `` lifted from points to event runtimes.

Equations

• Tense.TemporalConnectives.AnscombeEvent.after P Q = ∃ (e₁ : Event Time) (e₂ : Event Time), P e₁ ∧ Q e₂ ∧ e₂.τ.precedes e₁.τ

def Tense.TemporalConnectives.AnscombeEvent.before {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : Prop

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

This is [Ans64]'s `` lifted from points to event runtimes.

Equations

• Tense.TemporalConnectives.AnscombeEvent.before P Q = ∃ (e₁ : Event Time), P e₁ ∧ ∀ (e₂ : Event Time), Q e₂ → e₁.τ.precedes e₂.τ

theorem Tense.TemporalConnectives.AnscombeEvent.after_iff_allen {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : after P Q ↔ ∃ (e₁ : Event Time) (e₂ : Event Time), P e₁ ∧ Q e₂ ∧ AllenRelation.holdsIn AllenRelation.precedesSet e₂.τ e₁.τ

The event precedence underlying after is exactly the Allen precedes atom on run-times (precedesSet = {precedes}) — the relation Semantics/Tense/Reichenbach.lean already grounds tense in. Routing through Core/Order/AllenRelation reads the connective's temporal relation as a named atom-set rather than an ad-hoc inequality (and distinguishes it from Event.precedes of Semantics/Events/Adjacency.lean, which is the weaker {precedes, meets} that also admits abutment).

theorem Tense.TemporalConnectives.AnscombeEvent.before_iff_allen {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : before P Q ↔ ∃ (e₁ : Event Time), P e₁ ∧ ∀ (e₂ : Event Time), Q e₂ → AllenRelation.holdsIn AllenRelation.precedesSet e₁.τ e₂.τ

Dually, before relates the main event to every subordinate event by the same Allen precedes atom.

theorem Tense.TemporalConnectives.AnscombeEvent.after_veridical {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : after P Q → ∃ (e : Event 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.

theorem Tense.TemporalConnectives.AnscombeEvent.after_veridical_main {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : after P Q → ∃ (e : Event Time), P e

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

theorem Tense.TemporalConnectives.AnscombeEvent.before_nonveridical : ∃ (P : Event ℤ → Prop) (Q : Event ℤ → Prop), before P Q ∧ ¬∃ (e : Event ℤ), 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.

theorem Tense.TemporalConnectives.AnscombeEvent.before_veridical_main {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : before P Q → ∃ (e : Event Time), P e

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

theorem Tense.TemporalConnectives.AnscombeEvent.after_implies_anscombe {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : after P Q → Anscombe.after (eventDenotation P) (eventDenotation Q)

Event-level after implies [Ans64]'s after when projected through eventDenotation.

Proof: from e..precedes e. (i.e.,e..snd < e..fst), take t = e..fstandt' = e..snd`.

theorem Tense.TemporalConnectives.AnscombeEvent.before_implies_anscombe {Time : Type u_1} [LinearOrder Time] (P Q : Event Time → Prop) : before P Q → Anscombe.before (eventDenotation P) (eventDenotation Q)

Event-level before implies [Ans64]'s before when projected.

Proof: from e`, Q(e`) ` e`.`.snd < e`.`.fst`, take `t = e`.`.snd`. For any `t' ` timeTrace(eventDenotation Q)`, some `e has Q(e)ande..fst t', so t = e..snd < e..fst t'`.

theorem Tense.TemporalConnectives.anscombe_before_not_implies_event : ¬∀ (P Q : Event ℤ → Prop), Anscombe.before (eventDenotation P) (eventDenotation Q) → AnscombeEvent.before P Q

[Ans64]'s before does NOT imply the event-level 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]. `
• Event-level: (e).snd = 5, (e).fst = 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.

theorem Tense.TemporalConnectives.anscombe_after_not_implies_event : ¬∀ (P Q : Event ℤ → Prop), Anscombe.after (eventDenotation P) (eventDenotation Q) → AnscombeEvent.after P Q

[Ans64]'s after does NOT imply the event-level after: Anscombe allows the A-point to be inside B's runtime, while the event-level version 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. `
• Event-level: (eQ).snd = 8 > 5 = (eP).fst, so precedes.