@cite{anscombe-1964} / @cite{krifka-2010b}: Under-specification Semantics #
@cite{anscombe-1964} @cite{krifka-2010b} @cite{ladusaw-1980} @cite{beaver-condoravdi-2003}
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.
Anscombe's before B as a predicate on times (@cite{krifka-2010b}, 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
Instances For
Anscombe's after B as a predicate on times (@cite{krifka-2010b}, 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
Instances For
Heinämäki's analysis and equivalence with Anscombe #
@cite{heinamaki-1974}'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.
@cite{beaver-condoravdi-2003}: 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.
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
Instances For
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
Instances For
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
- Semantics.Tense.TemporalConnectives.isMinTime B lb = (lb ∈ Semantics.Tense.TemporalConnectives.timeTrace B ∧ ∀ t ∈ Semantics.Tense.TemporalConnectives.timeTrace B, lb ≤ t)
Instances For
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.
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.
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.
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.
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.
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 @cite{beaver-condoravdi-2003} express through earliest: the
universal force of earliest (selecting the minimum, which R-dominates
all other elements) creates a downward-entailing environment.
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."
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.
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.
Event-Level Temporal Connectives #
@cite{anscombe-1964} @cite{krifka-2010b}
@cite{anscombe-1964}'s point-level semantics and @cite{krifka-2010b}'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)] Double-existential: both events must exist.before(P, Q) =
e[P(e)e[Q(e)(e)
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
@cite{anscombe-1964} at Level 1 is preserved here at Level 3.
Level #
Level 3 (event predicates): operates on EvPred Time. Projects to
Level 2 via eventDenotation (EventBridge.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).
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 @cite{anscombe-1964}'s `` lifted from points to event runtimes.
Equations
- Semantics.Tense.TemporalConnectives.AnscombeEvent.after P Q = ∃ (e₁ : Semantics.Events.Event Time) (e₂ : Semantics.Events.Event Time), P e₁ ∧ Q e₂ ∧ e₂.τ.precedes e₁.τ
Instances For
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 @cite{anscombe-1964}'s `` lifted from points to event runtimes.
Equations
- Semantics.Tense.TemporalConnectives.AnscombeEvent.before P Q = ∃ (e₁ : Semantics.Events.Event Time), P e₁ ∧ ∀ (e₂ : Semantics.Events.Event Time), Q e₂ → e₁.τ.precedes e₂.τ
Instances For
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.
After is veridical w.r.t. the main clause too: both events must exist.
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.
Before is still veridical w.r.t. its main clause: the P-event must exist.
Event-level after implies @cite{anscombe-1964}'s after when projected
through eventDenotation.
Proof: from e..precedes e. (i.e.,e..finish < e..start), take t = e..startandt' = e..finish`.
Event-level before implies @cite{anscombe-1964}'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)ande..start t', so
t = e..finish < e..start t'`.
@cite{anscombe-1964}'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).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.
@cite{anscombe-1964}'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).finish = 8 > 5 =(eP).start, soprecedes.