PTS Constraints

@[reducible, inline]

abbrev Tense.TemporalAdverbials.PTSConstraint (Time : Type u_3) [LinearOrder Time] : Type u_3

A constraint on the Perfect Time Span. Adverbials restrict which PTS intervals are admissible.

Equations

• Tense.TemporalAdverbials.PTSConstraint Time = (NonemptyInterval Time → Prop)

inductive Tense.TemporalAdverbials.AdverbialType : Type

[IAI01] adverbial type classification.

• durative: specifies the left boundary (e.g., "since Monday")
• inclusive: does not specify the left boundary (e.g., "before Monday")

• durative : AdverbialType
• inclusive : AdverbialType

@[implicit_reducible]

instance Tense.TemporalAdverbials.instDecidableEqAdverbialType : DecidableEq AdverbialType

Equations

• Tense.TemporalAdverbials.instDecidableEqAdverbialType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tense.TemporalAdverbials.instReprAdverbialType.repr : AdverbialType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tense.TemporalAdverbials.instReprAdverbialType : Repr AdverbialType

Equations

• Tense.TemporalAdverbials.instReprAdverbialType = { reprPrec := Tense.TemporalAdverbials.instReprAdverbialType.repr }

Concrete Adverbials

def Tense.TemporalAdverbials.everSince {Time : Type u_2} [LinearOrder Time] (t₀ : Time) : PTSConstraint Time

"ever since t₀": PTS must start at t₀. E.g., "has been running since Monday" → PTS.fst = Monday.

Equations

• Tense.TemporalAdverbials.everSince t₀ pts = (pts.toProd.1 = t₀)

def Tense.TemporalAdverbials.forDurationFrom {Time : Type u_2} [LinearOrder Time] (tStart : Time) : PTSConstraint Time

"for (duration) from tStart": PTS must start at tStart. Simplified duration adverbial — the duration is implicit in the interval length [tStart, RB].

Equations

• Tense.TemporalAdverbials.forDurationFrom tStart pts = (pts.toProd.1 = tStart)

def Tense.TemporalAdverbials.always {Time : Type u_2} [LinearOrder Time] : PTSConstraint Time

"always" / no temporal adverbial: no constraint on PTS.

Equations

• Tense.TemporalAdverbials.always x✝ = True

def Tense.TemporalAdverbials.before {Time : Type u_2} [LinearOrder Time] : PTSConstraint Time

"before t" (inclusive adverbial): no constraint on PTS start. The adverbial constrains the event location, not the PTS boundary.

Equations

• Tense.TemporalAdverbials.before x✝ = True

LB Domain Extraction

def Tense.TemporalAdverbials.PTSConstraint.toLBDomain {Time : Type u_2} [LinearOrder Time] (adv : PTSConstraint Time) (tc : Time) : Set Time

Convert a PTS constraint to a domain of compatible LB values, given that the right boundary is fixed at tc.

For a constraint C, the compatible LBs are those tLB ≤ tc such that C holds of the interval [tLB, tc].

Equations

• adv.toLBDomain tc = {tLB : Time | tLB ≤ tc ∧ ∀ (h : tLB ≤ tc), adv { fst := tLB, snd := tc, fst_le_snd := h }}

PERF with Adverbial

def Tense.TemporalAdverbials.PERF_ADV {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.IntervalPred W Time) (adv : PTSConstraint Time) : Semantics.Aspect.PointPred W Time

Perfect with adverbial constraint: PERF_ADV(p, adv). Combines PERF with an adverbial constraint on the PTS. Equivalent to PERF_XN with the adverbial's derived LB domain.

Equations

• Tense.TemporalAdverbials.PERF_ADV p adv s = ∃ (pts : NonemptyInterval Time), Semantics.Aspect.RB pts s.time ∧ adv pts ∧ p s.world pts

Adverbial Type Properties

def Tense.TemporalAdverbials.AdverbialType.specifiesLB : AdverbialType → Bool

Does this adverbial type specify the left boundary? Durative adverbials pin the LB; inclusive adverbials leave it free.

Equations

• Tense.TemporalAdverbials.AdverbialType.durative.specifiesLB = true
• Tense.TemporalAdverbials.AdverbialType.inclusive.specifiesLB = false

Bridge Theorems

theorem Tense.TemporalAdverbials.perf_adv_eq_perf_xn {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.IntervalPred W Time) (adv : PTSConstraint Time) (tc : Time) (w : W) : PERF_ADV p adv { world := w, time := tc } ↔ Semantics.Aspect.PERF_XN p (adv.toLBDomain tc) { world := w, time := tc }

PERF_ADV is equivalent to PERF_XN with the adverbial's derived LB domain.

Proof sketch: Both existentially quantify over a PTS with RB = tc. PERF_ADV requires adv(PTS); PERF_XN requires LB(tLB, PTS) with tLB ∈ toLBDomain(adv, tc). These are equivalent by definition of toLBDomain: tLB ∈ toLBDomain ↔ tLB ≤ tc ∧ adv([tLB, tc]).

theorem Tense.TemporalAdverbials.everSince_specifies_lb {Time : Type u_2} [LinearOrder Time] (t₀ tc : Time) (h : t₀ ≤ tc) : (everSince t₀).toLBDomain tc = {t₀}

"ever since t₀" specifies the LB domain to exactly {t₀} (assuming t₀ ≤ tc).

Proof sketch: toLBDomain(everSince t₀, tc) = {tLB | tLB ≤ tc ∧ tLB = t₀} = {t₀} when t₀ ≤ tc.

theorem Tense.TemporalAdverbials.before_no_lb_constraint {Time : Type u_2} [LinearOrder Time] (tc : Time) : before.toLBDomain tc = {tLB : Time | tLB ≤ tc}

"before" imposes no LB constraint: all tLB ≤ tc are compatible.

Proof sketch: toLBDomain(before, tc) = {tLB | tLB ≤ tc ∧ True} = {tLB | tLB ≤ tc}.

theorem Tense.TemporalAdverbials.durative_licenses_u_perfect {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (t₀ tc : Time) (w : W) (_h : t₀ ≤ tc) : TenseAspectComposition.presPerfProgXN V {t₀} tc w → TenseAspectComposition.simplePresent V tc w

Durative adverbials (specified LB) license U-perf → simple present.

When the LB is pinned (durative adverbial), the U-perf reading entails the simple present via u_perf_entails_simple_present.

theorem Tense.TemporalAdverbials.inclusive_no_u_license {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : TenseAspectComposition.presPerfProgXN V Set.univ tc w ↔ TenseAspectComposition.simplePresent V tc w

Inclusive adverbials (unspecified LB) yield U-perf ↔ simple present when the LB domain is maximal.

With no LB constraint, the domain is {tLB | tLB ≤ tc}. Under IMPF (subinterval property), this is close to Set.univ for the relevant range, so U-perf ↔ simple present by broad_focus_equiv's argument.