Documentation

Linglib.Theories.Semantics.Tense.TemporalConnectives.Anscombe

@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.

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
          def Semantics.Tense.TemporalConnectives.isMinTime {Time : Type u_1} [LinearOrder Time] (B : SentDenotation Time) (lb : Time) :

          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
          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:

            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.