Beaver and Condoravdi (2003): a uniform before and after

Before and after differ in their logical properties, in licensing negative polarity items and in veridicality, which since Anscombe has been taken to show that their meanings are not uniform: a universal over the temporal clause for before and an existential for after. Beaver and Condoravdi show that on an instantiated temporal clause both are one connective, some main-clause time standing in an order to the earliest temporal-clause time (39), and the earliest time gives before its universal effect: it is downward entailing in its temporal clause wherever defined, and after upward entailing. Where the temporal clause is not instantiated, the earliest time is taken across alternatives branching from the world of evaluation at the main-clause time (47), so after stays veridical and before also has counterfactual and non-committal uses, which the context sorts (48).

Main results

• uniform_lt_iff_beforeEver, uniform_gt_iff_after: Proposition 2, the uniform connective is Anscombe's before and after on a temporal clause with a first time.
• isStrawsonDE_before, isStrawsonUE_after: the uniform before is Strawson downward entailing in its temporal clause and after Strawson upward entailing.
• connective_iff_uniform_of_inst: on an instantiated temporal clause, (47) is (45).
• after_veridical, veridical_inter_after: after entails its temporal clause, so a context updated with it is veridical (§6).
• existsUnique_reading: each nonempty context has exactly one of the readings of (48).
• mozart_update: in the context of p. 51, Mozart died before he finished the Requiem keeps exactly the worlds of its counterfactual reading.

Implementation notes

• The alternatives come from a T × W frame whose historical equivalence at t is agreement at all earlier times, and a clause respects it when historically equivalent worlds agree on it before t. The normality condition on alternatives (p. 50) is a choice of the model.
• In connective an undefined earliest time makes the sentence false. A context update discards both, so the readings of (48) are unaffected; the trivalent propositions beforeP and afterP keep the definedness condition for von Fintel's Strawson entailment.

TODO

• Heinämäki's interval semantics (35)–(38) and Proposition 1.

References

• [BC03]
• [Ans64]
• [Hei74]
• [Tho84]
• [vF99a]

The uniform connective (39)

Anscombe's before (27) quantifies universally over the temporal clause and her after existentially. On a temporal clause with a first time both compare a main-clause time with the first one, since a time precedes every time of the clause iff it precedes the first, and follows some time of the clause iff it follows the first (§5).

def BeaverCondoravdi2003.uniform {T : Type u_1} [LinearOrder T] (cmp : T → T → Prop) (A B : Set T) : Prop

The uniform connective (39) holds when some time of A stands in cmp to the earliest time of B.

Equations

• BeaverCondoravdi2003.uniform cmp A B = ∃ t ∈ A, ∃ (e : T), IsLeast B e ∧ cmp t e

theorem BeaverCondoravdi2003.uniform_lt_iff_beforeEver {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hB : ∃ (e : T), IsLeast (Tense.timeTrace B) e) : uniform (fun (x1 x2 : T) => x1 < x2) (Tense.timeTrace A) (Tense.timeTrace B) ↔ Tense.beforeEver A B

On a temporal clause with a first time, the uniform before is Anscombe's universal before, Proposition 2 for before.

theorem BeaverCondoravdi2003.uniform_gt_iff_after {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hB : ∃ (e : T), IsLeast (Tense.timeTrace B) e) : uniform (fun (x1 x2 : T) => x1 > x2) (Tense.timeTrace A) (Tense.timeTrace B) ↔ Anscombe1964.Anscombe.after A B

On a temporal clause with a first time, the uniform after is Anscombe's existential after, Proposition 2 for after.

theorem BeaverCondoravdi2003.anscombe_before_complement_DE {T : Type u_1} [LinearOrder T] {A B B' : Set (NonemptyInterval T)} (h : Tense.timeTrace B' ⊆ Tense.timeTrace B) : Tense.beforeEver A B → Tense.beforeEver A B'

The temporal clause of Anscombe's before is downward entailing, the NPI-licensing environment (29).

theorem BeaverCondoravdi2003.anscombe_after_complement_UE {T : Type u_1} [LinearOrder T] {A B B' : Set (NonemptyInterval T)} (h : Tense.timeTrace B ⊆ Tense.timeTrace B') : Anscombe1964.Anscombe.after A B → Anscombe1964.Anscombe.after A B'

The temporal clause of Anscombe's after is upward entailing (31).

theorem BeaverCondoravdi2003.anscombe_before_of_empty {T : Type u_1} [LinearOrder T] {A B : Set (NonemptyInterval T)} (hB : Tense.timeTrace B = ∅) (hA : (Tense.timeTrace A).Nonempty) : Tense.beforeEver A B

With a never-instantiated temporal clause Anscombe's before holds of any instantiated main clause, the overgeneration of (32) and (33), so David ate lots of ketchup before he made a clean sweep of all the gold medals comes out true if he never won.

Polarity

At a world the uniform connective (45) is a trivalent proposition, defined where the temporal clause has an earliest time in the world. Its before is then downward entailing in the temporal clause wherever it is defined, since a smaller clause starts no earlier, and its after upward entailing, so earliest gives before the universal effect that licenses negative polarity items (§7).

noncomputable def BeaverCondoravdi2003.beforeP {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) : W → SignType

A before B at a world, (45), defined where B has an earliest time in the world.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BeaverCondoravdi2003.afterP {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) : W → SignType

A after B at a world, (45), defined where B has an earliest time in the world.

Equations

• One or more equations did not get rendered due to their size.

theorem BeaverCondoravdi2003.isStrawsonDE_before {W : Type u_1} {T : Type u_2} [LinearOrder T] (A : Set (W × T)) : NaturalLogic.IsStrawsonDE (beforeP A)

The uniform before is Strawson downward entailing in its temporal clause.

theorem BeaverCondoravdi2003.isStrawsonUE_after {W : Type u_1} {T : Type u_2} [LinearOrder T] (A : Set (W × T)) : NaturalLogic.IsStrawsonUE (afterP A)

The uniform after is Strawson upward entailing in its temporal clause.

Alternatives and the modal connective (44)–(47)

Where the temporal clause is not instantiated in the world of evaluation, the earliest time is taken across alternatives of the world at the main-clause time (47). The alternatives lie among the historical alternatives at that time, the worlds agreeing with it at all earlier times, the initial branch point condition, and a world in which the temporal clause is instantiated is its own only alternative (p. 50). An earlier temporal-clause time then lies before the branching, so after is veridical, while a later one may lie on another branch (§6).

def BeaverCondoravdi2003.instTimes {W : Type u_1} {T : Type u_2} (worlds : Set W) (B : Set (W × T)) : Set T

The times at which B is instantiated in some world of worlds (46).

Equations

• BeaverCondoravdi2003.instTimes worlds B = {t : T | ∃ w ∈ worlds, (w, t) ∈ B}

def BeaverCondoravdi2003.Inst {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (w : W) : Prop

B is instantiated in w when it holds there at some time.

Equations

• BeaverCondoravdi2003.Inst B w = ∃ (t : T), (w, t) ∈ B

def BeaverCondoravdi2003.connective {W : Type u_1} {T : Type u_2} [LinearOrder T] (cmp : T → T → Prop) (A B : Set (W × T)) (alt : HistoricalAlternatives W T) (w : W) : Prop

The connective (47) holds at w when some main-clause time stands in cmp to the earliest temporal-clause time across the alternatives of w at that time.

Equations

• BeaverCondoravdi2003.connective cmp A B alt w = ∃ (t : T), (w, t) ∈ A ∧ ∃ (e : T), IsLeast (BeaverCondoravdi2003.instTimes (alt (w, t)) B) e ∧ cmp t e

@[reducible, inline]

abbrev BeaverCondoravdi2003.before {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistoricalAlternatives W T) (w : W) : Prop

A before B (47).

Equations

• BeaverCondoravdi2003.before A B alt w = BeaverCondoravdi2003.connective (fun (x1 x2 : T) => x1 < x2) A B alt w

@[reducible, inline]

abbrev BeaverCondoravdi2003.after {W : Type u_1} {T : Type u_2} [LinearOrder T] (A B : Set (W × T)) (alt : HistoricalAlternatives W T) (w : W) : Prop

A after B (47).

Equations

• BeaverCondoravdi2003.after A B alt w = BeaverCondoravdi2003.connective (fun (x1 x2 : T) => x1 > x2) A B alt w

theorem BeaverCondoravdi2003.connective_iff_uniform_of_eq_singleton {W : Type u_1} {T : Type u_2} [LinearOrder T] {cmp : T → T → Prop} {A B : Set (W × T)} {alt : HistoricalAlternatives W T} {w : W} (h : ∀ (t : T), alt (w, t) = {w}) : connective cmp A B alt w ↔ uniform cmp {t : T | (w, t) ∈ A} {t : T | (w, t) ∈ B}

With the world as its own only alternative, (47) is the uniform connective (45) on the times of the world.

theorem BeaverCondoravdi2003.connective_alt_inst {W : Type u_1} {T : Type u_2} [LinearOrder T] {cmp : T → T → Prop} {A B : Set (W × T)} {alt : HistoricalAlternatives W T} {w : W} (h : connective cmp A B alt w) : ∃ (t : T), (w, t) ∈ A ∧ ∃ w' ∈ alt (w, t), Inst B w'

Even a non-veridical before places its temporal clause on an alternative, (49).

def BeaverCondoravdi2003.RespectsHistory {W : Type u_1} {T : Type u_2} [LinearOrder T] (F : Temporal.TWFrame W T) (B : Set (W × T)) : Prop

A clause respects the historical equivalence of a frame when worlds historically equivalent at t agree on it at all earlier times.

Equations

• BeaverCondoravdi2003.RespectsHistory F B = ∀ ⦃w w' : W⦄ ⦃t t' : T⦄, t' < t → (F.sim t) w w' → ((w, t') ∈ B ↔ (w', t') ∈ B)

structure BeaverCondoravdi2003.Alternatives {W : Type u_1} {T : Type u_2} [LinearOrder T] (F : Temporal.TWFrame W T) (B : Set (W × T)) : Type (max u_1 u_2)

Beaver and Condoravdi's alternatives for a temporal clause over a frame (p. 50) lie among the historical alternatives and leave a world instantiating the clause as its own only alternative.

• alt : HistoricalAlternatives W T

  The alternatives of a world at a time.

• subset_alternatives (i : Reference.Index W T) : self.alt i ⊆ F.alternatives i

  The initial branch point condition.

• eq_singleton_of_inst ⦃w : W⦄ : Inst B w → ∀ (t : T), self.alt (w, t) = {w}

  A world in which the temporal clause is instantiated is its own only alternative.

theorem BeaverCondoravdi2003.connective_iff_uniform_of_inst {W : Type u_1} {T : Type u_2} [LinearOrder T] {cmp : T → T → Prop} {A B : Set (W × T)} {w : W} {F : Temporal.TWFrame W T} (a : Alternatives F B) (hw : Inst B w) : connective cmp A B a.alt w ↔ uniform cmp {t : T | (w, t) ∈ A} {t : T | (w, t) ∈ B}

On a temporal clause instantiated in the world, (47) is (45).

theorem BeaverCondoravdi2003.after_veridical {W : Type u_1} {T : Type u_2} [LinearOrder T] {A B : Set (W × T)} {w : W} {F : Temporal.TWFrame W T} (a : Alternatives F B) (hB : RespectsHistory F B) : after A B a.alt w → Inst B w

After entails its temporal clause (§6). Its earliest time precedes the main-clause time, so the alternative instantiating it agrees with the world there.

The readings of before (48)

A context, a set of worlds, is updated with a sentence by keeping the worlds at which it is true (p. 51). A context updated with A after B is always veridical, while one updated with A before B is veridical, counterfactual or non-committal, depending on the context.

inductive BeaverCondoravdi2003.BeforeReading : Type

The three readings of before (48).

• veridical : BeforeReading
• counterfactual : BeforeReading
• nonCommittal : BeforeReading

@[instance_reducible]

instance BeaverCondoravdi2003.instDecidableEqBeforeReading : DecidableEq BeforeReading

Equations

• BeaverCondoravdi2003.instDecidableEqBeforeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaverCondoravdi2003.instReprBeforeReading.repr : BeforeReading → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance BeaverCondoravdi2003.instReprBeforeReading : Repr BeforeReading

Equations

• BeaverCondoravdi2003.instReprBeforeReading = { reprPrec := BeaverCondoravdi2003.instReprBeforeReading.repr }

def BeaverCondoravdi2003.Veridical {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (c : Set W) : Prop

The veridical reading has every world of the context instantiate B.

Equations

• BeaverCondoravdi2003.Veridical B c = ∀ w ∈ c, BeaverCondoravdi2003.Inst B w

def BeaverCondoravdi2003.Counterfactual {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (c : Set W) : Prop

The counterfactual reading has no world of the context instantiate B.

Equations

• BeaverCondoravdi2003.Counterfactual B c = ∀ w ∈ c, ¬BeaverCondoravdi2003.Inst B w

def BeaverCondoravdi2003.NonCommittal {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (c : Set W) : Prop

The non-committal reading has some worlds of the context instantiate B and some not.

Equations

• BeaverCondoravdi2003.NonCommittal B c = ((∃ w ∈ c, BeaverCondoravdi2003.Inst B w) ∧ ∃ w ∈ c, ¬BeaverCondoravdi2003.Inst B w)

def BeaverCondoravdi2003.BeforeReading.Holds {W : Type u_1} {T : Type u_2} (B : Set (W × T)) (c : Set W) : BeforeReading → Prop

The property of a context that a reading names.

Equations

• BeaverCondoravdi2003.BeforeReading.Holds B c BeaverCondoravdi2003.BeforeReading.veridical = BeaverCondoravdi2003.Veridical B c
• BeaverCondoravdi2003.BeforeReading.Holds B c BeaverCondoravdi2003.BeforeReading.counterfactual = BeaverCondoravdi2003.Counterfactual B c
• BeaverCondoravdi2003.BeforeReading.Holds B c BeaverCondoravdi2003.BeforeReading.nonCommittal = BeaverCondoravdi2003.NonCommittal B c

theorem BeaverCondoravdi2003.existsUnique_reading {W : Type u_1} {T : Type u_2} {B : Set (W × T)} {c : Set W} (hc : c.Nonempty) : ∃! r : BeforeReading, BeforeReading.Holds B c r

Each nonempty context has exactly one of the readings (48).

theorem BeaverCondoravdi2003.veridical_inter_after {W : Type u_1} {T : Type u_2} [LinearOrder T] {A B : Set (W × T)} {F : Temporal.TWFrame W T} (a : Alternatives F B) (hB : RespectsHistory F B) (c : Set W) : Veridical B (c ∩ {w : W | after A B a.alt w})

A context updated with A after B is veridical (p. 51).

theorem BeaverCondoravdi2003.alt_inst_of_mem_inter_before {W : Type u_1} {T : Type u_2} [LinearOrder T] {A B : Set (W × T)} {alt : HistoricalAlternatives W T} {c : Set W} {w : W} (hw : w ∈ c ∩ {w : W | before A B alt w}) : ∃ (t : T), (w, t) ∈ A ∧ ∃ w' ∈ alt (w, t), Inst B w'

Every world of a context updated with A before B has, at a main-clause time, an alternative instantiating B, (49).

The Mozart example

In the context in which (40) is uttered, Mozart finishes the Requiem before dying in the finish world, dies first with a normal alternative in which he lives longer and finishes it in the early world, and dies first with a normal alternative in which he lives longer and still does not finish it in the idle world. Updating the context with Mozart died before he finished the Requiem discards the first as false and the third as undefined, leaving a counterfactual context (p. 51).

inductive BeaverCondoravdi2003.World : Type

The worlds of the Mozart example, with the alternatives later of early and idleLater of idle.

• finish : World
• early : World
• later : World
• idle : World
• idleLater : World

@[instance_reducible]

instance BeaverCondoravdi2003.instDecidableEqWorld : DecidableEq World

Equations

• BeaverCondoravdi2003.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaverCondoravdi2003.instReprWorld.repr : World → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance BeaverCondoravdi2003.instReprWorld : Repr World

Equations

• BeaverCondoravdi2003.instReprWorld = { reprPrec := BeaverCondoravdi2003.instReprWorld.repr }

def BeaverCondoravdi2003.World.death : World → ℕ

The time at which Mozart dies.

Equations

• BeaverCondoravdi2003.World.finish.death = 2
• BeaverCondoravdi2003.World.early.death = 1
• BeaverCondoravdi2003.World.later.death = 3
• BeaverCondoravdi2003.World.idle.death = 1
• BeaverCondoravdi2003.World.idleLater.death = 3

def BeaverCondoravdi2003.World.completion : World → Option ℕ

The time at which Mozart finishes the Requiem, if he does.

Equations

• BeaverCondoravdi2003.World.finish.completion = some 1
• BeaverCondoravdi2003.World.later.completion = some 2
• x✝.completion = none

def BeaverCondoravdi2003.dies : Set (World × ℕ)

The world–time pairs at which Mozart dies.

Equations

• BeaverCondoravdi2003.dies = {i : BeaverCondoravdi2003.World × ℕ | i.1.death = i.2}

def BeaverCondoravdi2003.finishes : Set (World × ℕ)

The world–time pairs at which Mozart finishes the Requiem.

Equations

• BeaverCondoravdi2003.finishes = {i : BeaverCondoravdi2003.World × ℕ | i.1.completion = some i.2}

def BeaverCondoravdi2003.frame : Temporal.TWFrame World ℕ

Worlds are historically equivalent at t when they agree on Mozart's death and on his finishing at all earlier times, each fact being settled from the next time on.

Equations

• One or more equations did not get rendered due to their size.

theorem BeaverCondoravdi2003.respectsHistory_finishes : RespectsHistory frame finishes

theorem BeaverCondoravdi2003.mem_alternatives_of_le_one {t : ℕ} (ht : t ≤ 1) (w v : World) : v ∈ frame.alternatives (w, t)

No fact is dated at time 0, so up to time 1 every world is a historical alternative to every other.

def BeaverCondoravdi2003.alt : HistoricalAlternatives World ℕ

The alternatives of the context, a world being its own only alternative except at the times up to Mozart's death in early and idle, where the world in which he lives longer is normal.

Equations

• BeaverCondoravdi2003.alt (BeaverCondoravdi2003.World.early, t) = if t ≤ 1 then {BeaverCondoravdi2003.World.early, BeaverCondoravdi2003.World.later} else {BeaverCondoravdi2003.World.early}
• BeaverCondoravdi2003.alt (BeaverCondoravdi2003.World.idle, t) = if t ≤ 1 then {BeaverCondoravdi2003.World.idle, BeaverCondoravdi2003.World.idleLater} else {BeaverCondoravdi2003.World.idle}
• BeaverCondoravdi2003.alt (w, snd) = {w}

def BeaverCondoravdi2003.alternatives : Alternatives frame finishes

The alternatives of the Mozart example meet the conditions of p. 50.

Equations

• One or more equations did not get rendered due to their size.

def BeaverCondoravdi2003.context : Set World

The context in which (40) is uttered, one world of each kind.

Equations

• BeaverCondoravdi2003.context = {BeaverCondoravdi2003.World.finish, BeaverCondoravdi2003.World.early, BeaverCondoravdi2003.World.idle}

theorem BeaverCondoravdi2003.mozart_update : context ∩ {w : World | before dies finishes alt w} = {World.early}

Updating the context with Mozart died before he finished the Requiem keeps exactly the early world.

theorem BeaverCondoravdi2003.counterfactual_mozart : Counterfactual finishes (context ∩ {w : World | before dies finishes alt w})

The updated context is counterfactual, Mozart finishing the Requiem in none of its worlds.

The examples

def BeaverCondoravdi2003.readingOf : String → Option BeforeReading

The reading a row reports.

Equations

• BeaverCondoravdi2003.readingOf "veridical" = some BeaverCondoravdi2003.BeforeReading.veridical
• BeaverCondoravdi2003.readingOf "counterfactual" = some BeaverCondoravdi2003.BeforeReading.counterfactual
• BeaverCondoravdi2003.readingOf "non-committal" = some BeaverCondoravdi2003.BeforeReading.nonCommittal
• BeaverCondoravdi2003.readingOf x✝ = none

theorem BeaverCondoravdi2003.rows_nonVeridical_before (e : Datum) : e ∈ Examples.all → ∀ r ∈ (e.feature? "reading" >>= readingOf).toList, r ≠ BeforeReading.veridical → e.feature? "connective" = some "before"

Every row reporting a non-veridical reading is a before sentence, as the veridicality of after, veridical_inter_after, predicts.