Condoravdi 2002: Temporal Interpretation of Modals

Non-root modals expand the time of evaluation forward and instantiate the property in their scope in the worlds of a modal base. Modals for the past are the same modals over the perfect, so might have is ambiguous between the modal over the perfect, an epistemic possibility about the past, and the perfect over the modal, a metaphysical possibility from a past perspective. Frame adverbials follow from intersecting the reference interval with the period named, still and already over a modal from the shrinking of live options as time advances, and the choice of modal base from the diversity condition, which a settled issue fails. The operators are stated over closed intervals of times that may run to the end of time.

Implementation notes

• The paper's now is an interval, albeit a short one, taken here as a point, and a modal base is indexed by the start of the reference interval; the paper's MB(w, t) takes an interval and its w ≃_t w' a point.
• Identity of the past enters as FixesPast, discharged for histories built from dated facts by fixesPast_eventive and fixesPast_stative; the counterfactual implication rests on the paper's footnote assumption PastAlternativesOutside.
• The sortal restriction of already, yet and still is partiality, and only the prior-phase half of their Löbner presuppositions is stated.

TODO

• The embedded modals of Mary believed that John may get sick are informal in the paper and absent here.
• He has still won is excluded by the paper as well known rather than derived; the German noch pattern that rests on it is a row, not a theorem.

References

• C. Condoravdi, Temporal Interpretation of Modals (2002)
• F. Mondadori, Remarks on Tense and Mood: The Perfect Future (1978)
• D. Abusch, Sequence of Tense and Temporal De Re (1997)
• D. Abusch, Generalizing Tense Semantics for Future Contexts (1998)
• M. Enç, Tense and Modality (1996)
• J. Groenendijk and M. Stokhof, Modality and Conversational Information (1975)
• A. Kratzer, The Notional Category of Modality (1981)
• D. Lewis, Counterfactual Dependence and Time's Arrow (1979)
• S. Löbner, German schon, erst, noch: An Integrated Analysis (1989)
• R. Thomason, Combinations of Tense and Modality (1984)

The operators

def Condoravdi2002.PRES {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (now : T) (Q : Aspect.SortedProperty W E T) (w : W) : Prop

The present tense instantiates the property at the time of utterance.

Equations

• Condoravdi2002.PRES now Q w = Aspect.At (Interval.pure ↑now) w Q

def Condoravdi2002.PERF {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

The perfect instantiates the property at some interval preceding the reference interval.

Equations

• Condoravdi2002.PERF Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => ∃ (t' : NonemptyInterval (WithTop T)), (↑t').Precedes t ∧ Aspect.At (↑t') w Q

def Condoravdi2002.MAY {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (MB : W → T → Set W) (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

MAY and MIGHT instantiate the property in some world of the modal base at the start of the reference interval, throughout the interval expanded forward to the end of time.

Equations

• Condoravdi2002.MAY MB Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => ∃ (t₀ : T), IsLeast ↑t ↑t₀ ∧ ∃ w' ∈ MB w t₀, Aspect.At (Interval.Ici ↑t₀) w' Q

def Condoravdi2002.WOLL {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (MB : W → T → Set W) (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

WOLL, the untensed modal of will and would, instantiates the property in every world of the modal base at the start of the reference interval, throughout the forward interval.

Equations

• Condoravdi2002.WOLL MB Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => ∃ (t₀ : T), IsLeast ↑t ↑t₀ ∧ ∀ w' ∈ MB w t₀, Aspect.At (Interval.Ici ↑t₀) w' Q

def Condoravdi2002.frame {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (period : Interval (WithTop T)) (Q : Aspect.SortedProperty W E T) : Aspect.SortedProperty W E T

A frame adverbial such as yesterday instantiates a property of eventualities within the intersection of the reference interval with the period named. The paper leaves it undefined on properties of times, which the theorems carry as IsEventuality.

Equations

• Condoravdi2002.frame period Q = Aspect.SortedProperty.temporal fun (w : W) (t : Interval (WithTop T)) => Aspect.At (t ⊓ period) w Q

def Condoravdi2002.phase {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] : Aspect.SortedProperty W E T → Option (Aspect.SortedProperty W E T)

Already, yet and still are the identity on properties of states and of times and undefined on properties of events.

Equations

• Condoravdi2002.phase (Aspect.SortedProperty.eventive P) = none
• Condoravdi2002.phase x✝ = some x✝

Characterizations

theorem Condoravdi2002.at_coe_may_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {i : NonemptyInterval (WithTop T)} : Aspect.At (↑i) w (MAY MB Q) ↔ ∃ (t₀ : T), i.toProd.1 = ↑t₀ ∧ ∃ w' ∈ MB w t₀, Aspect.At (Interval.Ici ↑t₀) w' Q

At a nonempty interval, MAY takes its modal base at the interval's start.

@[simp]

theorem Condoravdi2002.pres_may_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {now : T} : PRES now (MAY MB Q) w ↔ ∃ w' ∈ MB w now, Aspect.At (Interval.Ici ↑now) w' Q

At the present, MAY holds when some world of the base at the present has the property throughout the forward interval.

@[simp]

theorem Condoravdi2002.pres_woll_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {now : T} : PRES now (WOLL MB Q) w ↔ ∀ w' ∈ MB w now, Aspect.At (Interval.Ici ↑now) w' Q

At the present, WOLL holds when every world of the base at the present has the property throughout the forward interval.

@[simp]

theorem Condoravdi2002.at_Ici_perf_eventive_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} : Aspect.At (Interval.Ici ↑t) w (PERF (Aspect.SortedProperty.eventive P)) ↔ ∃ (e : E), P w e ∧ (Event.τ e).toProd.2 < t

The perfect of an event holds at a ray when the event ended before the ray starts.

@[simp]

theorem Condoravdi2002.pres_perf_may_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {now : T} : PRES now (PERF (MAY MB Q)) w ↔ ∃ t' < now, ∃ w' ∈ MB w t', Aspect.At (Interval.Ici ↑t') w' Q

At the present, the perfect over MAY holds when some past time has, in some world of the base at that time, the property throughout that time's forward interval.

The three readings

theorem Condoravdi2002.pres_may_eventive_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {MB : W → T → Set W} {now : T} : PRES now (MAY MB (Aspect.SortedProperty.eventive P)) w ↔ ∃ w' ∈ MB w now, ∃ (e : E), P w' e ∧ now ≤ (Event.τ e).toProd.1

A modal for the present with an eventive predicate, he might run, holds when some world of the base at the present has the event starting no earlier than the present. Future orientation is obligatory.

theorem Condoravdi2002.pres_may_stative_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {MB : W → T → Set W} {now : T} : PRES now (MAY MB (Aspect.SortedProperty.stative P)) w ↔ ∃ w' ∈ MB w now, ∃ (e : E), P w' e ∧ now ≤ (Event.τ e).toProd.2

A modal for the present with a stative predicate, he might be here, holds when some world of the base at the present has the state persisting at or past the present. The state may have started earlier, so future orientation is optional.

theorem Condoravdi2002.pres_may_perf_eventive_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {MB : W → T → Set W} {now : T} : PRES now (MAY MB (PERF (Aspect.SortedProperty.eventive P))) w ↔ ∃ w' ∈ MB w now, ∃ (e : E), P w' e ∧ (Event.τ e).toProd.2 < now

The modal over the perfect, he may have won, holds when some world of the base at the present has the event ending before the present. This is the epistemic reading, with present perspective and past orientation.

theorem Condoravdi2002.pres_perf_may_eventive_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {MB : W → T → Set W} {now : T} : PRES now (PERF (MAY MB (Aspect.SortedProperty.eventive P))) w ↔ ∃ t' < now, ∃ w' ∈ MB w t', ∃ (e : E), P w' e ∧ t' ≤ (Event.τ e).toProd.1

The perfect over the modal, he might have won, holds when some past time has, in some world of the base at that time, the event starting no earlier than it. This is the counterfactual reading, with past perspective and future orientation, Mondadori's future in the past.

Frame adverbials

theorem Condoravdi2002.frame_modal_past {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {now : T} (hQ : Q.IsEventuality) {period : Interval (WithTop T)} (hp : period.Precedes (Interval.Ici ↑now)) : ¬PRES now (MAY MB (frame period Q)) w

A modal for the present rejects a period wholly before the present, he may win yesterday, since the forward interval meets it in the null interval.

theorem Condoravdi2002.frame_modalPerf_nonpast {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {MB : W → T → Set W} {now : T} (hQ : Q.IsEventuality) {period : Interval (WithTop T)} (hp : period ≤ Interval.Ici ↑now) : ¬PRES now (MAY MB (PERF (frame period Q))) w

The modal over the perfect rejects a period lying at or after the present, he must have been available next month and it must have been raining now, since the interval the perfect supplies precedes the present, and so the period.

Live options shrink

theorem Condoravdi2002.may_antitone {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {history : HistoricalAlternatives W T} (hBC : ∀ (w : W), Antitone (history.metaphysicalBase w)) (hQ : Q.IsEventuality) : Antitone fun (t : T) => PRES t (MAY history.metaphysicalBase Q) w

A possibility at a time was a possibility at every earlier time, since the metaphysical base widens backward and the forward interval lengthens. This is why still, whose presupposition is a prior positive phase, scopes over a possibility modal, he may still win, and already, whose presupposition is a prior negative phase, cannot, he may already win; read backward, it is why he may win this game is false once he has lost.

def Condoravdi2002.AlreadyPresup {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (Q : Aspect.SortedProperty W E T) (w : W) (now : T) : Prop

The prior-phase half of Löbner's presupposition of already requires a prior negative phase.

Equations

• Condoravdi2002.AlreadyPresup Q w now = ∃ t' < now, ¬Condoravdi2002.PRES t' Q w

def Condoravdi2002.StillPresup {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (Q : Aspect.SortedProperty W E T) (w : W) (now : T) : Prop

The prior-phase half of Löbner's presupposition of still requires a prior positive phase.

Equations

• Condoravdi2002.StillPresup Q w now = ∃ t' < now, Condoravdi2002.PRES t' Q w

theorem Condoravdi2002.not_already_may {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {now : T} {history : HistoricalAlternatives W T} (hBC : ∀ (w : W), Antitone (history.metaphysicalBase w)) (hQ : Q.IsEventuality) (h : PRES now (MAY history.metaphysicalBase Q) w) : ¬AlreadyPresup (MAY history.metaphysicalBase Q) w now

In he may already win, the presupposition of already over a metaphysical possibility contradicts its assertion.

theorem Condoravdi2002.still_may {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {t' : T} {w : W} {now : T} {history : HistoricalAlternatives W T} (hBC : ∀ (w : W), Antitone (history.metaphysicalBase w)) (hQ : Q.IsEventuality) (h : PRES now (MAY history.metaphysicalBase Q) w) (ht' : t' < now) : StillPresup (MAY history.metaphysicalBase Q) w now

In he may still win, the presupposition of still over a metaphysical possibility is not merely consistent with the shrinking of possibilities, as the paper puts it, but entailed by the assertion, given any earlier time.

Settledness and the diversity condition

def Condoravdi2002.FixesPast {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (history : HistoricalAlternatives W T) (Q : Aspect.SortedProperty W E T) : Prop

The history relation fixes the instantiation of Q at every interval up to its time, so that worlds identical up to t agree on Q there.

Equations

• Condoravdi2002.FixesPast history Q = ∀ (t : T) (w w' : W), w' ∈ history (w, t) → ∀ (r : Interval (WithTop T)), (∀ x ∈ r, x ≤ ↑t) → (Aspect.At r w Q ↔ Aspect.At r w' Q)

theorem Condoravdi2002.fixesPast_eventive {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : FixesPast (Temporal.TWFrame.ofDatedFacts (fun (e : E) => (Event.τ e).toProd.1) P).alternatives (Aspect.SortedProperty.eventive P)

Worlds agreeing on the events that have begun agree on which events lie within an interval of the past.

theorem Condoravdi2002.fixesPast_stative {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : FixesPast (Temporal.TWFrame.ofDatedFacts (fun (e : E) => (Event.τ e).toProd.1) P).alternatives (Aspect.SortedProperty.stative P)

Worlds agreeing on the states that have begun agree on which states overlap an interval of the past.

theorem Condoravdi2002.settled_perf {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {history : HistoricalAlternatives W T} (h : FixesPast history Q) (cg : Set W) (t : T) : history.settled cg t fun (w : W) => Aspect.At (Interval.Ici ↑t) w (PERF Q)

Instantiation in the past of the perspective, the modal over the perfect, is settled in every common ground.

theorem Condoravdi2002.settled_present {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {history : HistoricalAlternatives W T} (h : FixesPast history Q) (cg : Set W) (t : T) : history.settled cg t fun (w : W) => Aspect.At (Interval.Ici ↑t) w (frame (Interval.pure ↑t) Q)

Instantiation at the present, a stative with now, is settled in every common ground, since the forward interval restricted to the present is the present.

theorem Condoravdi2002.not_diverse_of_settled {W : Type u_1} {T : Type u_2} {history : HistoricalAlternatives W T} {cg : Set W} {t : T} {R : W → Prop} (h : history.settled cg t R) : ¬HistoricalAlternatives.diverse history.metaphysicalBase cg t R

A common ground that settles a property fails the diversity condition for the metaphysical base, so a context cannot assign that base to a possibility modal applying to it, and the modal over the perfect and the present-referring stative are epistemic.

The counterfactual implication

def Condoravdi2002.PastAlternativesOutside {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) (cg : Set W) (t₀ : T) : Prop

The paper's footnote assumption says that a past alternative of a common-ground world that is no alternative at the time of utterance lies outside the common ground.

Equations

• Condoravdi2002.PastAlternativesOutside history cg t₀ = ∀ w ∈ cg, ∀ t' ≤ t₀, ∀ w' ∈ history.metaphysicalBase w t', w' ∉ history.metaphysicalBase w t₀ → w' ∉ cg

theorem Condoravdi2002.counterfactual_outside_cg {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : Aspect.SortedProperty W E T} {w : W} {history : HistoricalAlternatives W T} {cg : Set W} {t₀ : T} (h : PastAlternativesOutside history cg t₀) (hw : w ∈ cg) (hcf : PRES t₀ (PERF (MAY history.metaphysicalBase Q)) w) (hnow : ∀ t' < t₀, ∀ w' ∈ history.metaphysicalBase w t₀, ¬Aspect.At (Interval.Ici ↑t') w' Q) : ∃ t' < t₀, ∃ w' ∉ cg, w' ∈ history.metaphysicalBase w t' ∧ Aspect.At (Interval.Ici ↑t') w' Q

The counterfactual implication holds. When no present alternative verifies the past possibility, the world that does lies outside the common ground, which is what the speaker's backtracking to a past perspective signals.

Perspective and orientation

inductive Condoravdi2002.Scope : Type

A Scope is a scoping of a possibility modal with respect to the perfect.

• modal : Scope

  The modal alone, as in he may win.

• modalPerf : Scope

  The modal over the perfect, as in he may have won, the epistemic reading.

• perfModal : Scope

  The perfect over the modal, as in he might have won, the counterfactual reading.

@[instance_reducible]

instance Condoravdi2002.instDecidableEqScope : DecidableEq Scope

Equations

• Condoravdi2002.instDecidableEqScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Condoravdi2002.instFintypeScope : Fintype Scope

Equations

• Condoravdi2002.instFintypeScope = { elems := { val := ↑Condoravdi2002.Scope.enumList, nodup := Condoravdi2002.Scope.enumList_nodup }, complete := Condoravdi2002.instFintypeScope._proof_1 }

def Condoravdi2002.Scope.lf {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (MB : W → T → Set W) : Scope → Aspect.SortedProperty W E T → Aspect.SortedProperty W E T

s.lf is the scoping s as an operator on the property under the modal.

Equations

• Condoravdi2002.Scope.lf MB Condoravdi2002.Scope.modal x✝ = Condoravdi2002.MAY MB x✝
• Condoravdi2002.Scope.lf MB Condoravdi2002.Scope.modalPerf x✝ = Condoravdi2002.MAY MB (Condoravdi2002.PERF x✝)
• Condoravdi2002.Scope.lf MB Condoravdi2002.Scope.perfModal x✝ = Condoravdi2002.PERF (Condoravdi2002.MAY MB x✝)

def Condoravdi2002.Scope.perspective : Scope → Modality.TemporalPerspective

s.perspective is the time at which the modal base is evaluated, read off the three readings, the present in pres_may_eventive_iff and pres_may_perf_eventive_iff, the past time the perfect supplies in pres_perf_may_eventive_iff.

Equations

• Condoravdi2002.Scope.modal.perspective = Modality.TemporalPerspective.present
• Condoravdi2002.Scope.modalPerf.perspective = Modality.TemporalPerspective.present
• Condoravdi2002.Scope.perfModal.perspective = Modality.TemporalPerspective.past

def Condoravdi2002.Scope.orientation : Scope → Modality.TemporalOrientation

s.orientation is the direction of the instantiation from the perspective, read off the three readings, where the event starts no earlier than the perspective, or ends before it.

Equations

• Condoravdi2002.Scope.modal.orientation = Modality.TemporalOrientation.future
• Condoravdi2002.Scope.perfModal.orientation = Modality.TemporalOrientation.future
• Condoravdi2002.Scope.modalPerf.orientation = Modality.TemporalOrientation.past

theorem Condoravdi2002.Scope.orientation_of_perspective_past (s : Scope) : s.perspective = Modality.TemporalPerspective.past → s.orientation = Modality.TemporalOrientation.future

A past perspective comes with a future orientation, the empty cell of the paper's table.

A model

def Condoravdi2002.winOn (d : ℤ) : Unit → NonemptyInterval ℤ → Prop

winOn d is the predicate of a winning on day d, in a one-world model over integer days.

Equations

• Condoravdi2002.winOn d x✝ e = (e = NonemptyInterval.pure d)

def Condoravdi2002.anyWorld : Unit → ℤ → Set Unit

The unrestricted modal base admits every world.

Equations

• Condoravdi2002.anyWorld x✝¹ x✝ = Set.univ

inductive Condoravdi2002.Zone : Type

A Zone says where a period sits relative to the present.

• past : Zone
• present : Zone
• future : Zone

@[instance_reducible]

instance Condoravdi2002.instDecidableEqZone : DecidableEq Zone

Equations

• Condoravdi2002.instDecidableEqZone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Condoravdi2002.Zone.day : Zone → ℤ

z.day is the day the zone z names, the utterance being on day 0.

Equations

• Condoravdi2002.Zone.past.day = -1
• Condoravdi2002.Zone.present.day = 0
• Condoravdi2002.Zone.future.day = 1

def Condoravdi2002.Zone.period (z : Zone) : Interval (WithTop ℤ)

The period a zone names is its day.

Equations

• z.period = Interval.pure ↑z.day

def Condoravdi2002.Scope.zones : Scope → Finset Zone

s.zones are the zones the reference interval of the scoping s reaches, the forward interval of the present, the intervals before it, or the forward interval of a past time.

Equations

• Condoravdi2002.Scope.modal.zones = {Condoravdi2002.Zone.present, Condoravdi2002.Zone.future}
• Condoravdi2002.Scope.modalPerf.zones = {Condoravdi2002.Zone.past}
• Condoravdi2002.Scope.perfModal.zones = {Condoravdi2002.Zone.past, Condoravdi2002.Zone.present, Condoravdi2002.Zone.future}

def Condoravdi2002.Scope.Sat (s : Scope) (z : Zone) : Prop

In the model, the scoping's sentence about a winning on the zone's day, framed by that day and uttered on day 0, is true.

Equations

• s.Sat z = Condoravdi2002.PRES 0 (Condoravdi2002.Scope.lf Condoravdi2002.anyWorld s (Condoravdi2002.frame z.period (Aspect.SortedProperty.eventive (Condoravdi2002.winOn z.day)))) ()

theorem Condoravdi2002.zones_iff (s : Scope) (z : Zone) : z ∈ s.zones ↔ s.Sat z

The zone table is the satisfiability table, since a scoping admits a period exactly when its sentence about that period can be true, the deviant cells being frame_modal_past and frame_modalPerf_nonpast, the others witnessed.

The rows

def Condoravdi2002.scopes : List (String × Scope)

Equations

• Condoravdi2002.scopes = [("modal", Condoravdi2002.Scope.modal), ("modalPerf", Condoravdi2002.Scope.modalPerf), ("perfModal", Condoravdi2002.Scope.perfModal)]

structure Condoravdi2002.Adverbial : Type

An adverbial row records the scoping, the sort of the predicate, and the zone of the frame adverbial.

• scope : Scope

  The scoping.

• sort : Aspect.Dynamicity

  The sort of the predicate.

• zone : Zone

  The zone of the period.

def Condoravdi2002.Adverbial.ofRow (row : Datum) : Option Adverbial

Adverbial.ofRow row is the configuration that the adverbial row row records.

Equations

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

theorem Condoravdi2002.adverb_rows (row : Datum) : row ∈ Examples.all → ∀ a ∈ Adverbial.ofRow row, (row.judgment = Judgment.ungrammatical ↔ a.zone ∉ a.scope.zones) ∧ (row.judgment = Judgment.questionable ↔ a.scope = Scope.modal ∧ a.sort = Aspect.Dynamicity.dynamic ∧ a.zone = Zone.present)

In the adverbial patterns of [1], [2], [29], [34] and [35], a frame adverbial is deviant exactly when its zone lies outside the scoping's satisfiable cells, zones_iff; the one questionable row is the eventive predicate with now under a modal for the present, which the semantics admits by an event within the present.

inductive Condoravdi2002.Context : Type

A Context records what the context says about the issue.

• settled : Context
• unsettled : Context
• absent : Context

@[instance_reducible]

instance Condoravdi2002.instDecidableEqContext : DecidableEq Context

Equations

• Condoravdi2002.instDecidableEqContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Condoravdi2002.Reading : Type

A reading row records the scoping, the zone the instantiation refers to, and the context.

• scope : Scope

  The scoping.

• reference : Zone

  The zone referred to, the present for a stative with now.

• context : Context

  What the context says about the issue.

def Condoravdi2002.Reading.ofRow (row : Datum) : Option (Reading × Bool)

Reading.ofRow row is the configuration that the reading row row records, and whether the paper finds the metaphysical reading available.

Equations

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

def Condoravdi2002.Reading.Metaphysical (r : Reading) : Prop

The metaphysical base is assignable when the instantiation is neither in the past of the perspective, settled_perf, nor at the present, settled_present, nor settled by the context.

Equations

• r.Metaphysical = (r.scope ≠ Condoravdi2002.Scope.modalPerf ∧ r.reference ≠ Condoravdi2002.Zone.present ∧ r.context ≠ Condoravdi2002.Context.settled)

@[instance_reducible]

instance Condoravdi2002.instDecidableMetaphysical (r : Reading) : Decidable r.Metaphysical

Equations

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

theorem Condoravdi2002.reading_rows (row : Datum) : row ∈ Examples.all → ∀ p ∈ Reading.ofRow row, p.2 = true ↔ p.1.Metaphysical

In the readings of [6], [7], [41] and [42], the metaphysical reading is available exactly where settledness is not guaranteed.

inductive Condoravdi2002.Complement : Type

A Complement is the complement that a phase adverb applies to.

• eventive : Complement
• perfect : Complement

@[instance_reducible]

instance Condoravdi2002.instDecidableEqComplement : DecidableEq Complement

Equations

• Condoravdi2002.instDecidableEqComplement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Condoravdi2002.Complement.property : Complement → Aspect.SortedProperty Unit (NonemptyInterval Unit) Unit

c.property is a representative property of the sort of the complement c.

Equations

• Condoravdi2002.Complement.eventive.property = Aspect.SortedProperty.eventive fun (x : Unit) (x_1 : NonemptyInterval Unit) => True
• Condoravdi2002.Complement.perfect.property = Condoravdi2002.PERF (Aspect.SortedProperty.eventive fun (x : Unit) (x_1 : NonemptyInterval Unit) => True)

def Condoravdi2002.Complement.ofRow (row : Datum) : Option Complement

A sortal row records the complement of already or yet.

Equations

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

theorem Condoravdi2002.sortal_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ Complement.ofRow row, row.judgment = Judgment.acceptable ↔ (phase c.property).isSome = true

By the sortal restriction of [14] and [15], already and yet are acceptable exactly on the complements where phase is defined, the perfect of an eventive predicate among them.

inductive Condoravdi2002.Phase : Type

A Phase is one of the phase adverbs.

• already : Phase
• still : Phase

@[instance_reducible]

instance Condoravdi2002.instDecidableEqPhase : DecidableEq Phase

Equations

• Condoravdi2002.instDecidableEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Condoravdi2002.Phase.ofRow (row : Datum) : Option Phase

A phase row records the adverb scoping over the possibility modal.

Equations

• Condoravdi2002.Phase.ofRow row = do guard (row.feature? "construction" = some "phase") row.parse? "adverb" [("already", Condoravdi2002.Phase.already), ("still", Condoravdi2002.Phase.still)]

theorem Condoravdi2002.phase_rows (row : Datum) : row ∈ Examples.all → ∀ p ∈ Phase.ofRow row, row.judgment = Judgment.acceptable ↔ p = Phase.still

In the scopings of [36], [37] and [40], still over a possibility modal is acceptable and already is not, still_may and not_already_may.

inductive Condoravdi2002.Order : Type

An Order is one of the German orders of the modal and the perfect auxiliary, which mirror scope.

• modalHave : Order

  Könnte ... haben puts the modal over the perfect.

• hadModal : Order

  Hätte ... können puts the perfect over the modal.

@[instance_reducible]

instance Condoravdi2002.instDecidableEqOrder : DecidableEq Order

Equations

• Condoravdi2002.instDecidableEqOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Condoravdi2002.Phase.order : Phase → Order

p.order is the order that the presuppositions of the adverb p require, schon the modal over already over the perfect, since already can scope neither over a possibility modal, not_already_may, nor under it on an eventive radical, phase; noch the perfect over still over the modal, on the paper's exclusion of still over the perfect.

Equations

• Condoravdi2002.Phase.already.order = Condoravdi2002.Order.modalHave
• Condoravdi2002.Phase.still.order = Condoravdi2002.Order.hadModal

def Condoravdi2002.Order.ofRow (row : Datum) : Option (Order × Phase)

A German row records the order and the adverb.

Equations

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

theorem Condoravdi2002.german_rows (row : Datum) : row ∈ Examples.all → ∀ p ∈ Order.ofRow row, row.judgment = Judgment.acceptable ↔ p.1 = p.2.order

The German pattern [38] is acceptable exactly when the syntax realizes the order the adverb requires.