Anscombe 1964: before and after

Before and after are not converses: the Parthenon was there after St. Peter's was and St. Peter's was there after the Parthenon was are compatible, while the corresponding before claims are not (§I). p before q is p and not q, and then q; it is asymmetric and transitive once repetition — p, then not p, then p — is excluded, whereas p after q, q and then p, is neither, and p before q entails q after p but not conversely (§II). Quantifying over times renders p before q as a time of p before every time of q (§IV), which is right for before ever rather than before (§V): the two agree exactly when q does not repeat. For instantaneous events before and after are genuine converses (§VIII); otherwise a beginning or an ending is always involved (§IX–§X).

A clause's present-tense proposition holds at the times of its timeTrace, so excluding repetition is Set.OrdConnected and an instantaneous event has a singleton trace.

References

• [Ans64]

Definitions

def Anscombe1964.Anscombe.before {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

p before q holds when p and not q, and then q (§II).

Equations

• Anscombe1964.Anscombe.before A B = ∃ t ∈ Tense.timeTrace A \ Tense.timeTrace B, ∃ t' ∈ Tense.timeTrace B, t < t'

def Anscombe1964.Anscombe.after {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

p after q holds when q, and then p, a time of p after a time of q (§II, §IV).

Equations

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

def Anscombe1964.Repetition {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) : Prop

A clause repeats when p, and then not p, and then p (§II).

Equations

• Anscombe1964.Repetition A = ∃ t₁ ∈ Tense.timeTrace A, ∃ t₂ ∉ Tense.timeTrace A, ∃ t₃ ∈ Tense.timeTrace A, t₁ < t₂ ∧ t₂ < t₃

def Anscombe1964.Instantaneous {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) : Prop

A clause reports an instantaneous event when it holds at a single time (§VIII).

Equations

• Anscombe1964.Instantaneous A = ∃ (t : T), Tense.timeTrace A = {t}

The logical properties (§II)

theorem Anscombe1964.not_repetition_iff_ordConnected {T : Type u_1} [LinearOrder T] {A : Set (NonemptyInterval T)} : ¬Repetition A ↔ (Tense.timeTrace A).OrdConnected

Repetition is excluded exactly when the clause holds over an order-connected set.

theorem Anscombe1964.before_asymm {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hA : (Tense.timeTrace A).OrdConnected) (hB : (Tense.timeTrace B).OrdConnected) : Anscombe.before A B → ¬Anscombe.before B A

Before is asymmetric when repetition is excluded.

theorem Anscombe1964.before_trans {T : Type u_1} [LinearOrder T] {A B C : Set (NonemptyInterval T)} (hB : (Tense.timeTrace B).OrdConnected) (hC : (Tense.timeTrace C).OrdConnected) : Anscombe.before A B → Anscombe.before B C → Anscombe.before A C

Before is transitive when repetition is excluded.

theorem Anscombe1964.before_not_asymm : ∃ (A : Set (NonemptyInterval ℤ)) (B : Set (NonemptyInterval ℤ)), Anscombe.before A B ∧ Anscombe.before B A

With repetition admitted, before is not asymmetric, as in it was night before it was day, and day before it was night.

theorem Anscombe1964.after_of_before {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} : Anscombe.before A B → Anscombe.after B A

p before q entails q after p.

theorem Anscombe1964.after_not_asymm : ∃ (A : Set (NonemptyInterval ℤ)) (B : Set (NonemptyInterval ℤ)), Anscombe.after A B ∧ Anscombe.after B A

After is not asymmetric, as the overlapping existences of the Parthenon and St. Peter's show.

theorem Anscombe1964.after_self_iff {T : Type u_1} [LinearOrder T] {A : Set (NonemptyInterval T)} : Anscombe.after A A ↔ (Tense.timeTrace A).Nontrivial

The Parthenon was there after the Parthenon was there might pass and I was born after I was born does not, since a clause is after itself iff it holds at two times.

theorem Anscombe1964.not_after_self_of_instantaneous {T : Type u_1} [LinearOrder T] {A : Set (NonemptyInterval T)} (hA : Instantaneous A) : ¬Anscombe.after A A

theorem Anscombe1964.after_not_trans : ∃ (A : Set (NonemptyInterval ℤ)) (B : Set (NonemptyInterval ℤ)), Anscombe.after A B ∧ Anscombe.after B A ∧ ¬Anscombe.after A A

After is not transitive, as in I was born after the Parthenon was there; the Parthenon was there after I was born; ergo, I was born after I was born.

Quantification over times (§IV–§V)

theorem Anscombe1964.before_of_beforeEver {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hB : (Tense.timeTrace B).Nonempty) : Tense.beforeEver A B → Anscombe.before A B

Before ever is before, provided q held at all.

theorem Anscombe1964.before_iff_beforeEver {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hB : (Tense.timeTrace B).OrdConnected) : Anscombe.before A B ↔ Tense.beforeEver A B ∧ (Tense.timeTrace B).Nonempty

For a non-repeating q, before is before ever (§V).

theorem Anscombe1964.before_not_beforeEver : ∃ (A : Set (NonemptyInterval ℤ)) (B : Set (NonemptyInterval ℤ)), Anscombe.before A B ∧ ¬Tense.beforeEver A B

He studied his appearance in the glass before he used the telephone does not say he did so before he ever used it, so before does not entail before ever.

theorem Anscombe1964.beforeEver_iff_lt_least {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {lb : T} (hlb : IsLeast (Tense.timeTrace B) lb) : Tense.beforeEver A B ↔ ∃ t ∈ Tense.timeTrace A, t < lb

When q has a first time, p before ever q holds iff a time of p precedes it.

Instantaneous events (§VI–§VIII)

theorem Anscombe1964.after_iff_before_of_instantaneous {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hA : Instantaneous A) : Anscombe.after A B ↔ Anscombe.before B A

When p reports an instantaneous event, p after q is q before p (§X, case 2).

theorem Anscombe1964.not_after_of_before_of_instantaneous {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hA : Instantaneous A) (hB : (Tense.timeTrace B).OrdConnected) (h : Anscombe.before A B) : ¬Anscombe.after A B

An instantaneous p is not both before and after a non-repeating q (§X, case 1).

theorem Anscombe1964.after_and_before_of_extended : ∃ (A : Set (NonemptyInterval ℤ)) (B : Set (NonemptyInterval ℤ)), Instantaneous B ∧ Anscombe.before A B ∧ Anscombe.after A B

A stretch can be both before and after an instantaneous event (§X, case 1).

Beginnings and endings (§IX–§X)

theorem Anscombe1964.nonempty_of_before {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} : Anscombe.before A B → (Tense.timeTrace B).Nonempty

p before q implies that q began.

theorem Anscombe1964.before_iff_lt_least {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {lb : T} (hB : (Tense.timeTrace B).OrdConnected) (hlb : IsLeast (Tense.timeTrace B) lb) : Anscombe.before A B ↔ ∃ t ∈ Tense.timeTrace A, t < lb

For a non-repeating q with a first time, p before q is p before q began.

theorem Anscombe1964.after_iff_least_lt {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {lb : T} (hlb : IsLeast (Tense.timeTrace B) lb) : Anscombe.after A B ↔ ∃ t ∈ Tense.timeTrace A, lb < t

p after q is p after q began (§III (3), §X case 3a); q before p gives it too (after_of_before, case 3b).

theorem Anscombe1964.after_of_greatest_lt {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} {ub : T} (hub : IsGreatest (Tense.timeTrace B) ub) : (∃ t ∈ Tense.timeTrace A, ub < t) → Anscombe.after A B

p after q stopped gives p after q (§III (4) to (3), §X case 3c).