From 37d409d4719d2becbf66281df9a83c343a152795 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Sat, 30 May 2026 13:04:15 -0700 Subject: [PATCH] refactor(Semantics/Events): root-namespace Event, sort via Dynamicity --- Linglib.lean | 1 + Linglib/Features/Aktionsart.lean | 2 +- .../Slavic/Serbian/TemporalConnectives.lean | 1 - .../Tagalog/TemporalConnectives.lean | 1 - .../ArgumentIntroduction.lean | 212 ++++++++ Linglib/Semantics/ArgumentStructure/Defs.lean | 1 - Linglib/Semantics/ArgumentStructure/LF.lean | 19 +- Linglib/Semantics/Aspect/Basic.lean | 49 +- Linglib/Semantics/Aspect/Stratified.lean | 1 - .../Semantics/Aspect/SubeventStructure.lean | 16 +- .../Semantics/Aspect/SubintervalProperty.lean | 463 +++++++++--------- .../Semantics/Attitudes/RationalAttitude.lean | 12 +- Linglib/Semantics/Causation/PsychLink.lean | 33 +- Linglib/Semantics/Degree/MeasureFunction.lean | 1 - Linglib/Semantics/Events/Adjacency.lean | 4 - Linglib/Semantics/Events/Basic.lean | 65 +-- Linglib/Semantics/Events/CEM.lean | 11 +- Linglib/Semantics/Events/Defs.lean | 71 +-- .../Semantics/Quotation/Demonstration.lean | 1 - Linglib/Semantics/Spatial/Trace.lean | 1 - .../Semantics/Tense/SOT/Decomposition.lean | 5 +- .../Semantics/Tense/TemporalAdverbials.lean | 5 +- .../Tense/TemporalConnectives/Basic.lean | 2 +- .../TemporalConnectives/EventBridge.lean | 11 +- .../Tense/TenseAspectComposition.lean | 33 +- Linglib/Studies/Anscombe1964.lean | 43 +- Linglib/Studies/Bhadra2024.lean | 13 +- .../Studies/CarianiSantorioWellwood2024.lean | 6 +- Linglib/Studies/Condoravdi2002.lean | 53 +- Linglib/Studies/Cruse1973.lean | 9 +- Linglib/Studies/Giannakidou2002.lean | 59 ++- Linglib/Studies/IatridouZeijlstra2021.lean | 21 +- Linglib/Studies/KennedyLevin2008.lean | 1 - Linglib/Studies/Kiparsky2002.lean | 5 +- Linglib/Studies/Koev2017.lean | 9 +- Linglib/Studies/Krifka1998.lean | 3 - Linglib/Studies/OgiharaST2024.lean | 37 +- Linglib/Studies/Pasternak2019.lean | 24 +- Linglib/Studies/Pylkkanen2008.lean | 123 ++++- Linglib/Studies/Rouillard2026.lean | 17 +- Linglib/Studies/Rudin2025LI.lean | 3 +- Linglib/Studies/Wellwood2015.lean | 13 +- blog/references.bib | 27 + 43 files changed, 847 insertions(+), 640 deletions(-) create mode 100644 Linglib/Semantics/ArgumentStructure/ArgumentIntroduction.lean diff --git a/Linglib.lean b/Linglib.lean index 260fe69bd..108374d9e 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -2344,6 +2344,7 @@ import Linglib.Studies.Krifka2004 import Linglib.Semantics.Kinds.Subkinds import Linglib.Semantics.Homogeneity.Basic import Linglib.Semantics.ArgumentStructure.Relational +import Linglib.Semantics.ArgumentStructure.ArgumentIntroduction import Linglib.Semantics.Plurality.Algebra import Linglib.Semantics.Plurality.Basic import Linglib.Semantics.Plurality.Cover diff --git a/Linglib/Features/Aktionsart.lean b/Linglib/Features/Aktionsart.lean index 4cf61db9d..a48c2ce86 100644 --- a/Linglib/Features/Aktionsart.lean +++ b/Linglib/Features/Aktionsart.lean @@ -27,7 +27,7 @@ The CUM/QUA/DIV algebra over event predicates lives in `Telicity` here is the Smith-flavored derived label. Sibling formalizations of competitor lexical-aspect frameworks: -@cite{bach-1986} `EventSort` in `Semantics/Events/Basic.lean`; +@cite{bach-1986}; the event-token sort is this `Dynamicity` feature (`Event.sort`); @cite{krifka-1989}/@cite{krifka-1998} CUM/QUA/DIV in `Semantics/Events/CEM.lean`; @cite{dowty-1979} SIP in `Semantics/Tense/Aspect/SubintervalProperty.lean`; diff --git a/Linglib/Fragments/Slavic/Serbian/TemporalConnectives.lean b/Linglib/Fragments/Slavic/Serbian/TemporalConnectives.lean index a8b9565cc..d1e0ddf7e 100644 --- a/Linglib/Fragments/Slavic/Serbian/TemporalConnectives.lean +++ b/Linglib/Fragments/Slavic/Serbian/TemporalConnectives.lean @@ -26,7 +26,6 @@ PFV/IMPF opposition rather than Tagalog's finer-grained system. namespace Fragments.Slavic.Serbian.TemporalConnectives -open Semantics.Events open Semantics.Aspect open Fragments.English.TemporalExpressions (Reading TemporalExprEntry ComplementType) diff --git a/Linglib/Fragments/Tagalog/TemporalConnectives.lean b/Linglib/Fragments/Tagalog/TemporalConnectives.lean index 876731e2a..19b438f7d 100644 --- a/Linglib/Fragments/Tagalog/TemporalConnectives.lean +++ b/Linglib/Fragments/Tagalog/TemporalConnectives.lean @@ -22,7 +22,6 @@ overt aspect markers in Tagalog. namespace Fragments.Tagalog.TemporalConnectives -open Semantics.Events open Semantics.Aspect open Fragments.English.TemporalExpressions (Reading TemporalExprEntry ComplementType) diff --git a/Linglib/Semantics/ArgumentStructure/ArgumentIntroduction.lean b/Linglib/Semantics/ArgumentStructure/ArgumentIntroduction.lean new file mode 100644 index 000000000..1685970cd --- /dev/null +++ b/Linglib/Semantics/ArgumentStructure/ArgumentIntroduction.lean @@ -0,0 +1,212 @@ +import Linglib.Semantics.ArgumentStructure.Defs + +/-! +# Argument Introduction by Functional Heads + +@cite{kratzer-1996} @cite{pylkkanen-2008} @cite{wood-marantz-2017} +@cite{parsons-1990} @cite{moltmann-2025} @cite{hopperdietzel-2024} + +Neo-Davidsonian substrate for argument-introducing heads (Voice, applicative, +Cause), built on the canonical `ThematicRel` (`Entity → Event Time → Prop`, +@cite{moltmann-2025}: "the preferred version of event semantics for +syntacticians"). A verb/VP denotation is a predicate of events +`Event Time → Prop` (this is `Set (Event Time)`; used predicatively). + +The central new object is `VerbDenot`: a verb denotation classified by the +structure argument introduction is sensitive to (valence). @cite{pylkkanen-2008}'s +high/low contrast is the `IntroMode` parameter — whether the introduced +participant is related to the *event* (high applicative / Voice, via Event +Identification) or to the verb's internal *theme* (low applicative, via a +transfer relation). The transitivity restriction then falls out of the +denotations' types rather than being stipulated, and @cite{wood-marantz-2017}'s +contextually-interpreted single argument-introducer is its `IntroMode` reading. + +## Main definitions + +* `eventIdentification` — @cite{kratzer-1996}'s Event Identification combinator +* `RolesExclusive` — thematic uniqueness (the principle behind eq. 103) +* `VerbDenot` — verb denotation classified by valence +* `IntroMode` / `IntroMode.Licenses` — high/low introduction and its licensing +* `applToEvent` / `applToTheme` — the high / low applicative denotations +* `causeBieventive` / `causeThetaRole` — the §3.2 Cause-is-not-a-θ-role contrast +-/ + +namespace Semantics.ArgumentStructure + +variable {Entity : Type*} {Time : Type*} [LinearOrder Time] + +/-! ### Event Identification and thematic uniqueness -/ + +/-- Event Identification (@cite{kratzer-1996}): combine an argument-introducer +`f` (a thematic relation, awaiting its participant) with a VP predicate `g`, +conjoining at the event. The result still awaits the introduced participant. -/ +def eventIdentification (f : ThematicRel Entity Time) (g : Event Time → Prop) : + ThematicRel Entity Time := + fun x e => f x e ∧ g e + +theorem eventIdentification_apply (f : ThematicRel Entity Time) + (g : Event Time → Prop) (x : Entity) (e : Event Time) : + eventIdentification f g x e ↔ f x e ∧ g e := Iff.rfl + +/-- Two thematic relations are role-exclusive when no participant bears both to +the same event (thematic uniqueness). This is the principle behind +@cite{pylkkanen-2008}'s eq. 103: a participant cannot be both agent and theme. -/ +def RolesExclusive (r₁ r₂ : ThematicRel Entity Time) : Prop := + ∀ x e, r₁ x e → ¬ r₂ x e + +/-! ### Verb denotations classified by valence -/ + +/-- A verb/VP denotation, classified by the structure argument introduction is +sensitive to. The valence distinction is a genuine *type* difference, which is +why @cite{pylkkanen-2008}'s transitivity restriction is a fact about this type +rather than a stipulation. + +* `unergative` — a saturated event predicate, no internal-argument slot + (e.g. *run*). [Diagnostic 1 target] +* `transitive` — awaits its internal theme argument, carrying a theme relation + (e.g. *send a letter*). +* `kimianStative` — a relation over individuals with *no* event argument + (Kimian state, @cite{moltmann-2025} §1.4.1; e.g. *own*, *owe*). [Diagnostic 2] -/ +inductive VerbDenot (Entity : Type*) (Time : Type*) [LinearOrder Time] where + | unergative (body : Event Time → Prop) + | transitive (theme : ThematicRel Entity Time) (body : ThematicRel Entity Time) + | kimianStative (rel : Entity → Entity → Prop) + +namespace VerbDenot + +/-- Does this denotation supply an event-internal theme (Davidsonian transitive)? +`unergative` (no participant slot) and `kimianStative` (no event argument) lack +one, for two distinct structural reasons. -/ +def IsTransitive : VerbDenot Entity Time → Prop + | .transitive _ _ => True + | _ => False + +instance : DecidablePred (IsTransitive (Entity := Entity) (Time := Time)) := fun vd => + match vd with + | .transitive _ _ => .isTrue trivial + | .unergative _ => .isFalse id + | .kimianStative _ => .isFalse id + +end VerbDenot + +/-! ### Introduction mode and licensing -/ + +/-- The semantic mode of an argument introducer: whether it relates the +introduced participant to the *event* (high applicative / Voice, via Event +Identification) or to the verb's internal *theme* (low applicative, via a +transfer relation). This is @cite{pylkkanen-2008}'s high/low contrast at the +denotational level, and @cite{wood-marantz-2017}'s contextually-interpreted +single argument-introducer. -/ +inductive IntroMode where + | toEvent -- high applicative / Voice + | toTheme -- low applicative + deriving DecidableEq, Repr + +/-- Which verb denotations an introducer of this mode can compose with, derived +from the denotation's valence: an event-relating introducer composes with +anything; a theme-relating one needs an event-internal theme. -/ +def IntroMode.Licenses : IntroMode → VerbDenot Entity Time → Prop + | .toEvent, _ => True + | .toTheme, vd => vd.IsTransitive + +instance (m : IntroMode) : + DecidablePred (IntroMode.Licenses m (Entity := Entity) (Time := Time)) := fun vd => by + cases m <;> unfold IntroMode.Licenses <;> infer_instance + +/-! ### Applicative denotations -/ + +/-- High applicative / Voice denotation: introduce a participant related to the +EVENT, via Event Identification. Total over any VP predicate — so it composes +with unergatives. -/ +def applToEvent (rel : ThematicRel Entity Time) (vp : Event Time → Prop) : + ThematicRel Entity Time := + eventIdentification rel vp + +/-- Low applicative denotation: relate the applied argument to the THEME of a +transitive verb via a transfer relation. Requires the verb's internal theme +function `ThematicRel Entity Time` (type ⟨e,⟨s,t⟩⟩) — an unergative or Kimian +state cannot supply it. -/ +def applToTheme (themeRel : ThematicRel Entity Time) + (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time) + (theme applied : Entity) : Event Time → Prop := + fun e => verb theme e ∧ themeRel theme e ∧ transfer theme applied + +/-- Any low-applicative denotation entails the theme bears the theme relation — +the theme conjunct is present by construction. -/ +theorem applToTheme_entails_theme (themeRel : ThematicRel Entity Time) + (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time) + (theme applied : Entity) (e : Event Time) + (h : applToTheme themeRel transfer verb theme applied e) : themeRel theme e := + h.2.1 + +/-! ### The transitivity restriction, derived -/ + +/-- High introduction licenses any verb, including unergatives (Luganda/Venda/ +Albanian high applicatives over unergatives, @cite{pylkkanen-2008} §2.1.2). -/ +theorem toEvent_licenses_all (vd : VerbDenot Entity Time) : + IntroMode.toEvent.Licenses vd := trivial + +/-- Diagnostic 1: low (theme-relating) introduction is blocked over an +unergative — it has no event-internal theme. Derived from the valence type, +not stipulated. -/ +theorem toTheme_blocks_unergative (body : Event Time → Prop) : + ¬ IntroMode.toTheme.Licenses (VerbDenot.unergative (Entity := Entity) body) := + id + +/-- Diagnostic 2: low introduction is blocked over a Kimian stative — distinct +reason from Diagnostic 1: no event argument at all (@cite{moltmann-2025}). -/ +theorem toTheme_blocks_kimian (rel : Entity → Entity → Prop) : + ¬ IntroMode.toTheme.Licenses (VerbDenot.kimianStative (Time := Time) rel) := + id + +/-- Low introduction is licensed over a Davidsonian transitive (English DOC, +Hebrew possessor datives). -/ +theorem toTheme_licenses_transitive (themeRel body : ThematicRel Entity Time) : + IntroMode.toTheme.Licenses (VerbDenot.transitive themeRel body) := trivial + +/-- @cite{pylkkanen-2008}'s eq. 103, as a theorem about the denotations: +forcing a low (theme-relating) applicative onto an unergative binds the applied +argument's theme relation to the external argument, yielding `agentRel x e ∧ +themeRel x e` for one participant — contradictory under thematic uniqueness. +The transitivity restriction is thus *derived*, not stipulated. -/ +theorem low_external_arg_clash + (agentRel themeRel : ThematicRel Entity Time) + (excl : RolesExclusive agentRel themeRel) + (x : Entity) (e : Event Time) + (hAgent : agentRel x e) (hTheme : themeRel x e) : False := + excl x e hAgent hTheme + +/-! ### Cause is not a θ-role (@cite{pylkkanen-2008} Ch. 3 §3.2) -/ + +/-- Bieventive Cause: the causative head relates the described event to a +causing event, introducing NO individual. `λf.λe. ∃e'. f e' ∧ cause e e'`. -/ +def causeBieventive (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) : + Event Time → Prop := + fun e => ∃ e', caused e' ∧ cause e e' + +/-- The θ-role analysis @cite{pylkkanen-2008} argues against: Cause introduces a +causer individual. `λx.λe. causer x e ∧ ∃e'. f e' ∧ cause e e'`. -/ +def causeThetaRole (cause : Event Time → Event Time → Prop) + (causer : ThematicRel Entity Time) (caused : Event Time → Prop) : + ThematicRel Entity Time := + fun x e => causer x e ∧ ∃ e', caused e' ∧ cause e e' + +/-- The θ-role analysis forces an external (causer) participant: its denotation +entails `causer x e`. -/ +theorem causeThetaRole_forces_causer (cause : Event Time → Event Time → Prop) + (causer : ThematicRel Entity Time) (caused : Event Time → Prop) + (x : Entity) (e : Event Time) + (h : causeThetaRole cause causer caused x e) : causer x e := + h.1 + +/-- The bieventive analysis admits a causative event with NO external +participant: given only a causing relation to some caused event, +`causeBieventive` holds without any causer. This is the Japanese adversity +causative (@cite{pylkkanen-2008} §3.2.2) the θ-role analysis cannot model. -/ +theorem causeBieventive_no_external_arg + (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) + (e e' : Event Time) (hc : caused e') (hcause : cause e e') : + causeBieventive cause caused e := + ⟨e', hc, hcause⟩ + +end Semantics.ArgumentStructure diff --git a/Linglib/Semantics/ArgumentStructure/Defs.lean b/Linglib/Semantics/ArgumentStructure/Defs.lean index dd270a3a9..3edf683f5 100644 --- a/Linglib/Semantics/ArgumentStructure/Defs.lean +++ b/Linglib/Semantics/ArgumentStructure/Defs.lean @@ -28,7 +28,6 @@ type/structure declarations and the Fragment ↔ Theory bridge. namespace Semantics.ArgumentStructure -open Semantics.Events open Core.Time /-- A thematic relation: a two-place predicate relating an entity to an event. diff --git a/Linglib/Semantics/ArgumentStructure/LF.lean b/Linglib/Semantics/ArgumentStructure/LF.lean index e25dc4607..3ccbe5953 100644 --- a/Linglib/Semantics/ArgumentStructure/LF.lean +++ b/Linglib/Semantics/ArgumentStructure/LF.lean @@ -26,7 +26,6 @@ forms, and adverbial modification (Davidson's key payoff). namespace Semantics.ArgumentStructure -open Semantics.Events open Core.Time /-! ### Thematic axioms (Aktionsart selection + uniqueness) -/ @@ -41,10 +40,10 @@ class ThematicAxioms (Entity Time : Type*) [LinearOrder Time] (frame : ThematicFrame Entity Time) where /-- Agents only participate in actions (dynamic events). -/ agent_selects_action : ∀ (x : Entity) (e : Event Time), - frame.agent x e → e.sort = .action + frame.agent x e → e.sort = .dynamic /-- Holders only participate in states. -/ holder_selects_state : ∀ (x : Entity) (e : Event Time), - frame.holder x e → e.sort = .state + frame.holder x e → e.sort = .stative /-- Each event has at most one agent. -/ agent_unique : ∀ (x y : Entity) (e : Event Time), frame.agent x e → frame.agent y e → x = y @@ -67,19 +66,19 @@ theorem agent_holder_disjoint {Entity Time : Type*} [LinearOrder Time] /-! ### Adverbial modification (Davidson's key payoff) -/ /-- An event modifier: a predicate on events (e.g., "quickly", "in the park"). -/ -abbrev EventModifier (Time : Type*) [LinearOrder Time] := EvPred Time +abbrev EventModifier (Time : Type*) [LinearOrder Time] := Event Time → Prop /-- Apply a modifier to an event predicate via conjunction. @cite{davidson-1967}: adverbial modification is conjunction of event predicates. "John kicked the ball quickly" = ∃e. kick(e) ∧ Agent(j,e) ∧ Patient(b,e) ∧ quickly(e). -/ def modify {Time : Type*} [LinearOrder Time] - (P : EvPred Time) (M : EventModifier Time) : EvPred Time := + (P : Event Time → Prop) (M : EventModifier Time) : Event Time → Prop := λ e => P e ∧ M e /-- Modification is commutative: "quickly and loudly" = "loudly and quickly". -/ theorem modify_comm {Time : Type*} [LinearOrder Time] - (P : EvPred Time) (M₁ M₂ : EventModifier Time) : + (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify (modify P M₂) M₁ := by funext e simp only [modify] @@ -88,7 +87,7 @@ theorem modify_comm {Time : Type*} [LinearOrder Time] /-- Modification is associative. -/ theorem modify_assoc {Time : Type*} [LinearOrder Time] - (P : EvPred Time) (M₁ M₂ : EventModifier Time) : + (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify P (λ e => M₁ e ∧ M₂ e) := by funext e simp only [modify] @@ -101,14 +100,14 @@ theorem modify_assoc {Time : Type*} [LinearOrder Time] `intransitiveLogicalForm` but using `holder` instead of `agent`, reflecting that states select for holders. -/ def stativeLogicalForm {Entity Time : Type*} [LinearOrder Time] - (P : EvPred Time) (frame : ThematicFrame Entity Time) + (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) : Prop := ∃ s : Event Time, P s ∧ frame.holder x s /-- "x is happy in the morning" ↦ ∃s. P(s) ∧ Holder(x, s) ∧ M(s). State modification = event modification applied to states. -/ def modifiedStativeLogicalForm {Entity Time : Type*} [LinearOrder Time] - (P : EvPred Time) (frame : ThematicFrame Entity Time) + (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : Prop := ∃ s : Event Time, P s ∧ frame.holder x s ∧ M s @@ -116,7 +115,7 @@ def modifiedStativeLogicalForm {Entity Time : Type*} [LinearOrder Time] state modification is an instance of Davidson's conjunction-based event modification. -/ theorem modified_stative_is_pm {Entity Time : Type*} [LinearOrder Time] - (P : EvPred Time) (frame : ThematicFrame Entity Time) + (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : modifiedStativeLogicalForm P frame x M ↔ stativeLogicalForm (modify P M) frame x := by diff --git a/Linglib/Semantics/Aspect/Basic.lean b/Linglib/Semantics/Aspect/Basic.lean index 6157f0c7f..21a8a8098 100644 --- a/Linglib/Semantics/Aspect/Basic.lean +++ b/Linglib/Semantics/Aspect/Basic.lean @@ -17,7 +17,7 @@ following @cite{knick-sharf-2026}. ## Compositional Architecture ``` -EventPred ──[IMPF/PRFV]──▷ IntervalPred ──[PERF]──▷ PointPred ──[TENSE]──▷ Prop +Event Time → Prop ──[IMPF/PRFV]──▷ IntervalPred ──[PERF]──▷ PointPred ──[TENSE]──▷ Prop ``` Equations (verified against the @cite{knick-sharf-2026} proceedings PDF): @@ -60,7 +60,6 @@ namespace Semantics.Aspect open _root_.Core (WorldTimeIndex) open Core.Time open Features -open Semantics.Events -- ════════════════════════════════════════════════════ -- § Core Types @@ -68,7 +67,7 @@ open Semantics.Events /-! Event predicates and the `Event` type are imported from `Semantics/Events/Basic.lean` — the unified event ontology. - Tense-aspect code uses `Event Time` and `EventPred W Time` without + Tense-aspect code uses `Event Time` and `W → Event Time → Prop` without referencing `.sort` (the field exists for Krifka-style consumers but is irrelevant for Klein-style tense composition). -/ @@ -97,7 +96,7 @@ inductive ViewpointType where deriving DecidableEq, Repr, Inhabited /-- Bool-level viewpoint aspect, capturing the perfective/imperfective distinction - without the full interval-based `EventPred`/`IntervalPred` machinery. + without the full interval-based `Event Time → Prop`/`IntervalPred` machinery. Used by `Modal/Ability.lean` (actuality inferences) and `Phenomena/ActualityInferences/Data.lean` where the key insight is simply @@ -141,18 +140,18 @@ variable {Time : Type*} [LinearOrder Time] {W : Type*} /-- **IMPERFECTIVE**: reference time properly contained in event runtime. @cite{klein-1994}: TT INCL TSit. @cite{knick-sharf-2026} eq. 25. -/ -def IMPF (P : EventPred W Time) : IntervalPred W Time := +def IMPF (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, t.properSubinterval e.τ ∧ P w e /-- **PERFECTIVE**: event runtime contained in reference time. @cite{klein-1994}: TT AT TSit (simplified to TSit ⊆ TT, following @cite{smith-1997}). @cite{knick-sharf-2026} eq. 28. -/ -def PRFV (P : EventPred W Time) : IntervalPred W Time := +def PRFV (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, e.τ.subinterval t ∧ P w e /-- **PROSPECTIVE**: reference time before situation time. @cite{klein-1994}: TT BEFORE TSit. -/ -def PROSP (P : EventPred W Time) : IntervalPred W Time := +def PROSP (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, t.isBefore e.τ ∧ P w e /-- **INIT_OVERLAP**: initial overlap between reference time and event runtime. @@ -164,7 +163,7 @@ def PROSP (P : EventPred W Time) : IntervalPred W Time := neutral viewpoint (`ViewpointType.neutral`), which is a different concept. Pancheva's operator is an inner Asp₂ head; Smith's neutral viewpoint is a default viewpoint type. -/ -def INIT_OVERLAP (P : EventPred W Time) : IntervalPred W Time := +def INIT_OVERLAP (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, t.initialOverlap e.τ ∧ P w e @@ -221,12 +220,12 @@ def PERF_XN (p : IntervalPred W Time) (tᵣ : Set Time) : PointPred W Time := -- ════════════════════════════════════════════════════ /-- IMPF matches Klein's IMPERFECTIVE: ∃e where TT ⊂ TSit. -/ -theorem impf_is_klein_imperfective (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem impf_is_klein_imperfective (P : W → Event Time → Prop) (w : W) (t : Interval Time) : IMPF P w t ↔ ∃ e, ViewpointType.ttTSitRelation .imperfective t e.τ ∧ P w e := by simp only [IMPF, ViewpointType.ttTSitRelation, Event.τ] /-- PRFV matches Klein's PERFECTIVE: ∃e where TSit ⊆ TT. -/ -theorem prfv_is_klein_perfective (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem prfv_is_klein_perfective (P : W → Event Time → Prop) (w : W) (t : Interval Time) : PRFV P w t ↔ ∃ e, ViewpointType.ttTSitRelation .perfective t e.τ ∧ P w e := by simp only [PRFV, ViewpointType.ttTSitRelation, Event.τ] @@ -235,16 +234,16 @@ theorem prfv_is_klein_perfective (P : EventPred W Time) (w : W) (t : Interval Ti -- ════════════════════════════════════════════════════ /-- "has been V-ing" = PERF(IMPF(V)). -/ -abbrev perfProg (P : EventPred W Time) : PointPred W Time := +abbrev perfProg (P : W → Event Time → Prop) : PointPred W Time := PERF (IMPF P) /-- "has V-ed" = PERF(PRFV(V)). -/ -abbrev perfSimple (P : EventPred W Time) : PointPred W Time := +abbrev perfSimple (P : W → Event Time → Prop) : PointPred W Time := PERF (PRFV P) /-- PERF(IMPF(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the PTS properly inside the event, and P holds of the event. -/ -theorem perf_impf_unfold (P : EventPred W Time) (w : W) (t : Time) : +theorem perf_impf_unfold (P : W → Event Time → Prop) (w : W) (t : Time) : perfProg P ⟨w, t⟩ ↔ ∃ pts : Interval Time, ∃ e : Event Time, RB pts t ∧ pts.properSubinterval e.τ ∧ P w e := by @@ -256,7 +255,7 @@ theorem perf_impf_unfold (P : EventPred W Time) (w : W) (t : Time) : /-- PERF(PRFV(P)) unfolds: ∃ PTS and event, with PTS right-bounded at t, the event inside the PTS, and P holds of the event. -/ -theorem perf_prfv_unfold (P : EventPred W Time) (w : W) (t : Time) : +theorem perf_prfv_unfold (P : W → Event Time → Prop) (w : W) (t : Time) : perfSimple P ⟨w, t⟩ ↔ ∃ pts : Interval Time, ∃ e : Event Time, RB pts t ∧ e.τ.subinterval pts ∧ P w e := by @@ -297,12 +296,12 @@ theorem perf_xn_monotone (p : IntervalPred W Time) (tᵣ₁ tᵣ₂ : Set Time) -- ════════════════════════════════════════════════════ /-- IMPF entails an event exists. -/ -theorem impf_entails_event (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem impf_entails_event (P : W → Event Time → Prop) (w : W) (t : Interval Time) : IMPF P w t → ∃ e, P w e := λ ⟨e, _, hP⟩ => ⟨e, hP⟩ /-- PRFV entails an event exists. -/ -theorem prfv_entails_event (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem prfv_entails_event (P : W → Event Time → Prop) (w : W) (t : Interval Time) : PRFV P w t → ∃ e, P w e := λ ⟨e, _, hP⟩ => ⟨e, hP⟩ @@ -314,7 +313,7 @@ theorem perf_monotone (p q : IntervalPred W Time) /-- IMPF and PRFV impose opposite containment directions. IMPF: reference ⊂ event runtime. PRFV: event runtime ⊆ reference. -/ -theorem impf_prfv_opposite_containment (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem impf_prfv_opposite_containment (P : W → Event Time → Prop) (w : W) (t : Interval Time) : (IMPF P w t → ∃ e, P w e ∧ t.properSubinterval e.τ) ∧ (PRFV P w t → ∃ e, P w e ∧ e.τ.subinterval t) := ⟨λ ⟨e, hSub, hP⟩ => ⟨e, hP, hSub⟩, @@ -333,22 +332,22 @@ theorem impf_prfv_opposite_containment (P : EventPred W Time) (w : W) (t : Inter /-- Pancheva's UNBOUNDED (Asp₂): non-strict ⊆ variant of IMPF. ⟦UNBOUNDED⟧ = λP.λi.∃e[i ⊆ τ(e) & P(e)] (@cite{pancheva-2003}: 282, eq. 7b). Differs from IMPF in using non-strict ⊆ rather than strict ⊂. -/ -def UNBOUNDED (P : EventPred W Time) : IntervalPred W Time := +def UNBOUNDED (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, t.subinterval e.τ ∧ P w e /-- Pancheva's BOUNDED (Asp₂): strict ⊂ variant of PRFV. ⟦BOUNDED⟧ = λP.λi.∃e[τ(e) ⊂ i & P(e)] (@cite{pancheva-2003}: 282, eq. 7b). Differs from PRFV in using strict ⊂ rather than non-strict ⊆. -/ -def BOUNDED (P : EventPred W Time) : IntervalPred W Time := +def BOUNDED (P : W → Event Time → Prop) : IntervalPred W Time := λ w t => ∃ e : Event Time, e.τ.properSubinterval t ∧ P w e /-- IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆). -/ -theorem impf_entails_unbounded (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem impf_entails_unbounded (P : W → Event Time → Prop) (w : W) (t : Interval Time) : IMPF P w t → UNBOUNDED P w t := λ ⟨e, hSub, hP⟩ => ⟨e, hSub.1, hP⟩ /-- BOUNDED (strict ⊂) entails PRFV (non-strict ⊆). -/ -theorem bounded_entails_prfv (P : EventPred W Time) (w : W) (t : Interval Time) : +theorem bounded_entails_prfv (P : W → Event Time → Prop) (w : W) (t : Interval Time) : BOUNDED P w t → PRFV P w t := λ ⟨e, hSub, hP⟩ => ⟨e, hSub.1, hP⟩ @@ -390,25 +389,25 @@ inductive PerfectType where /-- Universal perfect: PERF_P(UNBOUNDED(V)). "has been running" — event ongoing throughout PTS. @cite{pancheva-2003}: explains why universal reading requires imperfective. -/ -abbrev universalPerfect (P : EventPred W Time) : IntervalPred W Time := +abbrev universalPerfect (P : W → Event Time → Prop) : IntervalPred W Time := PERF_P (UNBOUNDED P) /-- Experiential perfect: PERF_P(INIT_OVERLAP(V)). "has visited Paris" — event began within PTS. @cite{pancheva-2003}: initial-overlap aspect allows event to extend beyond PTS. -/ -abbrev experientialPerfect (P : EventPred W Time) : IntervalPred W Time := +abbrev experientialPerfect (P : W → Event Time → Prop) : IntervalPred W Time := PERF_P (INIT_OVERLAP P) /-- Resultative perfect: PERF_P(BOUNDED(V)). "has broken the vase" — event completed within PTS. Simplified: properly involves result state (@cite{pancheva-2003}: 288). -/ -abbrev resultativePerfect (P : EventPred W Time) : IntervalPred W Time := +abbrev resultativePerfect (P : W → Event Time → Prop) : IntervalPred W Time := PERF_P (BOUNDED P) /-- perfProg at a point entails universalPerfect at that point. Since IMPF (strict ⊂) entails UNBOUNDED (non-strict ⊆), PERF(IMPF(V)) entails PERF(UNBOUNDED(V)) = universalPerfect. -/ -theorem perf_prog_entails_universal_at_point (P : EventPred W Time) (w : W) (t : Time) : +theorem perf_prog_entails_universal_at_point (P : W → Event Time → Prop) (w : W) (t : Time) : perfProg P ⟨w, t⟩ → universalPerfect P w (Interval.point t) := λ h => (perf_p_at_point_iff_perf (UNBOUNDED P) w t).mpr (perf_monotone (IMPF P) (UNBOUNDED P) (impf_entails_unbounded P) w t h) diff --git a/Linglib/Semantics/Aspect/Stratified.lean b/Linglib/Semantics/Aspect/Stratified.lean index 9e7cc7083..e0f6e7d4b 100644 --- a/Linglib/Semantics/Aspect/Stratified.lean +++ b/Linglib/Semantics/Aspect/Stratified.lean @@ -76,7 +76,6 @@ atelicity diagnostic; CUM is the NP→VP propagation property. namespace Semantics.Aspect.Stratified -open Semantics.Events open Semantics.Events.CEM open _root_.Mereology open Core.Time diff --git a/Linglib/Semantics/Aspect/SubeventStructure.lean b/Linglib/Semantics/Aspect/SubeventStructure.lean index dc36d4cf1..6cfb0b2b2 100644 --- a/Linglib/Semantics/Aspect/SubeventStructure.lean +++ b/Linglib/Semantics/Aspect/SubeventStructure.lean @@ -21,7 +21,7 @@ temporally simple. This module makes that structure explicit via - `TemporalDecomposition`: `.simple` (single runtime) or `.complex` (phased) - `hasComplexDecomposition`: telic classes have complex decomposition - `DecomposedEv`: event enriched with decomposition -- `phasePred`: converts an interval (event phase) into an `EventPred` for +- `phasePred`: converts an interval (event phase) into an event predicate for ViewpointAspect operators - `MoensSteedmanClass`: five-way event classification - `Nucleus`: tripartite event structure (prep process → culmination → cons state) @@ -29,7 +29,7 @@ temporally simple. This module makes that structure explicit via ## ViewpointAspect Bridge (§ 6–7) -`phasePred` converts temporal phases into `EventPred Unit Time`, making them +`phasePred` converts temporal phases into `Unit → Event Time → Prop`, making them consumable by IMPF/PRFV/PERF. Key results: - `impf_phasePred` / `prfv_phasePred`: reduce operator applications to @@ -47,7 +47,6 @@ namespace Semantics.Aspect.SubeventStructure open Core.Time open Features -open Semantics.Events /-! ### Subevent Phases -/ @@ -142,14 +141,14 @@ structure DecomposedEv (Time : Type*) [LinearOrder Time] where runtime_consistent : decomposition.runtime = event.runtime /-- Attach a simple decomposition to an event (for states/activities). -/ -def Event.withSimpleDecomposition {Time : Type*} [LinearOrder Time] +def _root_.Event.withSimpleDecomposition {Time : Type*} [LinearOrder Time] (e : Event Time) : DecomposedEv Time where event := e decomposition := .simple e.runtime runtime_consistent := rfl /-- Attach a complex decomposition to an event (for accomplishments/achievements). -/ -def Event.withComplexDecomposition {Time : Type*} [LinearOrder Time] +def _root_.Event.withComplexDecomposition {Time : Type*} [LinearOrder Time] (e : Event Time) (phases : SubeventPhases Time) (h_act : phases.activityTrace.subinterval e.runtime) (h_res : phases.resultTrace.subinterval e.runtime) : DecomposedEv Time where @@ -186,7 +185,6 @@ theorem simple_no_activity {Time : Type*} [LinearOrder Time] /-! ### Phase Event Predicates -/ -open Semantics.Events open Semantics.Aspect /-- Event predicate localized to an interval: holds of eventualities whose @@ -198,7 +196,7 @@ open Semantics.Aspect is world-independent (following the same convention as `Giannakidou.lean`). -/ def phasePred {Time : Type*} [LinearOrder Time] - (phase : Interval Time) : EventPred Unit Time := + (phase : Interval Time) : Unit → Event Time → Prop := λ _ ev => ev.runtime = phase /-- IMPF applied to a phase predicate reduces to the reference time being @@ -209,7 +207,7 @@ theorem impf_phasePred {Time : Type*} [LinearOrder Time] simp only [IMPF, phasePred, Event.τ] constructor · rintro ⟨e, hSub, rfl⟩; exact hSub - · intro h; exact ⟨⟨phase, .action⟩, h, rfl⟩ + · intro h; exact ⟨⟨phase, .dynamic⟩, h, rfl⟩ /-- PRFV applied to a phase predicate reduces to the phase interval being contained in the reference time. -/ @@ -219,7 +217,7 @@ theorem prfv_phasePred {Time : Type*} [LinearOrder Time] simp only [PRFV, phasePred, Event.τ] constructor · rintro ⟨e, hSub, rfl⟩; exact hSub - · intro h; exact ⟨⟨phase, .action⟩, h, rfl⟩ + · intro h; exact ⟨⟨phase, .dynamic⟩, h, rfl⟩ /-! ### ViewpointAspect ↔ Decomposition Bridge -/ diff --git a/Linglib/Semantics/Aspect/SubintervalProperty.lean b/Linglib/Semantics/Aspect/SubintervalProperty.lean index 8d513ac52..46a20c8b6 100644 --- a/Linglib/Semantics/Aspect/SubintervalProperty.lean +++ b/Linglib/Semantics/Aspect/SubintervalProperty.lean @@ -1,232 +1,231 @@ -import Linglib.Semantics.Aspect.Basic - -/-! -# The Subinterval Property - -The subinterval property (Bennett & Partee 1972, Dowty 1979) is a fundamental -semantic property of event predicates that determines their aspectual class: - -- **Statives and activities** have it: if John is sleeping for [1pm, 3pm], - he is sleeping at every subinterval -- **Accomplishments and achievements** lack it: if John built a house in - [Jan, Dec], he did not build a house in [Jan, Feb] - -This property is central to the semantics of temporal adverbials -(@cite{rouillard-2026}), NPI licensing in boundary adverbials -(@cite{iatridou-zeijlstra-2021}), and the distribution of progressive -and imperfective aspect crosslinguistically. - -Originally extracted from a Rouillard-2026 substrate file (since deleted in -the 2026-05 rebuild — see `Studies/Rouillard2026.lean`) -because it is a general property of event predicates, not specific to any -particular analysis. --/ - -namespace Semantics.Aspect.SubintervalProperty - -open Core.Time -open Semantics.Events -open Semantics.Aspect - -variable {W Time : Type*} [LinearOrder Time] - -/-- **Subinterval property for event predicates** (mereological version). - SUB(P) iff every subinterval of a P-event's runtime that is also - the runtime of some event is the runtime of a P-event. - States and activities have this property; accomplishments/achievements - lack it. - - This is the universal-witness (Bennett-Partee 1972) form of stativity - along the time dimension. The `SR_univ` decomposition form at - @cite{champollion-2017}'s analogous parameter-space point (dim = τ, - point-interval granularity) is genuinely different math — ∃-decomposition - over P-parts vs ∀-projection over hypothetical witness events. The - quantifier-level cousin (Zhao 2025 Def. 5.36, ATOM-DIST_t) lives in - `Core/Time/AtomDist.lean`. The three formulations are NOT directly - interderivable; bridging requires explicit witness-existence - assumptions. -/ -def HasSubintervalProp (P : EventPred W Time) : Prop := - ∀ (e₁ : Event Time) (w : W), - P w e₁ → - ∀ (t : Interval Time), t.subinterval e₁.τ → - ∀ (e₂ : Event Time), e₂.τ = t → - P w e₂ - -/-- **Closed subinterval property** (CSUB). - For any subinterval t of a P-event's runtime, there exists a P-event - whose runtime is t. Stronger than SUB: guarantees witnesses exist, - not just that predication is preserved. -/ -def HasClosedSubintervalProp (P : EventPred W Time) : Prop := - ∀ (e₁ : Event Time) (w : W), - P w e₁ → - ∀ (t : Interval Time), t.subinterval e₁.τ → - ∃ (e₂ : Event Time), e₂.τ = t ∧ P w e₂ - --- ════════════════════════════════════════════════════ --- § Operator-Level Consequences --- ════════════════════════════════════════════════════ - -/-! The subinterval property's consequences at the level of aspect operators. - @cite{smith-1997} Ch. 2: states and activities have the subinterval - property; accomplishments, achievements, and semelfactives lack it. - - `Features/Aktionsart.lean` carries the VendlerClass enum used to - state the consumer-side facts (`c = .state ∨ c = .activity` for - SUB-having classes). Here we prove the operator-level consequences: - - 1. **Activity entailment** (p. 25): IMPF(activity) at I entails - PRFV(activity) at some I' ⊆ I — activities have part-whole homogeneity. - 2. **Imperfective paradox** (p. 29): IMPF(accomplishment) does NOT - entail PRFV(accomplishment) — the missing endpoint problem. - 3. **IMPF ⊢ PRFV ⟺ CSIP**: the imperfective entails the perfective - if and only if the predicate has the closed subinterval property. -/ - -open Features - -/-- **Activity entailment** (@cite{smith-1997} p. 25): - If an activity predicate P holds at interval I (IMPF reading: I is - inside the event's runtime), then P holds at every subinterval of I - (PRFV reading: subinterval is contained in the event). - - Formally: HasSubintervalProp(P) → IMPF(P)(w)(I) → ∀ I' ⊆ I, ∃e. τ(e) = I' ∧ P(w)(e). - - This is the semantic content of "activities entail their own - imperfective": "John was running" at I entails "John ran" at - every subinterval of I. -/ -theorem activity_entailment - (P : EventPred W Time) (hSub : HasClosedSubintervalProp P) - (w : W) (e₁ : Event Time) (hP : P w e₁) - (t : Interval Time) (hSub' : t.subinterval e₁.τ) : - ∃ (e₂ : Event Time), e₂.τ = t ∧ P w e₂ := - hSub e₁ w hP t hSub' - -/-- **Imperfective paradox** (@cite{smith-1997} p. 29): - The subinterval property fails for accomplishments. This is why - "John was building a house" does not entail "John built a house": - proper subintervals of a house-building event are not themselves - house-building events (the result state is missing). - - The hypothesis `t₁ < t₂` ensures Time is nontrivial — in a singleton - Time there is only one interval and the SIP holds vacuously for all P. - With two distinct time points, we can construct a "telic" predicate - P that holds only for events spanning the full interval [t₁, t₂] - and fails for proper subintervals like [t₁, t₁]. -/ -theorem imperfective_paradox_possible - (w : W) (t₁ t₂ : Time) (hlt : t₁ < t₂) : - ¬ (∀ (P : EventPred W Time), HasSubintervalProp P) := by - intro hall - -- Define a "telic" predicate: P holds iff the event's runtime ends at t₂ - let P : EventPred W Time := λ _ e => e.τ.finish = t₂ - have hSub := hall P - -- Construct an event e₁ with runtime [t₁, t₂]; P holds (finish = t₂) - -- sort defaults to .action; the proof doesn't reference .sort - let e₁ : Event Time := ⟨⟨t₁, t₂, le_of_lt hlt⟩, .action⟩ - have hPe₁ : P w e₁ := rfl - -- [t₁, t₁] is a subinterval of [t₁, t₂] - let sub : Interval Time := ⟨t₁, t₁, le_refl t₁⟩ - have hSI : sub.subinterval e₁.τ := ⟨le_refl t₁, le_of_lt hlt⟩ - -- SIP says P must hold for any event with runtime [t₁, t₁] - -- sort defaults to .action; the proof doesn't reference .sort - let e₂ : Event Time := ⟨sub, .action⟩ - have hPe₂ := hSub e₁ w hPe₁ sub hSI e₂ rfl - -- But P w e₂ means t₁ = t₂, contradicting t₁ < t₂ - exact absurd hPe₂ (ne_of_lt hlt) - --- ════════════════════════════════════════════════════ --- § IMPF ⊢ PRFV for Homogeneous Predicates --- ════════════════════════════════════════════════════ - -/-! The central result connecting aspect operators to the subinterval - property. For predicates with the closed SIP (states, activities), - the imperfective entails the perfective at the same interval: - - CSIP(P) → IMPF(P)(w)(t) → PRFV(P)(w)(t) - - This is the formal reason the imperfective paradox does NOT arise - for homogeneous predicates. "Mary was running" (IMPF) entails - "Mary ran" (PRFV) because any subinterval of a running event is - itself a running event — so the reference time t, which is inside - the event's runtime, is itself the runtime of a running event. - - Combined with `imperfective_paradox_possible` (which shows that - predicates without the SIP can fail this entailment), this gives - a complete characterization: - - IMPF entails PRFV ⟺ the predicate has the subinterval property - - The proof: - 1. IMPF gives us event e with t ⊂ τ(e) and P(w, e) - 2. properSubinterval implies subinterval: t ⊆ τ(e) - 3. CSIP with e, w, t yields witness e₂ with τ(e₂) = t and P(w, e₂) - 4. Since τ(e₂) = t ⊆ t (reflexive), PRFV holds with witness e₂ -/ - -/-- **IMPF entails PRFV for CSIP predicates** (@cite{smith-1997} Ch. 2). - If P has the closed subinterval property, then IMPF(P)(w)(t) entails - PRFV(P)(w)(t) — the imperfective entails the perfective at the same - reference interval. - - This is why "Mary was running" entails "Mary ran": the reference - time t is properly inside the running event's runtime, and since - running has the CSIP, there exists a running event whose runtime - IS exactly t, which satisfies the PRFV containment requirement. -/ -theorem impf_entails_prfv_of_csip - (P : EventPred W Time) (hCSIP : HasClosedSubintervalProp P) - (w : W) (t : Interval Time) : - IMPF P w t → PRFV P w t := by - intro ⟨e, hPSub, hP⟩ - -- hPSub : t.properSubinterval e.τ — reference time properly inside event - -- hPSub.1 : t.subinterval e.τ — non-strict containment (first component) - -- hP : P w e — the predicate holds for e - obtain ⟨e₂, he₂, hPe₂⟩ := hCSIP e w hP t hPSub.1 - -- e₂ : event with τ(e₂) = t and P(w, e₂) - -- For PRFV we need τ(e₂) ⊆ t, i.e. t ⊆ t (since τ(e₂) = t) - exact ⟨e₂, he₂ ▸ Interval.subinterval_refl t, hPe₂⟩ - -/-- **CSIP is necessary for IMPF→PRFV** (converse of `impf_entails_prfv_of_csip`): - if IMPF entails PRFV for ALL predicates, then every predicate has CSIP. - - Combined with the forward direction, this gives a complete characterization: - (∀ P, IMPF(P) ⊆ PRFV(P)) ⟺ (∀ P, CSIP(P)) - - The proof uses the **refined predicate trick**: given P, e, w, t with - P(w,e) and t ⊆ τ(e), we apply the hypothesis not to P directly but - to Q(w', e') := P(w', e') ∧ t ⊆ τ(e'). Then: - - PRFV gives τ(e₂) ⊆ t (event contained in reference time) - - Q gives t ⊆ τ(e₂) (from the predicate's second conjunct) - - Mutual containment gives τ(e₂) = t (closing the ⊆ → = gap) -/ -theorem csip_necessary_for_impf_prfv : - (∀ (P : EventPred W Time) (w : W) (t : Interval Time), - IMPF P w t → PRFV P w t) → - ∀ (P : EventPred W Time), HasClosedSubintervalProp P := by - intro hall P e w hP t hSub - -- Case split: τ(e) = t or τ(e) ≠ t - by_cases heq : e.τ = t - · -- τ(e) = t: e itself witnesses CSIP - exact ⟨e, heq, hP⟩ - · -- τ(e) ≠ t: t is a proper subinterval of τ(e) - -- Step 1: derive properness from subinterval + inequality - have hProper : t.properSubinterval e.τ := by - refine ⟨hSub, ?_⟩ - by_contra hne - push Not at hne - -- hne : t.start ≤ e.τ.start ∧ e.τ.finish ≤ t.finish - apply heq - have ⟨h1, h2⟩ := hSub - -- h1 : e.τ.start ≤ t.start, h2 : t.finish ≤ e.τ.finish - have hs := le_antisymm h1 hne.1 - have hf := le_antisymm hne.2 h2 - rcases e with ⟨⟨_, _, _⟩⟩; rcases t with ⟨_, _, _⟩; simp_all - -- Step 2: refined predicate Q carries reverse containment - let Q : EventPred W Time := fun w' e' => P w' e' ∧ t.subinterval e'.τ - -- IMPF(Q)(w)(t): witnessed by e (proper subinterval + P holds + t ⊆ τ(e)) - obtain ⟨e₂, hSub₂, hPe₂, hSubRev⟩ := hall Q w t ⟨e, hProper, hP, hSub⟩ - -- hSub₂ : τ(e₂) ⊆ t (from PRFV), hSubRev : t ⊆ τ(e₂) (from Q) - -- Mutual containment → equality - refine ⟨e₂, ?_, hPe₂⟩ - have ⟨a1, a2⟩ := hSub₂ - have ⟨b1, b2⟩ := hSubRev - rcases e₂ with ⟨⟨_, _, _⟩, _⟩; rcases t with ⟨_, _, _⟩ - simp only [Event.τ, Interval.mk.injEq] - exact ⟨le_antisymm b1 a1, le_antisymm a2 b2⟩ - -end Semantics.Aspect.SubintervalProperty +import Linglib.Semantics.Aspect.Basic + +/-! +# The Subinterval Property + +The subinterval property (Bennett & Partee 1972, Dowty 1979) is a fundamental +semantic property of event predicates that determines their aspectual class: + +- **Statives and activities** have it: if John is sleeping for [1pm, 3pm], + he is sleeping at every subinterval +- **Accomplishments and achievements** lack it: if John built a house in + [Jan, Dec], he did not build a house in [Jan, Feb] + +This property is central to the semantics of temporal adverbials +(@cite{rouillard-2026}), NPI licensing in boundary adverbials +(@cite{iatridou-zeijlstra-2021}), and the distribution of progressive +and imperfective aspect crosslinguistically. + +Originally extracted from a Rouillard-2026 substrate file (since deleted in +the 2026-05 rebuild — see `Studies/Rouillard2026.lean`) +because it is a general property of event predicates, not specific to any +particular analysis. +-/ + +namespace Semantics.Aspect.SubintervalProperty + +open Core.Time +open Semantics.Aspect + +variable {W Time : Type*} [LinearOrder Time] + +/-- **Subinterval property for event predicates** (mereological version). + SUB(P) iff every subinterval of a P-event's runtime that is also + the runtime of some event is the runtime of a P-event. + States and activities have this property; accomplishments/achievements + lack it. + + This is the universal-witness (Bennett-Partee 1972) form of stativity + along the time dimension. The `SR_univ` decomposition form at + @cite{champollion-2017}'s analogous parameter-space point (dim = τ, + point-interval granularity) is genuinely different math — ∃-decomposition + over P-parts vs ∀-projection over hypothetical witness events. The + quantifier-level cousin (Zhao 2025 Def. 5.36, ATOM-DIST_t) lives in + `Core/Time/AtomDist.lean`. The three formulations are NOT directly + interderivable; bridging requires explicit witness-existence + assumptions. -/ +def HasSubintervalProp (P : W → Event Time → Prop) : Prop := + ∀ (e₁ : Event Time) (w : W), + P w e₁ → + ∀ (t : Interval Time), t.subinterval e₁.τ → + ∀ (e₂ : Event Time), e₂.τ = t → + P w e₂ + +/-- **Closed subinterval property** (CSUB). + For any subinterval t of a P-event's runtime, there exists a P-event + whose runtime is t. Stronger than SUB: guarantees witnesses exist, + not just that predication is preserved. -/ +def HasClosedSubintervalProp (P : W → Event Time → Prop) : Prop := + ∀ (e₁ : Event Time) (w : W), + P w e₁ → + ∀ (t : Interval Time), t.subinterval e₁.τ → + ∃ (e₂ : Event Time), e₂.τ = t ∧ P w e₂ + +-- ════════════════════════════════════════════════════ +-- § Operator-Level Consequences +-- ════════════════════════════════════════════════════ + +/-! The subinterval property's consequences at the level of aspect operators. + @cite{smith-1997} Ch. 2: states and activities have the subinterval + property; accomplishments, achievements, and semelfactives lack it. + + `Features/Aktionsart.lean` carries the VendlerClass enum used to + state the consumer-side facts (`c = .state ∨ c = .activity` for + SUB-having classes). Here we prove the operator-level consequences: + + 1. **Activity entailment** (p. 25): IMPF(activity) at I entails + PRFV(activity) at some I' ⊆ I — activities have part-whole homogeneity. + 2. **Imperfective paradox** (p. 29): IMPF(accomplishment) does NOT + entail PRFV(accomplishment) — the missing endpoint problem. + 3. **IMPF ⊢ PRFV ⟺ CSIP**: the imperfective entails the perfective + if and only if the predicate has the closed subinterval property. -/ + +open Features + +/-- **Activity entailment** (@cite{smith-1997} p. 25): + If an activity predicate P holds at interval I (IMPF reading: I is + inside the event's runtime), then P holds at every subinterval of I + (PRFV reading: subinterval is contained in the event). + + Formally: HasSubintervalProp(P) → IMPF(P)(w)(I) → ∀ I' ⊆ I, ∃e. τ(e) = I' ∧ P(w)(e). + + This is the semantic content of "activities entail their own + imperfective": "John was running" at I entails "John ran" at + every subinterval of I. -/ +theorem activity_entailment + (P : W → Event Time → Prop) (hSub : HasClosedSubintervalProp P) + (w : W) (e₁ : Event Time) (hP : P w e₁) + (t : Interval Time) (hSub' : t.subinterval e₁.τ) : + ∃ (e₂ : Event Time), e₂.τ = t ∧ P w e₂ := + hSub e₁ w hP t hSub' + +/-- **Imperfective paradox** (@cite{smith-1997} p. 29): + The subinterval property fails for accomplishments. This is why + "John was building a house" does not entail "John built a house": + proper subintervals of a house-building event are not themselves + house-building events (the result state is missing). + + The hypothesis `t₁ < t₂` ensures Time is nontrivial — in a singleton + Time there is only one interval and the SIP holds vacuously for all P. + With two distinct time points, we can construct a "telic" predicate + P that holds only for events spanning the full interval [t₁, t₂] + and fails for proper subintervals like [t₁, t₁]. -/ +theorem imperfective_paradox_possible + (w : W) (t₁ t₂ : Time) (hlt : t₁ < t₂) : + ¬ (∀ (P : W → Event Time → Prop), HasSubintervalProp P) := by + intro hall + -- Define a "telic" predicate: P holds iff the event's runtime ends at t₂ + let P : W → Event Time → Prop := λ _ e => e.τ.finish = t₂ + have hSub := hall P + -- Construct an event e₁ with runtime [t₁, t₂]; P holds (finish = t₂) + -- sort defaults to .action; the proof doesn't reference .sort + let e₁ : Event Time := ⟨⟨t₁, t₂, le_of_lt hlt⟩, .dynamic⟩ + have hPe₁ : P w e₁ := rfl + -- [t₁, t₁] is a subinterval of [t₁, t₂] + let sub : Interval Time := ⟨t₁, t₁, le_refl t₁⟩ + have hSI : sub.subinterval e₁.τ := ⟨le_refl t₁, le_of_lt hlt⟩ + -- SIP says P must hold for any event with runtime [t₁, t₁] + -- sort defaults to .action; the proof doesn't reference .sort + let e₂ : Event Time := ⟨sub, .dynamic⟩ + have hPe₂ := hSub e₁ w hPe₁ sub hSI e₂ rfl + -- But P w e₂ means t₁ = t₂, contradicting t₁ < t₂ + exact absurd hPe₂ (ne_of_lt hlt) + +-- ════════════════════════════════════════════════════ +-- § IMPF ⊢ PRFV for Homogeneous Predicates +-- ════════════════════════════════════════════════════ + +/-! The central result connecting aspect operators to the subinterval + property. For predicates with the closed SIP (states, activities), + the imperfective entails the perfective at the same interval: + + CSIP(P) → IMPF(P)(w)(t) → PRFV(P)(w)(t) + + This is the formal reason the imperfective paradox does NOT arise + for homogeneous predicates. "Mary was running" (IMPF) entails + "Mary ran" (PRFV) because any subinterval of a running event is + itself a running event — so the reference time t, which is inside + the event's runtime, is itself the runtime of a running event. + + Combined with `imperfective_paradox_possible` (which shows that + predicates without the SIP can fail this entailment), this gives + a complete characterization: + + IMPF entails PRFV ⟺ the predicate has the subinterval property + + The proof: + 1. IMPF gives us event e with t ⊂ τ(e) and P(w, e) + 2. properSubinterval implies subinterval: t ⊆ τ(e) + 3. CSIP with e, w, t yields witness e₂ with τ(e₂) = t and P(w, e₂) + 4. Since τ(e₂) = t ⊆ t (reflexive), PRFV holds with witness e₂ -/ + +/-- **IMPF entails PRFV for CSIP predicates** (@cite{smith-1997} Ch. 2). + If P has the closed subinterval property, then IMPF(P)(w)(t) entails + PRFV(P)(w)(t) — the imperfective entails the perfective at the same + reference interval. + + This is why "Mary was running" entails "Mary ran": the reference + time t is properly inside the running event's runtime, and since + running has the CSIP, there exists a running event whose runtime + IS exactly t, which satisfies the PRFV containment requirement. -/ +theorem impf_entails_prfv_of_csip + (P : W → Event Time → Prop) (hCSIP : HasClosedSubintervalProp P) + (w : W) (t : Interval Time) : + IMPF P w t → PRFV P w t := by + intro ⟨e, hPSub, hP⟩ + -- hPSub : t.properSubinterval e.τ — reference time properly inside event + -- hPSub.1 : t.subinterval e.τ — non-strict containment (first component) + -- hP : P w e — the predicate holds for e + obtain ⟨e₂, he₂, hPe₂⟩ := hCSIP e w hP t hPSub.1 + -- e₂ : event with τ(e₂) = t and P(w, e₂) + -- For PRFV we need τ(e₂) ⊆ t, i.e. t ⊆ t (since τ(e₂) = t) + exact ⟨e₂, he₂ ▸ Interval.subinterval_refl t, hPe₂⟩ + +/-- **CSIP is necessary for IMPF→PRFV** (converse of `impf_entails_prfv_of_csip`): + if IMPF entails PRFV for ALL predicates, then every predicate has CSIP. + + Combined with the forward direction, this gives a complete characterization: + (∀ P, IMPF(P) ⊆ PRFV(P)) ⟺ (∀ P, CSIP(P)) + + The proof uses the **refined predicate trick**: given P, e, w, t with + P(w,e) and t ⊆ τ(e), we apply the hypothesis not to P directly but + to Q(w', e') := P(w', e') ∧ t ⊆ τ(e'). Then: + - PRFV gives τ(e₂) ⊆ t (event contained in reference time) + - Q gives t ⊆ τ(e₂) (from the predicate's second conjunct) + - Mutual containment gives τ(e₂) = t (closing the ⊆ → = gap) -/ +theorem csip_necessary_for_impf_prfv : + (∀ (P : W → Event Time → Prop) (w : W) (t : Interval Time), + IMPF P w t → PRFV P w t) → + ∀ (P : W → Event Time → Prop), HasClosedSubintervalProp P := by + intro hall P e w hP t hSub + -- Case split: τ(e) = t or τ(e) ≠ t + by_cases heq : e.τ = t + · -- τ(e) = t: e itself witnesses CSIP + exact ⟨e, heq, hP⟩ + · -- τ(e) ≠ t: t is a proper subinterval of τ(e) + -- Step 1: derive properness from subinterval + inequality + have hProper : t.properSubinterval e.τ := by + refine ⟨hSub, ?_⟩ + by_contra hne + push Not at hne + -- hne : t.start ≤ e.τ.start ∧ e.τ.finish ≤ t.finish + apply heq + have ⟨h1, h2⟩ := hSub + -- h1 : e.τ.start ≤ t.start, h2 : t.finish ≤ e.τ.finish + have hs := le_antisymm h1 hne.1 + have hf := le_antisymm hne.2 h2 + rcases e with ⟨⟨_, _, _⟩⟩; rcases t with ⟨_, _, _⟩; simp_all + -- Step 2: refined predicate Q carries reverse containment + let Q : W → Event Time → Prop := fun w' e' => P w' e' ∧ t.subinterval e'.τ + -- IMPF(Q)(w)(t): witnessed by e (proper subinterval + P holds + t ⊆ τ(e)) + obtain ⟨e₂, hSub₂, hPe₂, hSubRev⟩ := hall Q w t ⟨e, hProper, hP, hSub⟩ + -- hSub₂ : τ(e₂) ⊆ t (from PRFV), hSubRev : t ⊆ τ(e₂) (from Q) + -- Mutual containment → equality + refine ⟨e₂, ?_, hPe₂⟩ + have ⟨a1, a2⟩ := hSub₂ + have ⟨b1, b2⟩ := hSubRev + rcases e₂ with ⟨⟨_, _, _⟩, _⟩; rcases t with ⟨_, _, _⟩ + simp only [Event.τ, Interval.mk.injEq] + exact ⟨le_antisymm b1 a1, le_antisymm a2 b2⟩ + +end Semantics.Aspect.SubintervalProperty diff --git a/Linglib/Semantics/Attitudes/RationalAttitude.lean b/Linglib/Semantics/Attitudes/RationalAttitude.lean index dfef1029a..cf21c63e3 100644 --- a/Linglib/Semantics/Attitudes/RationalAttitude.lean +++ b/Linglib/Semantics/Attitudes/RationalAttitude.lean @@ -37,7 +37,6 @@ The parameter P is determined by complement size: namespace Semantics.Attitudes.RationalAttitude -open Semantics.Events (Event EventPred existsClosureW EventSort) open Minimalist (ComplementSize fValue) -- ════════════════════════════════════════════════════════════════ @@ -95,9 +94,10 @@ theorem size_determines_reading (cs : ComplementSize) : For CP complements, CLOSURE converts an event predicate P(e) into a proposition ∃e. P(e), yielding a belief-compatible propositional content. - This is `existsClosureW` from event semantics, re-exported under the - name used in @cite{fusco-sgrizzi-2026}. -/ -abbrev closure {W Time : Type*} [LinearOrder Time] := @existsClosureW W Time _ + This is pointwise Davidsonian existential closure (`Event.existsClosure`), + re-exported under the name used in @cite{fusco-sgrizzi-2026}. -/ +abbrev closure {W Time : Type*} [LinearOrder Time] (P : W → Event Time → Prop) : W → Prop := + fun w => Event.existsClosure (P w) -- ════════════════════════════════════════════════════════════════ -- § 4. Causative Attitude Verb (convincere-type) @@ -141,7 +141,7 @@ def CausativeAttitude.denote {E Time : Type*} [LinearOrder Time] v.isAgent e v.agent ∧ v.isPatient e v.experiencer ∧ v.cause e e' ∧ - e'.sort = .state ∧ -- Rational attitudes are stative + e'.sort = .stative ∧ -- Rational attitudes are stative v.isExperiencer e' v.experiencer ∧ P e' @@ -208,7 +208,7 @@ def intentionHolds {E W Time : Type*} [LinearOrder Time] (causeStar : CauseStar W Time) (agent : E) (P : E → W → Event Time → Prop) (w : W) : Prop := ∃ s : Event Time, - s.sort = .state ∧ + s.sort = .stative ∧ isIntention s w ∧ holder agent s w ∧ ∀ p ∈ content s, ∃ e : Event Time, causeStar s e p.1 ∧ P p.2 p.1 e diff --git a/Linglib/Semantics/Causation/PsychLink.lean b/Linglib/Semantics/Causation/PsychLink.lean index 2d82c02f0..dde6cbb6c 100644 --- a/Linglib/Semantics/Causation/PsychLink.lean +++ b/Linglib/Semantics/Causation/PsychLink.lean @@ -22,7 +22,7 @@ differ along three dimensions: | Counterfactual | effect persists after cause ceases | effect ceases with cause | The first three properties are formalized using existing Linglib types: -`EventSort`, `Interval.precedes`/`.overlaps`. +`Features.Dynamicity`, `Interval.precedes`/`.overlaps`. The fourth uses `universalCounterfactual` from `Counterfactual.lean`. ## Key results @@ -37,7 +37,6 @@ The fourth uses `universalCounterfactual` from `Counterfactual.lean`. namespace Semantics.Causation.PsychLink open Core.Time (Interval) -open Semantics.Events (EventSort) open Semantics.Causation.Psych (CausalSource) open Core.Order (SimilarityOrdering) open Semantics.Conditionals.Counterfactual (universalCounterfactual) @@ -53,9 +52,9 @@ open Semantics.Conditionals.Counterfactual (universalCounterfactual) causation (representation → state persistence). -/ structure PsychCausalLink (Time : Type*) [LinearOrder Time] where /-- Ontological sort of the causing eventuality -/ - causeSort : EventSort + causeSort : Features.Dynamicity /-- Ontological sort of the caused eventuality -/ - effectSort : EventSort + effectSort : Features.Dynamicity /-- Does the effect involve a transition (BECOME in @cite{rappaport-hovav-levin-1998})? Eventive: [CAUSE [BECOME [STATE]]] — yes. Maintenance: [CAUSE [STATE]] — no. -/ @@ -74,8 +73,8 @@ structure PsychCausalLink (Time : Type*) [LinearOrder Time] where Example: "The noise frightened John" — the noise event happens, THEN John enters the frightened state. -/ def eventiveLink (Time : Type*) [LinearOrder Time] : PsychCausalLink Time := - { causeSort := .action - effectSort := .action + { causeSort := .dynamic + effectSort := .dynamic involvesTransition := true temporalConstraint := Interval.precedes } @@ -92,8 +91,8 @@ def eventiveLink (Time : Type*) [LinearOrder Time] : PsychCausalLink Time := (b) Temporal contemporaneity (τ(cause) overlaps τ(effect)) (c) Counterfactual dependence (effect ceases when cause ceases) -/ def maintenanceLink (Time : Type*) [LinearOrder Time] : PsychCausalLink Time := - { causeSort := .state - effectSort := .state + { causeSort := .stative + effectSort := .stative involvesTransition := false temporalConstraint := Interval.overlaps } @@ -145,13 +144,13 @@ theorem precedes_excludes_overlap {Time : Type*} [LinearOrder Time] /-- Maintenance relates two states (@cite{kim-2024} property (a)). -/ theorem maintenance_both_states {Time : Type*} [LinearOrder Time] : - (maintenanceLink Time).causeSort = .state ∧ - (maintenanceLink Time).effectSort = .state := ⟨rfl, rfl⟩ + (maintenanceLink Time).causeSort = .stative ∧ + (maintenanceLink Time).effectSort = .stative := ⟨rfl, rfl⟩ /-- Eventive causation relates two dynamic eventualities. -/ theorem eventive_both_dynamic {Time : Type*} [LinearOrder Time] : - (eventiveLink Time).causeSort = .action ∧ - (eventiveLink Time).effectSort = .action := ⟨rfl, rfl⟩ + (eventiveLink Time).causeSort = .dynamic ∧ + (eventiveLink Time).effectSort = .dynamic := ⟨rfl, rfl⟩ /-- Maintenance involves no transition (no BECOME). -/ theorem maintenance_no_transition {Time : Type*} [LinearOrder Time] : @@ -163,8 +162,8 @@ theorem eventive_has_transition {Time : Type*} [LinearOrder Time] : /-- The two causal flavors assign opposite values on every dimension. -/ theorem flavors_differ_on_all_dimensions {Time : Type*} [LinearOrder Time] : - (eventiveLink Time).causeSort = .action ∧ - (maintenanceLink Time).causeSort = .state ∧ + (eventiveLink Time).causeSort = .dynamic ∧ + (maintenanceLink Time).causeSort = .stative ∧ (eventiveLink Time).involvesTransition = true ∧ (maintenanceLink Time).involvesTransition = false := ⟨rfl, rfl, rfl, rfl⟩ @@ -247,7 +246,7 @@ theorem dependent_excludes_persistent {W : Type*} [DecidableEq W] [Fintype W] /-- The three defining properties of maintenance causation from @cite{kim-2024}, formalized using existing infrastructure: - (a) Relates two eventualities — both are states (`EventSort.state`) + (a) Relates two eventualities — both are states (`Features.Dynamicity.stative`) (b) Temporal contemporaneity — `Interval.overlaps` (c) No transition — effect is a persisting state, not a change @@ -259,8 +258,8 @@ theorem dependent_excludes_persistent {W : Type*} [DecidableEq W] [Fintype W] for WHY maintenance-caused states are counterfactually dependent. -/ theorem maintenance_three_properties {Time : Type*} [LinearOrder Time] : -- (a) Both eventualities are states - (maintenanceLink Time).causeSort = .state ∧ - (maintenanceLink Time).effectSort = .state ∧ + (maintenanceLink Time).causeSort = .stative ∧ + (maintenanceLink Time).effectSort = .stative ∧ -- (b) Temporal contemporaneity (overlaps, not precedes) (maintenanceLink Time).temporalConstraint = Interval.overlaps ∧ -- (c) No transition (no BECOME) diff --git a/Linglib/Semantics/Degree/MeasureFunction.lean b/Linglib/Semantics/Degree/MeasureFunction.lean index 399b40ddc..2d7284195 100644 --- a/Linglib/Semantics/Degree/MeasureFunction.lean +++ b/Linglib/Semantics/Degree/MeasureFunction.lean @@ -61,7 +61,6 @@ quantify over the scale's maximum (or its absence). namespace Semantics.Degree.MeasureFunction -open Semantics.Events open Semantics.ArgumentStructure.Affectedness -- ════════════════════════════════════════════════════ diff --git a/Linglib/Semantics/Events/Adjacency.lean b/Linglib/Semantics/Events/Adjacency.lean index be3d88947..641eb79a8 100644 --- a/Linglib/Semantics/Events/Adjacency.lean +++ b/Linglib/Semantics/Events/Adjacency.lean @@ -18,8 +18,6 @@ are consumed by: convex-time derivation) -/ -namespace Semantics.Events - /-- Two events are temporally adjacent (`∞_E` in @cite{krifka-1998}'s notation) if their runtime intervals meet: one's finish equals the other's start. The natural concrete instance of K98's @@ -42,5 +40,3 @@ theorem Event.adjacent_symm {Time : Type*} [LinearOrder Time] e1.adjacent e2 ↔ e2.adjacent e1 := by unfold Event.adjacent exact ⟨Or.symm, Or.symm⟩ - -end Semantics.Events diff --git a/Linglib/Semantics/Events/Basic.lean b/Linglib/Semantics/Events/Basic.lean index 7b44aeb1f..c221759a1 100644 --- a/Linglib/Semantics/Events/Basic.lean +++ b/Linglib/Semantics/Events/Basic.lean @@ -4,22 +4,19 @@ import Linglib.Features.Aktionsart /-! # Neo-Davidsonian Event Semantics — basic API -API on top of `Events/Defs.lean`'s foundational types: sort predicates, -EventSort ↔ Aktionsart Dynamicity bridge, concrete examples on `ℤ`-time. +API on top of `Events/Defs.lean`'s foundational types: sort predicates over +the `Features.Dynamicity` event sort, and concrete examples on `ℤ`-time. Files that only need to *talk about* events should import `Defs.lean` -directly to avoid pulling in `Features.Aktionsart`. +directly. ## Main definitions -* `Event.isAction` / `Event.isState` — Bool sort predicates -* `EventSort.toDynamicity` / `dynamicityToEventSort` — Aktionsart bridge -* `vendlerClass_sort_agrees` — VendlerClass dynamicity ↔ EventSort +* `Event.isAction` / `Event.isState` — decidable `Prop` sort predicates + (the `dynamic` / `stative` poles of `Features.Dynamicity`) * `exampleRun` / `exampleKnow` — concrete `Event ℤ` instances -/ -namespace Semantics.Events - open Core.Time open Features @@ -27,27 +24,19 @@ open Features /-- Is this event an action (dynamic event)? -/ def Event.isAction {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := - e.sort = .action + e.sort = .dynamic /-- Is this event a state (stative event)? -/ def Event.isState {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop := - e.sort = .state + e.sort = .stative instance {Time : Type*} [LinearOrder Time] : DecidablePred (Event.isAction (Time := Time)) := - fun e => decEq e.sort .action + fun e => decEq e.sort .dynamic instance {Time : Type*} [LinearOrder Time] : DecidablePred (Event.isState (Time := Time)) := - fun e => decEq e.sort .state - -/-- Every event is either an action or a state (exhaustivity). -/ -theorem sort_exhaustive (s : EventSort) : s = .action ∨ s = .state := by - cases s <;> simp - -/-- No event is both an action and a state (exclusivity). -/ -theorem sort_exclusive : EventSort.action ≠ EventSort.state := by - decide + fun e => decEq e.sort .stative /-- `isAction` and `isState` are complementary. -/ theorem isAction_iff_not_isState {Time : Type*} [LinearOrder Time] (e : Event Time) : @@ -61,45 +50,15 @@ theorem isState_iff_not_isAction {Time : Type*} [LinearOrder Time] (e : Event Ti simp only [Event.isAction, Event.isState] cases e.sort <;> decide -/-! ### Dynamicity Bridge (EventSort ↔ Aktionsart) -/ - -/-- Map EventSort to Dynamicity (the aspectual feature). -/ -def EventSort.toDynamicity : EventSort → Dynamicity - | .action => .dynamic - | .state => .stative - -/-- Map Dynamicity back to EventSort. -/ -def dynamicityToEventSort : Dynamicity → EventSort - | .dynamic => .action - | .stative => .state - -/-- Roundtrip: toDynamicity ∘ dynamicityToEventSort = id. -/ -theorem dynamicity_roundtrip (d : Dynamicity) : - (dynamicityToEventSort d).toDynamicity = d := by - cases d <;> rfl - -/-- Roundtrip: dynamicityToEventSort ∘ toDynamicity = id. -/ -theorem eventSort_roundtrip (s : EventSort) : - dynamicityToEventSort s.toDynamicity = s := by - cases s <;> rfl - -/-- VendlerClass dynamicity agrees with EventSort classification. - States map to .state sort; all others map to .action sort. -/ -theorem vendlerClass_sort_agrees (c : VendlerClass) : - dynamicityToEventSort c.dynamicity = match c with - | .state => EventSort.state - | .activity | .achievement | .accomplishment | .semelfactive => EventSort.action := by - cases c <;> rfl - /-! ### Concrete examples (ℤ-time events) -/ /-- Example: a running event from time 1 to 5. -/ def exampleRun : Event ℤ := - ⟨⟨1, 5, by omega⟩, .action⟩ + ⟨⟨1, 5, by omega⟩, .dynamic⟩ /-- Example: a knowing state from time 0 to 10. -/ def exampleKnow : Event ℤ := - ⟨⟨0, 10, by omega⟩, .state⟩ + ⟨⟨0, 10, by omega⟩, .stative⟩ /-- The run event is an action. -/ theorem exampleRun_isAction : exampleRun.isAction := rfl @@ -123,5 +82,3 @@ theorem exampleRun_finish : exampleRun.τ.finish = 5 := rfl theorem exampleKnow_runtime : exampleKnow.τ.start = 0 ∧ exampleKnow.τ.finish = 10 := ⟨rfl, rfl⟩ - -end Semantics.Events diff --git a/Linglib/Semantics/Events/CEM.lean b/Linglib/Semantics/Events/CEM.lean index 5d1dc00f4..fbfcd1a94 100644 --- a/Linglib/Semantics/Events/CEM.lean +++ b/Linglib/Semantics/Events/CEM.lean @@ -18,7 +18,6 @@ Generic mereological definitions (`CUM`, `DIV`, `QUA`, `Atom`, `AlgClosure`, namespace Semantics.Events.CEM -open Semantics.Events open Core.Time open Features open _root_.Mereology @@ -30,11 +29,11 @@ open _root_.Mereology /-! ### Event CEM (Classical Extensional Mereology) -/ -/-- Classical Extensional Mereology for events: enriches `EventMereology` +/-- Classical Extensional Mereology for events: enriches `Event.Mereology` with binary sum (⊔) via `SemilatticeSup (Event Time)`. @cite{champollion-2017} Ch. 2: event domain forms a join semilattice. -/ class EventCEM (Time : Type*) [LinearOrder Time] - extends EventMereology Time where + extends Event.Mereology Time where /-- Events form a join semilattice (binary sum ⊕ exists). -/ evSemilatticeSup : SemilatticeSup (Event Time) /-- ≤ from SemilatticeSup agrees with partOf. -/ @@ -60,14 +59,14 @@ noncomputable instance eventCEMSemilatticeSup (Time : Type*) [LinearOrder Time] iff for any two V-events, their sum is also a V-event. @cite{champollion-2017} §3.2: activities and states are lexically cumulative. -/ def LexCum (Time : Type*) [LinearOrder Time] [cem : EventCEM Time] - (P : EvPred Time) : Prop := + (P : Event Time → Prop) : Prop := ∀ (e₁ e₂ : Event Time), P e₁ → P e₂ → P (@SemilatticeSup.sup _ cem.evSemilatticeSup e₁ e₂) -/-- LexCum is exactly CUM specialized to EvPred. +/-- LexCum is exactly CUM specialized to event predicates. This bridges the abstract and event-specific formulations. -/ theorem cum_iff_lexCum (Time : Type*) [LinearOrder Time] [cem : EventCEM Time] - (P : EvPred Time) : + (P : Event Time → Prop) : @CUM _ cem.evSemilatticeSup P ↔ LexCum Time P := by constructor · intro h e₁ e₂ h₁ h₂; exact h e₁ e₂ h₁ h₂ diff --git a/Linglib/Semantics/Events/Defs.lean b/Linglib/Semantics/Events/Defs.lean index c19963639..86586db58 100644 --- a/Linglib/Semantics/Events/Defs.lean +++ b/Linglib/Semantics/Events/Defs.lean @@ -1,32 +1,31 @@ import Mathlib.Order.Basic import Linglib.Core.Time.Interval.Basic import Linglib.Tactics.OntSort +import Linglib.Features.Aktionsart /-! # Neo-Davidsonian Event Semantics — type definitions Foundational types for neo-Davidsonian event semantics (@cite{davidson-1967}, @cite{parsons-1990}). Verbs denote predicates of -events; thematic roles are independent two-place predicates (see -`ThematicRoles.lean`). +events; thematic roles are independent two-place predicates +(`Semantics.ArgumentStructure.ThematicRel`). This file is the `Defs` partner to `Basic.lean`: pure type/structure declarations and one foundational typeclass + instance, no API. Files that only need to *talk about* events (taking `Event Time` as an -argument, parameterizing by `[EventMereology Time]`) can import this +argument, parameterizing by `[Event.Mereology Time]`) can import this file alone; files that need sort predicates, dynamicity bridges, or Davidsonian existential closure import `Basic.lean`. ## Main definitions -* `EventSort` — binary action/state ontological sort (@cite{bach-1986}) -* `Event` — the unified event type: a runtime interval + sort +* `Event` — the unified event type: a runtime interval + `Features.Dynamicity` sort * `Event.τ` — temporal trace function -* `EventMereology` — part-of typeclass with τ-monotonicity + sort-preservation -* `eventPreorder` — Preorder instance derived from EventMereology -* `EvPred` / `EventPred` — predicate / world-indexed-predicate types -* `existsClosure` / `existsClosureW` — Davidsonian existential closure -* `Manner` — manner ontology (@cite{liefke-2024} §4.3) +* `Event.Mereology` — part-of typeclass with τ-monotonicity + sort-preservation +* `Event.preorder` — Preorder instance derived from `Event.Mereology` +* `Event.existsClosure` — Davidsonian existential closure +* `Event.Manner` — manner ontology (@cite{liefke-2024} §4.3) ## Naming note @@ -36,7 +35,7 @@ sense, non-state) has largely collapsed in current practice — @cite{champollion-2017} and @cite{zhao-2025} both use "event" generically with sort/aktionsart as an inherent attribute. Tense-aspect code that doesn't care about sort simply doesn't reference `.sort`; -sortless construction sites default to `.action`. +sortless construction sites default to `.dynamic`. ## References @@ -47,48 +46,34 @@ sortless construction sites default to `.action`. * @cite{liefke-2024} §4.3 (manner ontology) -/ -namespace Semantics.Events - open Core.Time -/-- Binary ontological sort for events. Actions involve change; states do not. -/ -inductive EventSort where - | action -- dynamic events (run, kick, build) - | state -- stative events (know, love, own) - deriving DecidableEq, Repr, Inhabited - /-- An event: a temporal individual with ontological sort. -/ @[ont_sort] structure Event (Time : Type*) [LinearOrder Time] where /-- The temporal extent of this event -/ runtime : Interval Time - /-- Ontological sort: action or state -/ - sort : EventSort + /-- Ontological sort (aktionsart): `dynamic` or `stative` (@cite{bach-1986}). + This is the `Features.Dynamicity` feature — the action/state distinction + at the event-token level. -/ + sort : Features.Dynamicity + +namespace Event + +variable {Time : Type*} [LinearOrder Time] /-- Temporal trace function τ(e) = the runtime interval of event e. -/ @[simp] -def Event.τ {Time : Type*} [LinearOrder Time] (e : Event Time) : Interval Time := +def τ (e : Event Time) : Interval Time := e.runtime -/-- A predicate over events (not world-indexed). -/ -abbrev EvPred (Time : Type*) [LinearOrder Time] := Event Time → Prop - -/-- A world-indexed predicate over events. The standard type for verb / - VP denotations in tense-aspect composition. -/ -abbrev EventPred (W Time : Type*) [LinearOrder Time] := W → Event Time → Prop - /-- Existential closure: ∃e. P(e). The fundamental step from event semantics to truth conditions. -/ -def existsClosure {Time : Type*} [LinearOrder Time] (P : EvPred Time) : Prop := +def existsClosure (P : Event Time → Prop) : Prop := ∃ e : Event Time, P e -/-- World-indexed existential closure: λw. ∃e. P(w)(e). -/ -def existsClosureW {W Time : Type*} [LinearOrder Time] - (P : EventPred W Time) : W → Prop := - λ w => ∃ e : Event Time, P w e - /-- Axioms for event part-of structure. Part-of is a partial order on events with temporal and sort constraints. -/ -class EventMereology (Time : Type*) [LinearOrder Time] where +class Mereology (Time : Type*) [LinearOrder Time] where /-- e₁ is a part of e₂ -/ partOf : Event Time → Event Time → Prop /-- Part-of is reflexive -/ @@ -105,8 +90,8 @@ class EventMereology (Time : Type*) [LinearOrder Time] where sort_preserved : ∀ e₁ e₂, partOf e₁ e₂ → e₁.sort = e₂.sort /-- Event mereology induces a Preorder. -/ -instance eventPreorder (Time : Type*) [LinearOrder Time] - [m : EventMereology Time] : Preorder (Event Time) where +instance preorder (Time : Type*) [LinearOrder Time] + [m : Mereology Time] : Preorder (Event Time) where le := m.partOf le_refl := m.refl le_trans := m.trans @@ -119,14 +104,12 @@ instance eventPreorder (Time : Type*) [LinearOrder Time] exhibits : Event Time → Prop /-- The manner of an event under a similarity criterion. - `mannerOf sim e` gives the manner class of `e` under `sim`. -/ -def mannerOf {Time : Type*} [LinearOrder Time] - (sim : Event Time → Event Time → Prop) (e : Event Time) : Manner Time := + `e.manner sim` gives the manner class of `e` under `sim`. -/ +def manner (e : Event Time) (sim : Event Time → Event Time → Prop) : Manner Time := ⟨sim e⟩ /-- Two events share a manner iff both satisfy the manner predicate. -/ -def Manner.sharedBy {Time : Type*} [LinearOrder Time] - (m : Manner Time) (e₁ e₂ : Event Time) : Prop := +def Manner.sharedBy (m : Manner Time) (e₁ e₂ : Event Time) : Prop := m.exhibits e₁ ∧ m.exhibits e₂ -end Semantics.Events +end Event diff --git a/Linglib/Semantics/Quotation/Demonstration.lean b/Linglib/Semantics/Quotation/Demonstration.lean index 13c9544ac..4033267eb 100644 --- a/Linglib/Semantics/Quotation/Demonstration.lean +++ b/Linglib/Semantics/Quotation/Demonstration.lean @@ -92,7 +92,6 @@ their own performance type. namespace Semantics.Quotation.Demonstration -open Semantics.Events open Semantics.ArgumentStructure (EventRel) open Core.Time diff --git a/Linglib/Semantics/Spatial/Trace.lean b/Linglib/Semantics/Spatial/Trace.lean index 9b05d2966..19168d8eb 100644 --- a/Linglib/Semantics/Spatial/Trace.lean +++ b/Linglib/Semantics/Spatial/Trace.lean @@ -32,7 +32,6 @@ All three use the same QUA/CUM pullback mechanism via `MereoDim`. because "towards the store" denotes a CUM set of paths. -/ -open Semantics.Events open Semantics.Events.CEM open Semantics.Spatial.Path open Features diff --git a/Linglib/Semantics/Tense/SOT/Decomposition.lean b/Linglib/Semantics/Tense/SOT/Decomposition.lean index 36db551c4..489cbfb5c 100644 --- a/Linglib/Semantics/Tense/SOT/Decomposition.lean +++ b/Linglib/Semantics/Tense/SOT/Decomposition.lean @@ -164,7 +164,6 @@ discourse-salient temporal antecedent. This explains the striking contrast: German: "Ich habe den Herd nicht ausgeschaltet." ✓ (present perfect ok) -/ open Semantics.Tense.TenseAspectComposition -open Semantics.Events open Semantics.Aspect /-- Kratzer's English simple past = PRESENT tense + PERFECT aspect. @@ -210,14 +209,14 @@ theorem english_deictic_german_anaphoric (n : ℕ) : present perfect have the SAME compositional semantics. They differ only in whether the PERF is morphologically fused or transparent. -/ theorem english_past_eq_presPerfSimple {W Time : Type*} [LinearOrder Time] - (V : EventPred W Time) (tc : Time) (w : W) : + (V : W → Event Time → Prop) (tc : Time) (w : W) : presPerfSimple V tc w ↔ ∃ pts : Core.Time.Interval Time, RB pts tc ∧ PRFV V w pts := Iff.rfl /-- German Preterit maps to `simplePast` from the pipeline: genuine past tense (existential over past times) + perfective aspect. -/ theorem german_preterit_eq_simplePast {W Time : Type*} [LinearOrder Time] - (V : EventPred W Time) (tc : Time) (w : W) : + (V : W → Event Time → Prop) (tc : Time) (w : W) : simplePast V tc w ↔ ∃ t : Time, t < tc ∧ PRFV V w (Core.Time.Interval.point t) := Iff.rfl diff --git a/Linglib/Semantics/Tense/TemporalAdverbials.lean b/Linglib/Semantics/Tense/TemporalAdverbials.lean index 97a58ad1e..92e110881 100644 --- a/Linglib/Semantics/Tense/TemporalAdverbials.lean +++ b/Linglib/Semantics/Tense/TemporalAdverbials.lean @@ -32,7 +32,6 @@ import Linglib.Semantics.Tense.TenseAspectComposition namespace Semantics.Tense.TemporalAdverbials open Core.Time -open Semantics.Events open Semantics.Aspect open Semantics.Tense.TenseAspectComposition @@ -168,7 +167,7 @@ theorem before_no_lb_constraint (tc : Time) : When the LB is pinned (durative adverbial), the U-perf reading entails the simple present via `u_perf_entails_simple_present`. -/ -theorem durative_licenses_u_perfect (V : EventPred W Time) (t₀ tc : Time) (w : W) +theorem durative_licenses_u_perfect (V : W → Event Time → Prop) (t₀ tc : Time) (w : W) (_h : t₀ ≤ tc) : presPerfProgXN V {t₀} tc w → simplePresent V tc w := u_perf_entails_simple_present V {t₀} tc w @@ -179,7 +178,7 @@ theorem durative_licenses_u_perfect (V : EventPred W Time) (t₀ tc : Time) (w : 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. -/ -theorem inclusive_no_u_license (V : EventPred W Time) (tc : Time) (w : W) : +theorem inclusive_no_u_license (V : W → Event Time → Prop) (tc : Time) (w : W) : presPerfProgXN V Set.univ tc w ↔ simplePresent V tc w := broad_focus_equiv V tc w diff --git a/Linglib/Semantics/Tense/TemporalConnectives/Basic.lean b/Linglib/Semantics/Tense/TemporalConnectives/Basic.lean index 0d207a01a..170891ee5 100644 --- a/Linglib/Semantics/Tense/TemporalConnectives/Basic.lean +++ b/Linglib/Semantics/Tense/TemporalConnectives/Basic.lean @@ -16,7 +16,7 @@ a sentence's truth. Two canonical patterns: sets (Level 1). This is the lower half of the three-level projection chain: ``` -Level 3: EvPred Time (event predicates) +Level 3: Event Time → Prop (event predicates) ↓ eventDenotation (see EventBridge.lean) Level 2: SentDenotation Time (interval sets — this file) ↓ timeTrace diff --git a/Linglib/Semantics/Tense/TemporalConnectives/EventBridge.lean b/Linglib/Semantics/Tense/TemporalConnectives/EventBridge.lean index b00230a25..0cbd1f0ae 100644 --- a/Linglib/Semantics/Tense/TemporalConnectives/EventBridge.lean +++ b/Linglib/Semantics/Tense/TemporalConnectives/EventBridge.lean @@ -8,7 +8,7 @@ import Linglib.Semantics.Events.Basic The projection from event predicates (Level 3) to interval sets (Level 2): ``` -Level 3: EvPred Time (event predicates — O&ST, future theories) +Level 3: Event Time → Prop (event predicates — O&ST, future theories) ↓ eventDenotation (this file) Level 2: SentDenotation Time (interval sets — Anscombe, Rett) ↓ timeTrace (Basic.lean) @@ -33,7 +33,6 @@ namespace Semantics.Tense.TemporalConnectives open Core.Time open Core.Time.Interval -open Semantics.Events variable {Time : Type*} [LinearOrder Time] @@ -47,7 +46,7 @@ variable {Time : Type*} [LinearOrder Time] interval-set semantics (Level 2). Every event-level temporal connective theory can be projected down to the interval level through this map, then compared with Anscombe and Rett. -/ -def eventDenotation (P : EvPred Time) : SentDenotation Time := +def eventDenotation (P : Event Time → Prop) : SentDenotation Time := { i | ∃ e, P e ∧ e.τ = i } -- ============================================================================ @@ -60,7 +59,7 @@ theorem eventDenotation_empty : ext i; simp [eventDenotation] /-- Nonempty predicate gives nonempty denotation (if there exists a witness). -/ -theorem eventDenotation_nonempty (P : EvPred Time) (e : Event Time) (he : P e) : +theorem eventDenotation_nonempty (P : Event Time → Prop) (e : Event Time) (he : P e) : e.τ ∈ eventDenotation P := ⟨e, he, rfl⟩ @@ -74,7 +73,7 @@ theorem eventDenotation_nonempty (P : EvPred Time) (e : Event Time) (he : P e) : This is the composition `timeTrace ∘ eventDenotation`, showing that the full projection chain Level 3 → Level 1 can be stated directly. -/ -theorem timeTrace_eventDenotation (P : EvPred Time) : +theorem timeTrace_eventDenotation (P : Event Time → Prop) : timeTrace (eventDenotation P) = { t | ∃ e, P e ∧ e.τ.contains t } := by ext t simp only [timeTrace, eventDenotation, Set.mem_setOf_eq] @@ -103,7 +102,7 @@ theorem eventDenotation_singleton (e₀ : Event Time) : Note: this is a subset, not equality, because `stativeDenotation i` contains all subintervals including those that might not be runtimes of any event. -/ -theorem eventDenotation_sub_stative (i : Interval Time) (P : EvPred Time) +theorem eventDenotation_sub_stative (i : Interval Time) (P : Event Time → Prop) (hP : ∀ e, P e → e.τ.subinterval i) : eventDenotation P ⊆ stativeDenotation i := by intro j ⟨e, he, hj⟩ diff --git a/Linglib/Semantics/Tense/TenseAspectComposition.lean b/Linglib/Semantics/Tense/TenseAspectComposition.lean index 3e2d2cd18..6675be5be 100644 --- a/Linglib/Semantics/Tense/TenseAspectComposition.lean +++ b/Linglib/Semantics/Tense/TenseAspectComposition.lean @@ -7,7 +7,7 @@ evaluation, following @cite{knick-sharf-2026}. ## The Pipeline ``` -EventPred ──[IMPF/PRFV]──▷ IntervalPred ──[PERF]──▷ PointPred ──[eval*]──▷ Prop +Event Time → Prop ──[IMPF/PRFV]──▷ IntervalPred ──[PERF]──▷ PointPred ──[eval*]──▷ Prop ``` The aspect chain produces `PointPred W Time = WorldTimeIndex W Time → Prop`. @@ -41,7 +41,6 @@ namespace Semantics.Tense.TenseAspectComposition open Core (WorldTimeIndex) open Core.Time -open Semantics.Events open Semantics.Aspect variable {W Time : Type*} [LinearOrder Time] @@ -73,33 +72,33 @@ def evalFut (p : PointPred W Time) (tc : Time) (w : W) : Prop := "John runs" = at speech time, ∃e with tc ⊂ τ(e) and V(e). Since atPoint evaluates at [tc, tc], this gives: ∃e, [tc,tc] ⊂ τ(e) ∧ V(e). -/ -def simplePresent (V : EventPred W Time) (tc : Time) (w : W) : Prop := +def simplePresent (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop := evalPres (IntervalPred.atPoint (IMPF V)) tc w /-- **Simple past**: PAST(PRFV(V).atPoint). "John ran" = ∃t < tc, ∃e with τ(e) ⊆ [t,t] and V(e). -/ -def simplePast (V : EventPred W Time) (tc : Time) (w : W) : Prop := +def simplePast (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop := evalPast (IntervalPred.atPoint (PRFV V)) tc w /-- **Present perfect progressive**: PRES(PERF(IMPF(V))). "John has been running" = at tc, ∃PTS with RB(PTS, tc) and IMPF(V)(PTS). -/ -def presPerfProg (V : EventPred W Time) (tc : Time) (w : W) : Prop := +def presPerfProg (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop := evalPres (PERF (IMPF V)) tc w /-- **Present perfect simple**: PRES(PERF(PRFV(V))). "John has run" = at tc, ∃PTS with RB(PTS, tc) and PRFV(V)(PTS). -/ -def presPerfSimple (V : EventPred W Time) (tc : Time) (w : W) : Prop := +def presPerfSimple (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop := evalPres (PERF (PRFV V)) tc w /-- **Present perfect progressive with Extended Now**: PRES(PERF_XN(IMPF(V), tᵣ)). @cite{knick-sharf-2026} eq. 39b: the U-perf reading. "John has been running (since Monday)" with domain restriction tᵣ on LB. -/ -def presPerfProgXN (V : EventPred W Time) (tᵣ : Set Time) (tc : Time) (w : W) : Prop := +def presPerfProgXN (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : Prop := evalPres (PERF_XN (IMPF V) tᵣ) tc w /-- **Past perfect progressive**: PAST(PERF(IMPF(V))). "John had been running" = ∃t < tc, PERF(IMPF(V))(w)(t). -/ -def pastPerfProg (V : EventPred W Time) (tc : Time) (w : W) : Prop := +def pastPerfProg (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop := evalPast (PERF (IMPF V)) tc w -- ════════════════════════════════════════════════════ @@ -107,14 +106,14 @@ def pastPerfProg (V : EventPred W Time) (tc : Time) (w : W) : Prop := -- ════════════════════════════════════════════════════ /-- Simple present unfolds to: ∃e, [tc,tc] ⊂ τ(e) ∧ V(w)(e). -/ -theorem simplePresent_unfold (V : EventPred W Time) (tc : Time) (w : W) : +theorem simplePresent_unfold (V : W → Event Time → Prop) (tc : Time) (w : W) : simplePresent V tc w ↔ ∃ e : Event Time, (Interval.point tc).properSubinterval e.τ ∧ V w e := by rfl /-- Present perfect progressive with XN unfolds to K&S eq. 39b: ∃PTS, ∃tLB ∈ tᵣ, LB(tLB, PTS) ∧ RB(PTS, tc) ∧ IMPF(V)(w)(PTS). -/ -theorem presPerfProgXN_unfold (V : EventPred W Time) (tᵣ : Set Time) +theorem presPerfProgXN_unfold (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : presPerfProgXN V tᵣ tc w ↔ ∃ pts : Interval Time, ∃ tLB ∈ tᵣ, @@ -135,7 +134,7 @@ theorem presPerfProgXN_unfold (V : EventPred W Time) (tᵣ : Set Time) Proof sketch: Given PERF_XN(IMPF(V), tᵣ)(w)(tc), we have PTS with RB(PTS, tc) and ∃e with PTS ⊂ τ(e). Since [tc,tc] ⊆ PTS (because tc = PTS.finish) and PTS ⊂ τ(e), we get [tc,tc] ⊂ τ(e). -/ -theorem u_perf_entails_simple_present (V : EventPred W Time) +theorem u_perf_entails_simple_present (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : presPerfProgXN V tᵣ tc w → simplePresent V tc w := by intro ⟨pts, _, _, _, hRB, e, ⟨⟨hS1, hS2⟩, hOr⟩, hV⟩ @@ -155,7 +154,7 @@ theorem u_perf_entails_simple_present (V : EventPred W Time) ∃e with [tc,tc] ⊂ τ(e). Construct PTS = [e.τ.start, tc]. Then LB(e.τ.start, PTS) ∈ Set.univ, RB(PTS, tc), and PTS ⊆ τ(e) with PTS ⊂ τ(e) (since tc < e.τ.finish by properSubinterval). -/ -theorem broad_focus_equiv (V : EventPred W Time) (tc : Time) (w : W) : +theorem broad_focus_equiv (V : W → Event Time → Prop) (tc : Time) (w : W) : presPerfProgXN V Set.univ tc w ↔ simplePresent V tc w := by constructor · exact u_perf_entails_simple_present V Set.univ tc w @@ -175,7 +174,7 @@ theorem broad_focus_equiv (V : EventPred W Time) (tc : Time) (w : W) : Proof sketch: Given PTS₁ = [tLB₁, tc] with e.τ ⊃ PTS₁ and V(e), construct PTS₂ = [tLB₂, tc]. Since tLB₁ < tLB₂ ≤ tc, PTS₂ is valid. PTS₂ ⊆ PTS₁ ⊆ τ(e), and PTS₂ ⊂ τ(e) follows from PTS₁ ⊂ τ(e). -/ -theorem earlier_lb_stronger_impf (V : EventPred W Time) +theorem earlier_lb_stronger_impf (V : W → Event Time → Prop) (tLB₁ tLB₂ : Time) (tc : Time) (w : W) (h : tLB₁ < tLB₂) (htc : tLB₂ ≤ tc) : PERF_XN (IMPF V) {tLB₁} ⟨w, tc⟩ → PERF_XN (IMPF V) {tLB₂} ⟨w, tc⟩ := by intro ⟨pts, tLB, htLB, hLB, hRB, e, ⟨⟨hS1, hS2⟩, _hOr⟩, hV⟩ @@ -205,7 +204,7 @@ theorem earlier_lb_stronger_impf (V : EventPred W Time) Proof sketch: Given PTS₂ = [tLB₂, tc] with τ(e) ⊆ PTS₂, construct PTS₁ = [tLB₁, tc]. Since tLB₁ < tLB₂, PTS₂ ⊆ PTS₁, so τ(e) ⊆ PTS₁. -/ -theorem later_lb_stronger_prfv (V : EventPred W Time) +theorem later_lb_stronger_prfv (V : W → Event Time → Prop) (tLB₁ tLB₂ : Time) (tc : Time) (w : W) (h : tLB₁ < tLB₂) : PERF_XN (PRFV V) {tLB₂} ⟨w, tc⟩ → PERF_XN (PRFV V) {tLB₁} ⟨w, tc⟩ := by intro ⟨pts, tLB, htLB, hLB, hRB, e, ⟨hS1, hS2⟩, hV⟩ @@ -231,14 +230,14 @@ theorem later_lb_stronger_prfv (V : EventPred W Time) but does NOT satisfy IMPF for PTS = [0, 4] (since [0,4] ⊄ [1,5]: the event hadn't started at time 0). -/ theorem earlier_lb_not_weaker_impf : - ¬ ∀ (V : EventPred Unit ℤ) (tLB₁ tLB₂ : ℤ) (tc : ℤ) (w : Unit), + ¬ ∀ (V : Unit → Event ℤ → Prop) (tLB₁ tLB₂ : ℤ) (tc : ℤ) (w : Unit), tLB₁ < tLB₂ → PERF_XN (IMPF V) {tLB₂} ⟨w, tc⟩ → PERF_XN (IMPF V) {tLB₁} ⟨w, tc⟩ := by intro hall -- Counterexample: event runtime [1,5], tLB₁=0, tLB₂=2, tc=4 -- sort defaults to .action; the proof doesn't reference .sort - let e₀ : Event ℤ := ⟨⟨1, 5, by omega⟩, .action⟩ - let V : EventPred Unit ℤ := fun _ e => e = e₀ + let e₀ : Event ℤ := ⟨⟨1, 5, by omega⟩, .dynamic⟩ + let V : Unit → Event ℤ → Prop := fun _ e => e = e₀ -- Premise: PERF_XN(IMPF(V), {2})(⟨(), 4⟩) -- PTS = [2,4], event [1,5]: [2,4] ⊂ [1,5] ✓ have prem : PERF_XN (IMPF V) {(2 : ℤ)} ⟨(), 4⟩ := by diff --git a/Linglib/Studies/Anscombe1964.lean b/Linglib/Studies/Anscombe1964.lean index 717b8dc36..2222ecded 100644 --- a/Linglib/Studies/Anscombe1964.lean +++ b/Linglib/Studies/Anscombe1964.lean @@ -260,7 +260,7 @@ true when no Q-event exists). The same ` /` pattern present in ## Level -**Level 3 (event predicates)**: operates on `EvPred Time`. Projects to +**Level 3 (event predicates)**: operates on `Event Time → Prop`. Projects to Level 2 via `eventDenotation` (EventBridge.lean). ## Cross-Level Comparison @@ -275,7 +275,6 @@ namespace Semantics.Tense.TemporalConnectives open Core.Time open Core.Time.Interval -open Semantics.Events variable {Time : Type*} [LinearOrder Time] @@ -290,7 +289,7 @@ variable {Time : Type*} [LinearOrder Time] the main event's runtime. This is @cite{anscombe-1964}'s `` lifted from points to event runtimes. -/ -def AnscombeEvent.after (P Q : EvPred Time) : Prop := +def AnscombeEvent.after (P Q : Event Time → Prop) : Prop := ∃ e₁ e₂ : Event Time, P e₁ ∧ Q e₂ ∧ e₂.τ.precedes e₁.τ /-- Event-level *before*: `e`[P(e`) ` `e`[Q(e`) ` `(e`) ` `(e`)]]. @@ -301,7 +300,7 @@ def AnscombeEvent.after (P Q : EvPred Time) : Prop := non-veridical. This is @cite{anscombe-1964}'s `` lifted from points to event runtimes. -/ -def AnscombeEvent.before (P Q : EvPred Time) : Prop := +def AnscombeEvent.before (P Q : Event Time → Prop) : Prop := ∃ e₁ : Event Time, P e₁ ∧ ∀ e₂ : Event Time, Q e₂ → e₁.τ.precedes e₂.τ -- ============================================================================ @@ -312,13 +311,13 @@ def AnscombeEvent.before (P Q : EvPred Time) : Prop := This follows directly from the double-existential structure: the definition asserts `e`, Q(e`), which witnesses the complement. -/ -theorem AnscombeEvent.after_veridical (P Q : EvPred Time) : +theorem AnscombeEvent.after_veridical (P Q : Event Time → Prop) : AnscombeEvent.after P Q → ∃ e : Event Time, Q e := by rintro ⟨_, e₂, _, hq, _⟩ exact ⟨e₂, hq⟩ /-- *After* is veridical w.r.t. the main clause too: both events must exist. -/ -theorem AnscombeEvent.after_veridical_main (P Q : EvPred Time) : +theorem AnscombeEvent.after_veridical_main (P Q : Event Time → Prop) : AnscombeEvent.after P Q → ∃ e : Event Time, P e := by rintro ⟨e₁, _, hp, _, _⟩ exact ⟨e₁, hp⟩ @@ -329,13 +328,13 @@ theorem AnscombeEvent.after_veridical_main (P Q : EvPred Time) : Concretely: if P has a witness and Q is empty, then `e`, Q(e`) `... is vacuously true. -/ theorem AnscombeEvent.before_nonveridical : - ∃ (P Q : EvPred ℤ), AnscombeEvent.before P Q ∧ ¬∃ e : Event ℤ, Q e := by - refine ⟨fun e => e = ⟨⟨0, 1, by omega⟩, .action⟩, fun _ => False, ?_, ?_⟩ - · exact ⟨⟨⟨0, 1, by omega⟩, .action⟩, rfl, fun _ h => h.elim⟩ + ∃ (P Q : Event ℤ → Prop), AnscombeEvent.before P Q ∧ ¬∃ e : Event ℤ, Q e := by + refine ⟨fun e => e = ⟨⟨0, 1, by omega⟩, .dynamic⟩, fun _ => False, ?_, ?_⟩ + · exact ⟨⟨⟨0, 1, by omega⟩, .dynamic⟩, rfl, fun _ h => h.elim⟩ · rintro ⟨_, h⟩; exact h /-- *Before* is still veridical w.r.t. its main clause: the P-event must exist. -/ -theorem AnscombeEvent.before_veridical_main (P Q : EvPred Time) : +theorem AnscombeEvent.before_veridical_main (P Q : Event Time → Prop) : AnscombeEvent.before P Q → ∃ e : Event Time, P e := by rintro ⟨e₁, hp, _⟩ exact ⟨e₁, hp⟩ @@ -349,7 +348,7 @@ theorem AnscombeEvent.before_veridical_main (P Q : EvPred Time) : Proof: from `e`.`.precedes e`.` (i.e., `e`.`.finish < e`.`.start`), take `t = e`.`.start` and `t' = e`.`.finish`. -/ -theorem AnscombeEvent.after_implies_anscombe (P Q : EvPred Time) : +theorem AnscombeEvent.after_implies_anscombe (P Q : Event Time → Prop) : AnscombeEvent.after P Q → Anscombe.after (eventDenotation P) (eventDenotation Q) := by rintro ⟨e₁, e₂, hp, hq, hprec⟩ refine ⟨e₁.τ.start, ?_, e₂.τ.finish, ?_, hprec⟩ @@ -364,7 +363,7 @@ theorem AnscombeEvent.after_implies_anscombe (P Q : EvPred Time) : `t = e`.`.finish`. For any `t' ` timeTrace(eventDenotation Q)`, some `e`` has `Q(e`)` and `e`.`.start ` t'`, so `t = e`.`.finish < e`.`.start ` t'`. -/ -theorem AnscombeEvent.before_implies_anscombe (P Q : EvPred Time) : +theorem AnscombeEvent.before_implies_anscombe (P Q : Event Time → Prop) : AnscombeEvent.before P Q → Anscombe.before (eventDenotation P) (eventDenotation Q) := by rintro ⟨e₁, hp, hall⟩ refine ⟨e₁.τ.finish, ?_, ?_⟩ @@ -389,13 +388,13 @@ theorem AnscombeEvent.before_implies_anscombe (P Q : EvPred Time) : The point-level theory sees a point in A before all of B; the event-level theory requires the entire A-runtime to precede the entire B-runtime. -/ theorem anscombe_before_not_implies_event : - ¬∀ (P Q : EvPred ℤ), + ¬∀ (P Q : Event ℤ → Prop), Anscombe.before (eventDenotation P) (eventDenotation Q) → AnscombeEvent.before P Q := by intro h - let eP : Event ℤ := ⟨⟨1, 5, by omega⟩, .action⟩ - let eQ : Event ℤ := ⟨⟨3, 8, by omega⟩, .action⟩ - let P : EvPred ℤ := fun e => e = eP - let Q : EvPred ℤ := fun e => e = eQ + let eP : Event ℤ := ⟨⟨1, 5, by omega⟩, .dynamic⟩ + let eQ : Event ℤ := ⟨⟨3, 8, by omega⟩, .dynamic⟩ + let P : Event ℤ → Prop := fun e => e = eP + let Q : Event ℤ → Prop := fun e => e = eQ have hansc : Anscombe.before (eventDenotation P) (eventDenotation Q) := by refine ⟨1, ?_, ?_⟩ · rw [timeTrace_eventDenotation] @@ -417,13 +416,13 @@ theorem anscombe_before_not_implies_event : - Anscombe: t=5, t'=1, 1 < 5. ` - Event-level: `(eQ).finish = 8 > 5 = `(eP).start, so `precedes. ` -/ theorem anscombe_after_not_implies_event : - ¬∀ (P Q : EvPred ℤ), + ¬∀ (P Q : Event ℤ → Prop), Anscombe.after (eventDenotation P) (eventDenotation Q) → AnscombeEvent.after P Q := by intro h - let eP : Event ℤ := ⟨⟨5, 5, by omega⟩, .action⟩ - let eQ : Event ℤ := ⟨⟨1, 8, by omega⟩, .action⟩ - let P : EvPred ℤ := fun e => e = eP - let Q : EvPred ℤ := fun e => e = eQ + let eP : Event ℤ := ⟨⟨5, 5, by omega⟩, .dynamic⟩ + let eQ : Event ℤ := ⟨⟨1, 8, by omega⟩, .dynamic⟩ + let P : Event ℤ → Prop := fun e => e = eP + let Q : Event ℤ → Prop := fun e => e = eQ have hansc : Anscombe.after (eventDenotation P) (eventDenotation Q) := by refine ⟨5, ?_, 1, ?_, by omega⟩ · rw [timeTrace_eventDenotation] diff --git a/Linglib/Studies/Bhadra2024.lean b/Linglib/Studies/Bhadra2024.lean index 2c0e288a4..5d54b686b 100644 --- a/Linglib/Studies/Bhadra2024.lean +++ b/Linglib/Studies/Bhadra2024.lean @@ -230,7 +230,6 @@ theorem pc_roots_allow_restitutive_again : section CompositionalVRO -open Semantics.Events open Core.Time variable {Entity State Time : Type*} [LinearOrder Time] @@ -554,8 +553,7 @@ theorem break_end_to_end : section CompositionalExamples -open Semantics.Events Core.Time - +open Core.Time /-- VRO for "fold": PFC verb with multi-membered outcome set. The parchment can end up in any of several states after folding. Outcome set = {slightlyCreased, folded, tightlyFolded} (3 members). @@ -655,17 +653,16 @@ end CompositionalExamples section StressTests -open Semantics.Events Core.Time - +open Core.Time /-- Event from t=0 to t=5 (the base event, e.g. folding). -/ private def ev₁ : Event ℤ where runtime := ⟨0, 5, by omega⟩ - sort := .action + sort := .dynamic /-- Event from t=10 to t=15 (the reversal/restitution event, e.g. unfolding). -/ private def ev₂ : Event ℤ where runtime := ⟨10, 15, by omega⟩ - sort := .action + sort := .dynamic /-- ev₁ temporally precedes ev₂: τ(ev₁).finish < τ(ev₂).start. -/ private theorem ev₁_precedes_ev₂ : (Event.τ ev₁).precedes (Event.τ ev₂) := by @@ -707,7 +704,7 @@ theorem fold_un_satisfiable : /-- Event from t=20 to t=25 (the re-event, e.g. re-folding). -/ private def ev₃ : Event ℤ where runtime := ⟨20, 25, by omega⟩ - sort := .action + sort := .dynamic /-- State function for fold/unfold/refold scenario: - t ≤ 0: flat (pre-state of first fold) diff --git a/Linglib/Studies/CarianiSantorioWellwood2024.lean b/Linglib/Studies/CarianiSantorioWellwood2024.lean index 758f24335..940dba72e 100644 --- a/Linglib/Studies/CarianiSantorioWellwood2024.lean +++ b/Linglib/Studies/CarianiSantorioWellwood2024.lean @@ -410,9 +410,9 @@ the others wire through substrate theorems directly. -/ theorem confidence_comparative_reduces {E : Type*} {Time : Type*} [LinearOrder Time] {frame : Semantics.ArgumentStructure.ThematicFrame E Time} - {P : Semantics.Events.EvPred Time} - {μ : Semantics.Events.Event Time → ℚ} - {a b : E} {sa sb : Semantics.Events.Event Time} + {P : Event Time → Prop} + {μ : Event Time → ℚ} + {a b : E} {sa sb : Event Time} (ha : frame.holder a sa ∧ P sa) (ha_unique : ∀ s, frame.holder a s → P s → s = sa) (hb : frame.holder b sb ∧ P sb) diff --git a/Linglib/Studies/Condoravdi2002.lean b/Linglib/Studies/Condoravdi2002.lean index 82153e5c0..8349ad8a0 100644 --- a/Linglib/Studies/Condoravdi2002.lean +++ b/Linglib/Studies/Condoravdi2002.lean @@ -43,7 +43,6 @@ namespace Condoravdi2002 open Core.Time open Features (Dynamicity) -open Semantics.Events open Semantics.Aspect open HistoricalAlternatives open Semantics.Modality (TemporalPerspective TemporalOrientation) @@ -64,17 +63,17 @@ variable {W Time : Type*} [LinearOrder Time] /-- Eventive AT, `AT(t, w, P)` for eventive `P`: an event of `P` whose runtime is included in `t`. Definitionally Klein's perfective `Aspect.PRFV`; Condoravdi writes the conjuncts predicate-first, `PRFV` relation-first. -/ -def atEvent (P : EventPred W Time) : IntervalPred W Time := PRFV P +def atEvent (P : W → Event Time → Prop) : IntervalPred W Time := PRFV P /-- Stative AT, `AT(t, w, P)` for stative `P`: an event of `P` whose runtime merely overlaps `t`. Weaker than `Aspect.IMPF` (proper inclusion), so it has no Aspect counterpart and stays a local definition. -/ -def atState (P : EventPred W Time) : IntervalPred W Time := +def atState (P : W → Event Time → Prop) : IntervalPred W Time := fun w t => ∃ e : Event Time, e.τ.overlaps t ∧ P w e /-- The AT relation, dispatching on eventuality sort. The paper's third case - (properties of times) is vacuous here: `EventPred` is eventuality-valued. -/ -def at' (sort : Dynamicity) (P : EventPred W Time) (w : W) (t : Interval Time) : + (properties of times) is vacuous here: the event predicate is eventuality-valued. -/ +def at' (sort : Dynamicity) (P : W → Event Time → Prop) (w : W) (t : Interval Time) : Prop := match sort with | .dynamic => atEvent P w t @@ -82,20 +81,20 @@ def at' (sort : Dynamicity) (P : EventPred W Time) (w : W) (t : Interval Time) : /-- Eventive instantiation is stronger than stative: an event included in the interval certainly overlaps it. -/ -theorem atState_of_atEvent (P : EventPred W Time) (w : W) (t : Interval Time) +theorem atState_of_atEvent (P : W → Event Time → Prop) (w : W) (t : Interval Time) (h : atEvent P w t) : atState P w t := let ⟨e, hSub, hP⟩ := h ⟨e, Interval.subinterval_overlaps hSub, hP⟩ /-- `atEvent` is monotone in the reference interval. -/ -theorem atEvent_mono {t₁ t₂ : Interval Time} (P : EventPred W Time) (w : W) +theorem atEvent_mono {t₁ t₂ : Interval Time} (P : W → Event Time → Prop) (w : W) (hSub : t₁.subinterval t₂) (h : atEvent P w t₁) : atEvent P w t₂ := let ⟨e, heSub, hP⟩ := h ⟨e, ⟨le_trans hSub.1 heSub.1, le_trans heSub.2 hSub.2⟩, hP⟩ /-- `atState` is monotone in the reference interval: overlap with a subinterval entails overlap with the containing interval. -/ -theorem atState_mono {t₁ t₂ : Interval Time} (P : EventPred W Time) (w : W) +theorem atState_mono {t₁ t₂ : Interval Time} (P : W → Event Time → Prop) (w : W) (hSub : t₁.subinterval t₂) (h : atState P w t₁) : atState P w t₂ := let ⟨e, hOv, hP⟩ := h ⟨e, ⟨le_trans hOv.1 hSub.2, le_trans hSub.1 hOv.2⟩, hP⟩ @@ -109,16 +108,16 @@ constraints are expressed directly: for events the runtime starts at or after /-- Event instantiated in the future of `t` — `AT([t, _), w, P)` for eventive `P`: the event starts at or after `t`. -/ -def atEventForward (P : EventPred W Time) (w : W) (t : Time) : Prop := +def atEventForward (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∃ e : Event Time, t ≤ e.τ.start ∧ P w e /-- State instantiated through `t` — `AT([t, _), w, P)` for stative `P`: the state persists at or past `t`. -/ -def atStateForward (P : EventPred W Time) (w : W) (t : Time) : Prop := +def atStateForward (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∃ e : Event Time, t ≤ e.τ.finish ∧ P w e /-- Forward AT, dispatching on eventuality sort. -/ -def atForward (sort : Dynamicity) (P : EventPred W Time) (w : W) (t : Time) : +def atForward (sort : Dynamicity) (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := match sort with | .dynamic => atEventForward P w t @@ -126,19 +125,19 @@ def atForward (sort : Dynamicity) (P : EventPred W Time) (w : W) (t : Time) : /-- Forward stative is weaker than forward eventive: if the event starts at or after `t`, its finish is also at or after `t`. -/ -theorem atStateForward_of_atEventForward (P : EventPred W Time) (w : W) +theorem atStateForward_of_atEventForward (P : W → Event Time → Prop) (w : W) (t : Time) (h : atEventForward P w t) : atStateForward P w t := let ⟨e, hStart, hP⟩ := h ⟨e, le_trans hStart e.τ.valid, hP⟩ /-- `atEvent` at a point `[t, t]` implies `atEventForward` at `t`. -/ -theorem atEventForward_of_atEvent_point (P : EventPred W Time) (w : W) (t : Time) +theorem atEventForward_of_atEvent_point (P : W → Event Time → Prop) (w : W) (t : Time) (h : atEvent P w (Interval.point t)) : atEventForward P w t := let ⟨e, hSub, hP⟩ := h ⟨e, hSub.1, hP⟩ /-- `atState` at a point `[t, t]` implies `atStateForward` at `t`. -/ -theorem atStateForward_of_atState_point (P : EventPred W Time) (w : W) (t : Time) +theorem atStateForward_of_atState_point (P : W → Event Time → Prop) (w : W) (t : Time) (h : atState P w (Interval.point t)) : atStateForward P w t := let ⟨e, hOv, hP⟩ := h ⟨e, hOv.2, hP⟩ @@ -152,13 +151,13 @@ variable {W Time : Type*} [LinearOrder Time] /-- Present tense: instantiates a property at the utterance time. The temporal anchor is a single point. -/ -def pres (sort : Dynamicity) (P : EventPred W Time) (t : Time) +def pres (sort : Dynamicity) (P : W → Event Time → Prop) (t : Time) (w : W) : Prop := at' sort P w (Interval.point t) /-- Perfect: shifts evaluation to a prior time. There is some `t' < t` at which the property holds. -/ -def perf (sort : Dynamicity) (P : EventPred W Time) (w : W) +def perf (sort : Dynamicity) (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∃ t' : Time, t' < t ∧ at' sort P w (Interval.point t') @@ -175,26 +174,26 @@ prospective operator; `may_of_mayCore_dynamic` relates the two. -/ /-- Modal possibility core: ∃ w' ∈ MB(w,t), the prejacent holds at the point `t` in `w'`. No forward expansion. -/ def mayCore (MB : W → Time → Set W) (sort : Dynamicity) - (P : EventPred W Time) (w : W) (t : Time) : Prop := + (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∃ w' ∈ MB w t, at' sort P w' (Interval.point t) /-- MAY/MIGHT: existential quantification over the modal base, with forward temporal expansion. The English modal lexicalizes the prospective choice (@cite{condoravdi-2002}). -/ def may (MB : W → Time → Set W) (sort : Dynamicity) - (P : EventPred W Time) (w : W) (t : Time) : Prop := + (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∃ w' ∈ MB w t, atForward sort P w' t /-- Modal necessity core: ∀ w' ∈ MB(w,t), the prejacent holds at the point `t` in `w'`. No forward expansion. -/ def wollCore (MB : W → Time → Set W) (sort : Dynamicity) - (P : EventPred W Time) (w : W) (t : Time) : Prop := + (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∀ w' ∈ MB w t, at' sort P w' (Interval.point t) /-- WOLL: universal quantification over the modal base, with forward temporal expansion. The untensed modal underlying *will* / *would*. -/ def woll (MB : W → Time → Set W) (sort : Dynamicity) - (P : EventPred W Time) (w : W) (t : Time) : Prop := + (P : W → Event Time → Prop) (w : W) (t : Time) : Prop := ∀ w' ∈ MB w t, atForward sort P w' t /-- For dynamic predicates, `mayCore` implies `may`: forward expansion @@ -202,7 +201,7 @@ def woll (MB : W → Time → Set W) (sort : Dynamicity) pointwise instantiation gives an event whose start lies at or after `t`, which is exactly what `atEventForward` requires. -/ theorem may_of_mayCore_dynamic (MB : W → Time → Set W) - (P : EventPred W Time) (w : W) (t : Time) + (P : W → Event Time → Prop) (w : W) (t : Time) (h : mayCore MB .dynamic P w t) : may MB .dynamic P w t := by obtain ⟨w', hMem, hAt⟩ := h refine ⟨w', hMem, ?_⟩ @@ -211,7 +210,7 @@ theorem may_of_mayCore_dynamic (MB : W → Time → Set W) /-- For stative predicates, `mayCore` implies `may`: pointwise state overlap entails forward state persistence at the point. -/ theorem may_of_mayCore_stative (MB : W → Time → Set W) - (P : EventPred W Time) (w : W) (t : Time) + (P : W → Event Time → Prop) (w : W) (t : Time) (h : mayCore MB .stative P w t) : may MB .stative P w t := by obtain ⟨w', hMem, hAt⟩ := h refine ⟨w', hMem, ?_⟩ @@ -227,7 +226,7 @@ counterfactual modality. The trivial single-operator examples /-- "He may have won" — *epistemic* reading. The modal scopes over the perfect (PRES > MAY > PERF). Modal base evaluated at `t`; the perfect back-shifts inside the modal's scope. -/ -def mayEpistemic (MB : W → Time → Set W) (P : EventPred W Time) +def mayEpistemic (MB : W → Time → Set W) (P : W → Event Time → Prop) (t : Time) (w : W) : Prop := ∃ w' ∈ MB w t, perf .dynamic P w' t @@ -236,7 +235,7 @@ def mayEpistemic (MB : W → Time → Set W) (P : EventPred W Time) base's evaluation point to a past `t'`; the modal then quantifies over worlds compatible with the past, with the property in `[t', _)`. -/ -def mightCounterfactual (MB : W → Time → Set W) (P : EventPred W Time) +def mightCounterfactual (MB : W → Time → Set W) (P : W → Event Time → Prop) (t : Time) (w : W) : Prop := ∃ t' : Time, t' < t ∧ may MB .dynamic P w t' @@ -284,7 +283,7 @@ variable {W Time : Type*} [LinearOrder Time] point of instantiation gives a degenerate PTS `[t', t']` right-bounded at `t`. -/ theorem perf_eventive_implies_perfSimple - (P : EventPred W Time) (w : W) (t : Time) + (P : W → Event Time → Prop) (w : W) (t : Time) (h : perf .dynamic P w t) : perfSimple P ⟨w, t⟩ := by obtain ⟨t', hlt, e, hSub, hP⟩ := h exact ⟨⟨t', t, le_of_lt hlt⟩, rfl, e, @@ -292,7 +291,7 @@ theorem perf_eventive_implies_perfSimple /-- @cite{klein-1994}'s imperfective entails Condoravdi's stative AT: proper inclusion of the reference interval in the event runtime implies overlap. -/ -theorem atState_of_impf (P : EventPred W Time) (w : W) (t : Interval Time) +theorem atState_of_impf (P : W → Event Time → Prop) (w : W) (t : Interval Time) (h : IMPF P w t) : atState P w t := let ⟨e, hPSub, hP⟩ := h have hOv : e.τ.overlaps t := @@ -326,7 +325,7 @@ theorem modal_over_perf_blocks_metaphysical (history : HistoricalAlternatives W Time) (MB : W → Time → Set W) (cg : Set W) (now : Time) - (P : EventPred W Time) + (P : W → Event Time → Prop) (hMB : ∀ w ∈ cg, ∀ w' ∈ MB w now, histEquiv history now w w') (hSettled : settled history cg now (λ w => perf .dynamic P w now)) : ¬ diverse MB cg now (λ w => perf .dynamic P w now) := diff --git a/Linglib/Studies/Cruse1973.lean b/Linglib/Studies/Cruse1973.lean index 6c72e7db8..4626db04d 100644 --- a/Linglib/Studies/Cruse1973.lean +++ b/Linglib/Studies/Cruse1973.lean @@ -43,7 +43,6 @@ and is marginal for others. namespace Cruse1973 -open Semantics.Events open Semantics.ArgumentStructure open Semantics.Causation.CoerciveImplication open Features (Causative) @@ -190,7 +189,7 @@ theorem agent_is_agentive_subfeature {Entity Time : Type*} [LinearOrder Time] [ax : ThematicAxioms Entity Time frame] (x : Entity) (e : Event Time) (h : frame.agent x e) : - profile.hasAgentive x e ∧ e.sort = .action := + profile.hasAgentive x e ∧ e.sort = .dynamic := ⟨link.agent_implies_agentive x e h, ax.agent_selects_action x e h⟩ -- ════════════════════════════════════════════════════ @@ -287,10 +286,10 @@ theorem make_lexicalizes_sufficient_initiative : role, which requires e.sort =.action. -/ theorem stative_can_pass_doTest : ∃ (profile : AgentivityProfile Unit ℤ) (x : Unit) (e : Event ℤ), - e.sort = .state ∧ passesDoTest x e profile := by + e.sort = .stative ∧ passesDoTest x e profile := by -- Witness: a profile where () has volitive in a stative event refine ⟨⟨λ _ _ => True, λ _ _ => False, λ _ _ => False, λ _ _ => False⟩, - (), ⟨⟨0, 10, by omega⟩, .state⟩, rfl, ?_⟩ + (), ⟨⟨0, 10, by omega⟩, .stative⟩, rfl, ?_⟩ exact Or.inl trivial /-- Parsons' `agent_selects_action` is NOT contradicted by stative @@ -307,7 +306,7 @@ theorem agent_selects_action_consistent {Entity Time : Type*} [LinearOrder Time] {frame : ThematicFrame Entity Time} [ax : ThematicAxioms Entity Time frame] (x : Entity) (e : Event Time) - (hState : e.sort = .state) + (hState : e.sort = .stative) (hAgent : frame.agent x e) : False := by have hAction := ax.agent_selects_action x e hAgent diff --git a/Linglib/Studies/Giannakidou2002.lean b/Linglib/Studies/Giannakidou2002.lean index 4a12fa1df..72bdbdc1b 100644 --- a/Linglib/Studies/Giannakidou2002.lean +++ b/Linglib/Studies/Giannakidou2002.lean @@ -42,7 +42,7 @@ Uses `Aspect.Core.UNBOUNDED` (= non-strict IMPF, @cite{pancheva-2003}) projected to `SentDenotation` for the imperfective denotation: ``` -EventPred Unit Time ──[UNBOUNDED]──▷ IntervalPred ──[fix w=()]──▷ SentDenotation +Unit → Event Time → Prop ──[UNBOUNDED]──▷ IntervalPred ──[fix w=()]──▷ SentDenotation ``` The key property — subinterval-closure — holds for both `UNBOUNDED` (⊆) and @@ -68,7 +68,6 @@ namespace Giannakidou2002 open Core.Time open Core.Time.Interval -open Semantics.Events open Semantics.Aspect open Semantics.Tense.TemporalConnectives @@ -84,7 +83,7 @@ variable {Time : Type*} [LinearOrder Time] rather than `IMPF` (which requires strict ⊂) because the homogeneity argument is identical and the non-strict version connects cleanly to `stativeDenotation`. -/ -abbrev impfDen (P : EventPred Unit Time) : SentDenotation Time := +abbrev impfDen (P : Unit → Event Time → Prop) : SentDenotation Time := { i | UNBOUNDED P () i } /-- PRFV denotation: the set of exact event runtimes. @@ -92,7 +91,7 @@ abbrev impfDen (P : EventPred Unit Time) : SentDenotation Time := the runtime: TSit ⊆ TT), this gives the τ-image {τ(e) | P(e)} — the interval set that directly characterizes the event's temporal extent. This matches the `eventDenotation` pattern from `EventBridge.lean`. -/ -def prfvDen (P : EventPred Unit Time) : SentDenotation Time := +def prfvDen (P : Unit → Event Time → Prop) : SentDenotation Time := { i | ∃ e : Event Time, P () e ∧ e.τ = i } -- ============================================================================ @@ -111,7 +110,7 @@ def IsHomogeneous (D : SentDenotation Time) : Prop := of the main clause of durative *until*. The imperfective viewpoint provides this automatically: since the event extends beyond any reference interval, every sub-window into the event is equally valid. -/ -theorem impfDen_subinterval_closed (P : EventPred Unit Time) +theorem impfDen_subinterval_closed (P : Unit → Event Time → Prop) (t : Interval Time) (ht : t ∈ impfDen P) (t' : Interval Time) (ht' : t'.subinterval t) : t' ∈ impfDen P := by @@ -119,7 +118,7 @@ theorem impfDen_subinterval_closed (P : EventPred Unit Time) exact ⟨e, ⟨le_trans hSub.1 ht'.1, le_trans ht'.2 hSub.2⟩, hP⟩ /-- IMPF denotation contains the event runtime itself (the maximal interval). -/ -theorem impfDen_contains_runtime (P : EventPred Unit Time) +theorem impfDen_contains_runtime (P : Unit → Event Time → Prop) (e : Event Time) (hP : P () e) : e.τ ∈ impfDen P := ⟨e, subinterval_refl _, hP⟩ @@ -133,12 +132,12 @@ theorem impfDen_contains_runtime (P : EventPred Unit Time) This is why perfective clauses cannot be main clauses of durative *until*: they lack the homogeneity that *until* requires. -/ theorem prfvDen_not_subinterval_closed : - ¬ ∀ (P : EventPred Unit ℤ) (t : Interval ℤ), + ¬ ∀ (P : Unit → Event ℤ → Prop) (t : Interval ℤ), t ∈ prfvDen P → ∀ t', t'.subinterval t → t' ∈ prfvDen P := by intro h -- sort defaults to .action; the proof doesn't reference .sort - let e₀ : Event ℤ := ⟨⟨0, 5, by omega⟩, .action⟩ - let P : EventPred Unit ℤ := fun _ e => e = e₀ + let e₀ : Event ℤ := ⟨⟨0, 5, by omega⟩, .dynamic⟩ + let P : Unit → Event ℤ → Prop := fun _ e => e = e₀ let sub : Interval ℤ := ⟨1, 3, by omega⟩ have hrt : e₀.τ ∈ prfvDen P := ⟨e₀, rfl, rfl⟩ have hsub : sub.subinterval e₀.τ := by @@ -157,7 +156,7 @@ theorem prfvDen_not_subinterval_closed : -- ============================================================================ /-- IMPF denotation is homogeneous — wide scope is available. -/ -theorem impfDen_homogeneous (P : EventPred Unit Time) : +theorem impfDen_homogeneous (P : Unit → Event Time → Prop) : IsHomogeneous (impfDen P) := impfDen_subinterval_closed P @@ -165,7 +164,7 @@ theorem impfDen_homogeneous (P : EventPred Unit Time) : available. This is derived from the subinterval-closure failure, not stipulated as a Bool field. -/ theorem prfvDen_not_always_homogeneous : - ¬ ∀ (P : EventPred Unit ℤ), IsHomogeneous (prfvDen P) := by + ¬ ∀ (P : Unit → Event ℤ → Prop), IsHomogeneous (prfvDen P) := by intro h exact prfvDen_not_subinterval_closed fun P t ht t' ht' => h P t ht t' ht' @@ -175,9 +174,9 @@ theorem prfvDen_not_always_homogeneous : PRFV's failure of subinterval-closure, not from a stipulated constraint. -/ theorem scope_pattern_derived : -- IMPF always permits wide scope (homogeneous) - (∀ (P : EventPred Unit Time), IsHomogeneous (impfDen P)) ∧ + (∀ (P : Unit → Event Time → Prop), IsHomogeneous (impfDen P)) ∧ -- PRFV does not always permit wide scope (not always homogeneous) - ¬ (∀ (P : EventPred Unit ℤ), IsHomogeneous (prfvDen P)) := + ¬ (∀ (P : Unit → Event ℤ → Prop), IsHomogeneous (prfvDen P)) := ⟨impfDen_homogeneous, prfvDen_not_always_homogeneous⟩ -- ============================================================================ @@ -197,7 +196,7 @@ theorem impfDen_singleton_eq_stativeDenotation constructor · rintro ⟨e, hSub, rfl⟩; exact hSub -- sort defaults to .action; the proof doesn't reference .sort - · intro h; exact ⟨⟨i, .action⟩, h, rfl⟩ + · intro h; exact ⟨⟨i, .dynamic⟩, h, rfl⟩ /-- For a single event, the PRFV denotation is exactly the accomplishment denotation (singleton containing just the runtime). -/ @@ -211,7 +210,7 @@ theorem prfvDen_singleton_eq_accomplishmentDenotation constructor · rintro ⟨e, rfl, rfl⟩; rfl -- sort defaults to .action; the proof doesn't reference .sort - · intro h; exact ⟨⟨i, .action⟩, rfl, h.symm⟩ + · intro h; exact ⟨⟨i, .dynamic⟩, rfl, h.symm⟩ -- ============================================================================ -- § 5: Time Traces Coincide @@ -223,7 +222,7 @@ theorem prfvDen_singleton_eq_accomplishmentDenotation This is why Karttunen's Level 1 (point-set) definitions cannot distinguish imperfective from perfective clauses — the difference is only visible at Level 2 (interval sets). -/ -theorem timeTrace_impf_eq_prfv (P : EventPred Unit Time) : +theorem timeTrace_impf_eq_prfv (P : Unit → Event Time → Prop) : timeTrace (impfDen P) = timeTrace (prfvDen P) := by ext t simp only [timeTrace, prfvDen, UNBOUNDED, Set.mem_setOf_eq, Event.τ] @@ -248,7 +247,7 @@ theorem timeTrace_impf_eq_prfv (P : EventPred Unit Time) : Available when A is imperfective: the main clause denotes a homogeneous interval set via IMPF, so *until* can take it as an argument. Negation scopes over the entire *until*-clause. -/ -def wideScopeNotUntil (A : EventPred Unit Time) (B : SentDenotation Time) : Prop := +def wideScopeNotUntil (A : Unit → Event Time → Prop) (B : SentDenotation Time) : Prop := ¬ Karttunen.when_ (impfDen A) B /-- **Narrow-scope negation** under *until* (= Karttunen's ¬*before*): @@ -260,13 +259,13 @@ def wideScopeNotUntil (A : EventPred Unit Time) (B : SentDenotation Time) : Prop This is the only reading available with perfective main clauses: since PRFV gives a bounded event, *until* reduces to temporal ordering and negation gives Karttunen's notUntil = ¬before. -/ -def narrowScopeNotUntil (A : EventPred Unit Time) (B : SentDenotation Time) : Prop := +def narrowScopeNotUntil (A : Unit → Event Time → Prop) (B : SentDenotation Time) : Prop := Karttunen.notUntil (prfvDen A) B /-- Narrow-scope ¬*until* is exactly ¬*before* (by definition). This is @cite{karttunen-1974}'s identity, now made explicit in the aspectual decomposition. -/ -theorem narrowScope_eq_not_before (A : EventPred Unit Time) (B : SentDenotation Time) : +theorem narrowScope_eq_not_before (A : Unit → Event Time → Prop) (B : SentDenotation Time) : narrowScopeNotUntil A B ↔ ¬ Anscombe.before (prfvDen A) B := Iff.rfl @@ -278,11 +277,11 @@ theorem narrowScope_eq_not_before (A : EventPred Unit Time) (B : SentDenotation - Narrow scope: ¬(A happened before B). FALSE — time 0 < 7, so A precedes B and `Anscombe.before` holds. -/ theorem scope_readings_distinct : - ∃ (A : EventPred Unit ℤ) (B : SentDenotation ℤ), + ∃ (A : Unit → Event ℤ → Prop) (B : SentDenotation ℤ), wideScopeNotUntil A B ∧ ¬ narrowScopeNotUntil A B := by -- sort defaults to .action; the proof doesn't reference .sort - let e₀ : Event ℤ := ⟨⟨0, 5, by omega⟩, .action⟩ - let A : EventPred Unit ℤ := fun _ e => e = e₀ + let e₀ : Event ℤ := ⟨⟨0, 5, by omega⟩, .dynamic⟩ + let A : Unit → Event ℤ → Prop := fun _ e => e = e₀ let iB : Interval ℤ := ⟨7, 7, by omega⟩ let B : SentDenotation ℤ := {iB} refine ⟨A, B, ?_, ?_⟩ @@ -305,11 +304,11 @@ theorem scope_readings_distinct : but wide-scope fails. This confirms the two readings are genuinely independent. -/ theorem scope_readings_independent : - ∃ (A : EventPred Unit ℤ) (B : SentDenotation ℤ), + ∃ (A : Unit → Event ℤ → Prop) (B : SentDenotation ℤ), ¬ wideScopeNotUntil A B ∧ narrowScopeNotUntil A B := by -- sort defaults to .action; the proof doesn't reference .sort - let e₀ : Event ℤ := ⟨⟨5, 10, by omega⟩, .action⟩ - let A : EventPred Unit ℤ := fun _ e => e = e₀ + let e₀ : Event ℤ := ⟨⟨5, 10, by omega⟩, .dynamic⟩ + let A : Unit → Event ℤ → Prop := fun _ e => e = e₀ let iB : Interval ℤ := ⟨3, 7, by omega⟩ let B : SentDenotation ℤ := {iB} refine ⟨A, B, ?_, ?_⟩ @@ -407,9 +406,9 @@ theorem notUntil_not_implies_eventiveUntil : (imperfective *mexri* + continuation asserting no event) and ex. (57) (perfective *para monon* + contradictory continuation). -/ theorem wideScopeNotUntil_compatible_with_empty_main : - ∃ (A : EventPred Unit ℤ) (B : SentDenotation ℤ), + ∃ (A : Unit → Event ℤ → Prop) (B : SentDenotation ℤ), wideScopeNotUntil A B ∧ ¬ ∃ t, t ∈ timeTrace (impfDen A) := by - let A : EventPred Unit ℤ := fun _ _ => False + let A : Unit → Event ℤ → Prop := fun _ _ => False let B : SentDenotation ℤ := { Interval.point 0 } refine ⟨A, B, ?_, ?_⟩ · intro ⟨t, ⟨i, ⟨e, _, habs⟩, _⟩, _⟩; exact habs @@ -536,7 +535,7 @@ theorem veridicality_split : would always be homogeneous. But we proved in §2 that PRFV is NOT always homogeneous (`prfvDen_not_subinterval_closed`). -/ theorem stativizer_false_for_perfective : - ¬ (∀ (P : EventPred Unit ℤ), IsHomogeneous (prfvDen P)) := + ¬ (∀ (P : Unit → Event ℤ → Prop), IsHomogeneous (prfvDen P)) := prfvDen_not_always_homogeneous /-- The five stativizer diagnostics and their results for negated @@ -606,9 +605,9 @@ theorem stativizer_all_wrong : from PRFV (not IMPF), which is why wide-scope is unavailable. -/ theorem english_past_perfective_default : -- PRFV lacks homogeneity → wide scope unavailable - ¬ (∀ (P : EventPred Unit ℤ), IsHomogeneous (prfvDen P)) ∧ + ¬ (∀ (P : Unit → Event ℤ → Prop), IsHomogeneous (prfvDen P)) ∧ -- IMPF has homogeneity → wide scope would be available if past were imperfective - (∀ (P : EventPred Unit ℤ), IsHomogeneous (impfDen P)) := + (∀ (P : Unit → Event ℤ → Prop), IsHomogeneous (impfDen P)) := ⟨prfvDen_not_always_homogeneous, impfDen_homogeneous⟩ -- ============================================================================ diff --git a/Linglib/Studies/IatridouZeijlstra2021.lean b/Linglib/Studies/IatridouZeijlstra2021.lean index b5a24af9e..135be59d1 100644 --- a/Linglib/Studies/IatridouZeijlstra2021.lean +++ b/Linglib/Studies/IatridouZeijlstra2021.lean @@ -50,7 +50,6 @@ framework but has not been line-by-line cross-checked against IZ namespace IatridouZeijlstra2021 open Core.Time -open Semantics.Events open Semantics.Aspect open Semantics.Aspect.SubintervalProperty open Semantics.Tense.TemporalAdverbials (PTSConstraint AdverbialType) @@ -264,17 +263,17 @@ theorem subdomain_monotone (τ₁ τ₂ : Interval Time) /-- An event of type P has its runtime inside time span τ. This is the assertion form for both PTS and UTS: ∃e.[P(e) ∧ Run(e) ⊆ τ] -/ -def eventInSpan (P : EventPred W Time) (w : W) (τ : Interval Time) : Prop := +def eventInSpan (P : W → Event Time → Prop) (w : W) (τ : Interval Time) : Prop := ∃ e : Event Time, e.τ.subinterval τ ∧ P w e /-- Negated form: no P-event has runtime inside τ. ¬∃e.[P(e) ∧ Run(e) ⊆ τ] -/ -def noEventInSpan (P : EventPred W Time) (w : W) (τ : Interval Time) : Prop := +def noEventInSpan (P : W → Event Time → Prop) (w : W) (τ : Interval Time) : Prop := ¬ eventInSpan P w τ /-- If a culminated event occurs in a subinterval, it occurs in the superinterval. Entailment from subinterval to superinterval. -/ -theorem eventInSpan_monotone (P : EventPred W Time) (w : W) +theorem eventInSpan_monotone (P : W → Event Time → Prop) (w : W) (τ₁ τ₂ : Interval Time) (h : τ₁.subinterval τ₂) : eventInSpan P w τ₁ → eventInSpan P w τ₂ := by intro ⟨e, hsub, hP⟩ @@ -283,7 +282,7 @@ theorem eventInSpan_monotone (P : EventPred W Time) (w : W) /-- Subdomain alternatives for culminated events are all nonweaker: every subdomain alternative entails the assertion. This is because eventInSpan is monotone in the time span. -/ -theorem subdomain_alts_nonweaker (P : EventPred W Time) (w : W) +theorem subdomain_alts_nonweaker (P : W → Event Time → Prop) (w : W) (τ : Interval Time) (τ' : Interval Time) (h : τ' ∈ SubdomainAlternatives τ) : eventInSpan P w τ' → eventInSpan P w τ := eventInSpan_monotone P w τ' τ h @@ -301,7 +300,7 @@ theorem subdomain_alts_nonweaker (P : EventPred W Time) (w : W) This explains why *in years* is an NPI: "*Joe has met Mary in weeks" is ungrammatical because exhaustification of the domain alternatives in a positive context yields contradiction. -/ -theorem positive_exhaustification_contradicts (P : EventPred W Time) (w : W) +theorem positive_exhaustification_contradicts (P : W → Event Time → Prop) (w : W) (τ : Interval Time) (_hassert : eventInSpan P w τ) -- The exhaustifier requires negating all stronger alternatives @@ -319,7 +318,7 @@ theorem positive_exhaustification_contradicts (P : EventPred W Time) (w : W) WEAKER than the assertion ¬∃e.[P(e) ∧ Run(e) ⊆ τ] (for τ' ⊆ τ). Since no subdomain alternative is stronger, there is nothing to exclude, and exhaustification applies vacuously. No contradiction arises. -/ -theorem negated_subdomain_weaker (P : EventPred W Time) (w : W) +theorem negated_subdomain_weaker (P : W → Event Time → Prop) (w : W) (τ τ' : Interval Time) (h : τ'.subinterval τ) : noEventInSpan P w τ → noEventInSpan P w τ' := by intro hneg hev @@ -340,12 +339,12 @@ theorem negated_subdomain_weaker (P : EventPred W Time) (w : W) that stretches as far as possible, the LB must be at the most recent occurrence of the event. This makes the event's occurrence a presupposition, not just an implicature — hence noncancelable. -/ -def actualityInference (P : EventPred W Time) (w : W) +def actualityInference (P : W → Event Time → Prop) (w : W) (τ : Interval Time) : Prop := eventInSpan P w τ /-- The AI with *in years* is at the LB: the event occurs at the LB point. -/ -def aiAtBoundary (P : EventPred W Time) (w : W) +def aiAtBoundary (P : W → Event Time → Prop) (w : W) (τ : Interval Time) : Prop := ∃ e : Event Time, e.τ.finish = τ.start ∧ P w e @@ -392,7 +391,7 @@ def imperfectiveContainment (e : Event Time) (τ : Interval Time) : Prop := is vacuous for affirmative imperfectives — explaining why *until*-d (affirmative imperfective + *until*) is fine without negation. @cite{iatridou-zeijlstra-2021} §7.2 -/ -theorem impf_subdomain_entailed (P : EventPred W Time) +theorem impf_subdomain_entailed (P : W → Event Time → Prop) (hSub : HasSubintervalProp P) (w : W) (e : Event Time) (τ : Interval Time) (hP : P w e) (hImpf : τ.subinterval e.τ) @@ -403,7 +402,7 @@ theorem impf_subdomain_entailed (P : EventPred W Time) ⟨le_trans hImpf.1 hτ'.1, le_trans hτ'.2 hImpf.2⟩ -- By SUB, any event with runtime τ' is a P-event -- sort defaults to .action; the proof doesn't reference .sort - exact ⟨⟨τ', .action⟩, ⟨le_refl _, le_refl _⟩, hSub e w hP τ' h_sub_e ⟨τ', .action⟩ rfl⟩ + exact ⟨⟨τ', .dynamic⟩, ⟨le_refl _, le_refl _⟩, hSub e w hP τ' h_sub_e ⟨τ', .dynamic⟩ rfl⟩ -- ════════════════════════════════════════════════════ -- § 11. Bridge: Constant's Observation diff --git a/Linglib/Studies/KennedyLevin2008.lean b/Linglib/Studies/KennedyLevin2008.lean index 427851dbb..c3bc2b337 100644 --- a/Linglib/Studies/KennedyLevin2008.lean +++ b/Linglib/Studies/KennedyLevin2008.lean @@ -328,7 +328,6 @@ theorem warm_pipeline_converge : self-contained. The fragment-level §1-4 results above are independent of this substrate work. -/ -open Semantics.Events open Semantics.ArgumentStructure.Affectedness open Semantics.ArgumentStructure.Affectedness.Hierarchy open Semantics.Degree.MeasureFunction diff --git a/Linglib/Studies/Kiparsky2002.lean b/Linglib/Studies/Kiparsky2002.lean index e0bfaaa51..607ed04b2 100644 --- a/Linglib/Studies/Kiparsky2002.lean +++ b/Linglib/Studies/Kiparsky2002.lean @@ -65,7 +65,6 @@ open Core.Time.Reichenbach open Features open Semantics.Aspect open Semantics.Aspect.SubeventStructure -open Semantics.Events -- ════════════════════════════════════════════════════ -- § 1. Perfect Readings (@cite{kiparsky-2002}) @@ -262,7 +261,7 @@ theorem existential_eq_perf_prfv {Time : Type*} [LinearOrder Time] constructor · rintro ⟨pts, hR, hSub⟩ -- sort defaults to .action; the proof doesn't reference .sort - exact ⟨pts, hR, ⟨d.runtime, .action⟩, hSub, rfl⟩ + exact ⟨pts, hR, ⟨d.runtime, .dynamic⟩, hSub, rfl⟩ · rintro ⟨pts, hR, e, hSub, heq⟩ exact ⟨pts, hR, heq ▸ hSub⟩ @@ -278,7 +277,7 @@ theorem universal_eq_perf_unbounded {Time : Type*} [LinearOrder Time] constructor · rintro ⟨pts, hR, hSub⟩ -- sort defaults to .action; the proof doesn't reference .sort - exact ⟨pts, hR, ⟨d.runtime, .action⟩, hSub, rfl⟩ + exact ⟨pts, hR, ⟨d.runtime, .dynamic⟩, hSub, rfl⟩ · rintro ⟨pts, hR, e, hSub, heq⟩ exact ⟨pts, hR, heq ▸ hSub⟩ diff --git a/Linglib/Studies/Koev2017.lean b/Linglib/Studies/Koev2017.lean index feccc48b9..6f5aa8df5 100644 --- a/Linglib/Studies/Koev2017.lean +++ b/Linglib/Studies/Koev2017.lean @@ -167,7 +167,6 @@ while the assertion commits the speaker to p via DECL (72). open Core.Time open Semantics.Presupposition -open Semantics.Events open Semantics.Tense.Evidential open Fragments.Slavic.Bulgarian.Evidentials @@ -346,17 +345,17 @@ def LearningScenario.toEvidentialProp (s : LearningScenario ℤ) /-! ### Concrete Scenarios -/ /-- Described event: interval [0, 5]. -/ -def describedEvent : Event ℤ := ⟨⟨0, 5, by omega⟩, .action⟩ +def describedEvent : Event ℤ := ⟨⟨0, 5, by omega⟩, .dynamic⟩ /-- Learning event (indirect): interval [10, 15] — strictly later. -/ -def learningEventIndirect : Event ℤ := ⟨⟨10, 15, by omega⟩, .state⟩ +def learningEventIndirect : Event ℤ := ⟨⟨10, 15, by omega⟩, .stative⟩ /-- Learning event (direct witness): interval [2, 4] — overlaps described. -/ -def learningEventDirect : Event ℤ := ⟨⟨2, 4, by omega⟩, .state⟩ +def learningEventDirect : Event ℤ := ⟨⟨2, 4, by omega⟩, .stative⟩ /-- Learning event (spatial distance): interval [0, 5] — same time, different place (smoke from chimney). -/ -def learningEventSpatial : Event ℤ := ⟨⟨0, 5, by omega⟩, .state⟩ +def learningEventSpatial : Event ℤ := ⟨⟨0, 5, by omega⟩, .stative⟩ /-- Indirect evidence scenario: described event [0,5], learning event [10,15]. -/ def indirectScenario : LearningScenario ℤ where diff --git a/Linglib/Studies/Krifka1998.lean b/Linglib/Studies/Krifka1998.lean index b1e3b6ffb..a76c7a4e8 100644 --- a/Linglib/Studies/Krifka1998.lean +++ b/Linglib/Studies/Krifka1998.lean @@ -912,7 +912,6 @@ end K98PropositionalSubstrate section SpatialTracePullback -open Semantics.Events open Semantics.Events.CEM open Semantics.Spatial.Path @@ -941,7 +940,6 @@ end SpatialTracePullback section Expansiveness -open Semantics.Events open Semantics.Events.CEM variable {α : Type*} [SemilatticeSup α] @@ -962,7 +960,6 @@ end Expansiveness section MovementInstances -open Semantics.Events open Semantics.Events.CEM open Semantics.Spatial.Path diff --git a/Linglib/Studies/OgiharaST2024.lean b/Linglib/Studies/OgiharaST2024.lean index 9185bb75a..7e0c78ab7 100644 --- a/Linglib/Studies/OgiharaST2024.lean +++ b/Linglib/Studies/OgiharaST2024.lean @@ -398,7 +398,6 @@ theorem logical_property_asymmetry : -- ════════════════════════════════════════════════════════════════ open Semantics.Tense.TemporalConnectives -open Semantics.Events open Fragments.English.TemporalExpressions -- ════════════════════════════════════════════════════════════════ @@ -429,7 +428,7 @@ theorem fragment_veridicality_asymmetry : This is not a stipulation in the Fragment — it follows from the semantics. -/ theorem after_veridicality_derived : - ∀ (P Q : EvPred ℤ), AnscombeEvent.after P Q → ∃ e : Event ℤ, Q e := + ∀ (P Q : Event ℤ → Prop), AnscombeEvent.after P Q → ∃ e : Event ℤ, Q e := fun P Q h => AnscombeEvent.after_veridical P Q h /-- O&ST's theory derives *before*'s non-veridicality from the universal @@ -438,7 +437,7 @@ theorem after_veridicality_derived : Concretely: any P-event with an empty Q yields `before(P, Q)`. -/ theorem before_nonveridicality_derived : - ∃ (P Q : EvPred ℤ), AnscombeEvent.before P Q ∧ ¬∃ e : Event ℤ, Q e := + ∃ (P Q : Event ℤ → Prop), AnscombeEvent.before P Q ∧ ¬∃ e : Event ℤ, Q e := AnscombeEvent.before_nonveridical -- ════════════════════════════════════════════════════════════════ @@ -450,10 +449,10 @@ theorem before_nonveridicality_derived : - arriving event at time 0 O&ST predicts: after(leave, arrive) holds (τ(arrive) ≺ τ(leave)). -/ theorem scenario_after_punctual : - let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .action⟩ - let arrive : Event ℤ := ⟨⟨0, 0, le_refl _⟩, .action⟩ + let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .dynamic⟩ + let arrive : Event ℤ := ⟨⟨0, 0, le_refl _⟩, .dynamic⟩ AnscombeEvent.after (· = leave) (· = arrive) := by - refine ⟨⟨⟨1, 1, le_refl _⟩, .action⟩, ⟨⟨0, 0, le_refl _⟩, .action⟩, rfl, rfl, ?_⟩ + refine ⟨⟨⟨1, 1, le_refl _⟩, .dynamic⟩, ⟨⟨0, 0, le_refl _⟩, .dynamic⟩, rfl, rfl, ?_⟩ simp [Core.Time.Interval.precedes, Event.τ] /-- Scenario: "He left₁ before she arrived₃" with punctual events. @@ -461,19 +460,19 @@ theorem scenario_after_punctual : - arriving event at time 3 O&ST predicts: before(leave, arrive) holds (τ(leave) ≺ τ(arrive)). -/ theorem scenario_before_punctual : - let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .action⟩ - let arrive : Event ℤ := ⟨⟨3, 3, le_refl _⟩, .action⟩ + let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .dynamic⟩ + let arrive : Event ℤ := ⟨⟨3, 3, le_refl _⟩, .dynamic⟩ AnscombeEvent.before (· = leave) (· = arrive) := by - refine ⟨⟨⟨1, 1, le_refl _⟩, .action⟩, rfl, ?_⟩ + refine ⟨⟨⟨1, 1, le_refl _⟩, .dynamic⟩, rfl, ?_⟩ intro e₂ rfl simp [Core.Time.Interval.precedes, Event.τ] /-- Scenario: "The bomb exploded₅ before anyone defused it" (nobody defused it). O&ST predicts: before(explode, defuse) holds vacuously (no defuse-events). -/ theorem scenario_before_counterfactual : - let explode : Event ℤ := ⟨⟨5, 5, le_refl _⟩, .action⟩ + let explode : Event ℤ := ⟨⟨5, 5, le_refl _⟩, .dynamic⟩ AnscombeEvent.before (· = explode) (fun _ => False) := by - exact ⟨⟨⟨5, 5, le_refl _⟩, .action⟩, rfl, fun _ h => h.elim⟩ + exact ⟨⟨⟨5, 5, le_refl _⟩, .dynamic⟩, rfl, fun _ h => h.elim⟩ -- ════════════════════════════════════════════════════════════════ -- § 13: Cross-Level Projection Verification @@ -482,15 +481,15 @@ theorem scenario_before_counterfactual : /-- The punctual after-scenario projects correctly through eventDenotation: O&ST.after implies Anscombe.after on the projected interval sets. -/ theorem scenario_after_projects : - let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .action⟩ - let arrive : Event ℤ := ⟨⟨0, 0, le_refl _⟩, .action⟩ + let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .dynamic⟩ + let arrive : Event ℤ := ⟨⟨0, 0, le_refl _⟩, .dynamic⟩ Anscombe.after (eventDenotation (· = leave)) (eventDenotation (· = arrive)) := AnscombeEvent.after_implies_anscombe _ _ scenario_after_punctual /-- The punctual before-scenario projects correctly through eventDenotation. -/ theorem scenario_before_projects : - let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .action⟩ - let arrive : Event ℤ := ⟨⟨3, 3, le_refl _⟩, .action⟩ + let leave : Event ℤ := ⟨⟨1, 1, le_refl _⟩, .dynamic⟩ + let arrive : Event ℤ := ⟨⟨3, 3, le_refl _⟩, .dynamic⟩ Anscombe.before (eventDenotation (· = leave)) (eventDenotation (· = arrive)) := AnscombeEvent.before_implies_anscombe _ _ scenario_before_punctual @@ -701,7 +700,7 @@ The following theorems make this structural parallel precise. -/ `impf_entails_prfv_of_csip` from SubintervalProperty.lean. -/ theorem csip_entails_completion {W Time : Type*} [LinearOrder Time] - (P : EventPred W Time) (hCSIP : HasClosedSubintervalProp P) + (P : W → Event Time → Prop) (hCSIP : HasClosedSubintervalProp P) (w : W) (t : Core.Time.Interval Time) : IMPF P w t → PRFV P w t := fun h => impf_entails_prfv_of_csip P hCSIP w t h @@ -716,7 +715,7 @@ theorem csip_entails_completion `imperfective_paradox_possible` from SubintervalProperty.lean. -/ theorem non_csip_lacks_completion {W : Type*} (w : W) (t₁ t₂ : ℤ) (hlt : t₁ < t₂) : - ¬ (∀ (P : EventPred W ℤ), HasSubintervalProp P) := + ¬ (∀ (P : W → Event ℤ → Prop), HasSubintervalProp P) := imperfective_paradox_possible w t₁ t₂ hlt /-- **Progressive–before modal resolution**: When P lacks CSIP (accomplishment), @@ -731,7 +730,7 @@ theorem non_csip_lacks_completion event whose continuation satisfies Q in accessible worlds. -/ theorem progressive_before_modal_resolution {W Time : Type*} [LinearOrder Time] - (P Q : EventPred W Time) + (P Q : W → Event Time → Prop) (alternatives : Event Time → Set W) (w : W) (t : Core.Time.Interval Time) (hIMPF : IMPF P w t) @@ -754,7 +753,7 @@ theorem progressive_before_modal_resolution resolution (the progressive / anti-veridical *before*). -/ theorem csip_determines_modal_need {W Time : Type*} [LinearOrder Time] - (P : EventPred W Time) (w : W) (t : Core.Time.Interval Time) : + (P : W → Event Time → Prop) (w : W) (t : Core.Time.Interval Time) : (HasClosedSubintervalProp P → IMPF P w t → PRFV P w t) ∧ (IMPF P w t → ¬HasClosedSubintervalProp P → ¬(∀ (t' : Core.Time.Interval Time), t'.subinterval t → diff --git a/Linglib/Studies/Pasternak2019.lean b/Linglib/Studies/Pasternak2019.lean index 553c3f265..0aca7ed9c 100644 --- a/Linglib/Studies/Pasternak2019.lean +++ b/Linglib/Studies/Pasternak2019.lean @@ -67,7 +67,7 @@ The first-pass version of this file claimed several substrate gaps that do not exist. Corrected: - §4.2 two-dimensional ontology: a vertical-altitude axis would *extend* - `Semantics.Events.Basic.EventMereology` (which already provides the + `Event.Mereology` (which already provides the `Preorder (Event Time)` instance Pasternak's part-whole relation consumes). Not a substrate gap; a refinement. - §5 `want`/`wish`/`regret`: `Semantics/Attitudes/Desire.lean` @@ -86,7 +86,6 @@ namespace Pasternak2019 open Semantics.Gradability.StatesBased open Semantics.Attitudes.Confidence -open Semantics.Events (Event EvPred) open Semantics.ArgumentStructure (ThematicFrame) /-! ## §1. Monotonicity (Pasternak (4)) @@ -152,7 +151,7 @@ not the verb). experiencer roles come from a `ThematicFrame` at use sites. -/ structure MentalStateVerb (Time : Type*) [LinearOrder Time] where /-- The verb's lexical predicate on eventualities (e.g., `hate`, `love`) -/ - predicate : EvPred Time + predicate : Event Time → Prop /-- Intensity measure function — Pasternak's `μ_int` -/ μint : Event Time → ℚ @@ -184,7 +183,7 @@ Pasternak's intensity case is one specialization. -/ Wellwood's `comparativeTruthHetero` for Pasternak's intensity case. -/ @[simp] def themedPredicate {Entity Time : Type*} [LinearOrder Time] (v : MentalStateVerb Time) (frame : ThematicFrame Entity Time) - (x : Entity) : EvPred Time := + (x : Entity) : Event Time → Prop := fun e => v.predicate e ∧ frame.theme x e /-- The intensity comparative `α V x more than β V y` (Pasternak (53)): @@ -340,10 +339,10 @@ theorem intensityComparative_max {Entity Time : Type*} [LinearOrder Time] `MentalStateHomogeneity` is `Mereology.DIV` over the ambient `[Preorder Event]`. When `Event = Event Time` and the preorder comes from -`Semantics/Events/Basic.lean::EventMereology`, Pasternak's claim +`Semantics/Events/Basic.lean::Event.Mereology`, Pasternak's claim becomes: vP-predicates respect the event-mereology part-of. We expose two substrate consequences below: a downward-closure inheritance lemma -for sort-determined predicates (using `EventMereology.sort_preserved`), +for sort-determined predicates (using `Event.Mereology.sort_preserved`), and a g-homogeneity bridge to `Core/Mereology.lean::gHomogeneous` (triggered when the carrier is a `PartialOrder`). @@ -357,21 +356,20 @@ adjectives like `confident that p`). The substrate-level identification (monotonicity = admissibleMeasure) is now in the `admissibleMeasure` docstring, not as a redundant per-file Iff.rfl. -/ -open Semantics.Events in /-- Sort-determined predicates inherit homogeneity from - `EventMereology.sort_preserved`: any predicate of the form + `Event.Mereology.sort_preserved`: any predicate of the form "eventuality has sort `s`" is downward-closed under part-of, so `MentalStateHomogeneity` follows for free. Pasternak's mental-state predicates are stative (Levin class 31.2; Vendler `state`); to the extent they implicate sort, they inherit homogeneity from this theorem. -/ theorem sortDetermined_isHomogeneous - {Time : Type*} [LinearOrder Time] [EventMereology Time] - (s : EventSort) : - letI := eventPreorder Time + {Time : Type*} [LinearOrder Time] [Event.Mereology Time] + (s : Features.Dynamicity) : + letI := Event.preorder Time MentalStateHomogeneity (fun e : Event Time => e.sort = s) := by intro e e' hPe hle - exact (EventMereology.sort_preserved e' e hle).trans hPe + exact (Event.Mereology.sort_preserved e' e hle).trans hPe /-- On a `PartialOrder` carrier, Pasternak's `MentalStateHomogeneity` implies `Mereology.gHomogeneous` (every proper part has a P-part — @@ -430,7 +428,7 @@ entries with measure-function payloads. ### §4.2 Two-dimensional state ontology + DOG (eq. 87) Pasternak's vertical altitude axis `K` (PDF p.288) extends rather than -replaces the substrate's `EventMereology Time` preorder. A +replaces the substrate's `Event.Mereology Time` preorder. A `Semantics/Events/VerticalDimension.lean` add-on with `κ : Event Time → Set Altitude` plus the DOG fineness lattice (which can consume `Core.Order.FeaturePreorder.coarsen_via_monotone`) is a clean diff --git a/Linglib/Studies/Pylkkanen2008.lean b/Linglib/Studies/Pylkkanen2008.lean index 545755c07..b6da09d71 100644 --- a/Linglib/Studies/Pylkkanen2008.lean +++ b/Linglib/Studies/Pylkkanen2008.lean @@ -4,6 +4,7 @@ import Linglib.Syntax.Minimalist.ApplicativeDiagnostics import Linglib.Syntax.Minimalist.Voice import Linglib.Syntax.Minimalist.VoiceProjection import Linglib.Semantics.ArgumentStructure.EntailmentProfile +import Linglib.Semantics.ArgumentStructure.ArgumentIntroduction import Linglib.Data.WALS.Features.F109A import Linglib.Studies.Larson1988 @@ -273,9 +274,11 @@ def venda_appl : LangApplProfile := , classification := .high } /-- Albanian: high. I vrapova (25a); Agimi i mban Drites çanten time - (25b). Albanian "depictives" can also modify implicit external - arguments and DPs inside PPs, so they don't qualify as English-style - depictives — Test 3 is *inapplicable* (§2.1.3.2.5). -/ + (25b). Albanian postverbal APs pattern like English ones (modifying + internal and external but not implicit external arguments), except + that — unlike English depictives — they can also easily modify DPs + inside PPs. That extra breadth disqualifies them as English-style + depictives, so Test 3 is *inapplicable* (§2.1.3.2.5). -/ def albanian_appl : LangApplProfile := { language := "Albanian" , diagnostics := @@ -404,16 +407,30 @@ in §13. -/ Pylkkänen's other major Ch. 3 argument: the causative head Cause introduces a *causing event*, not a θ-role on the external argument. -Evidence: Japanese adversity causatives (eq. 19–25) have causative +Evidence: Japanese adversity causatives (§3.2.2) have causative morphology and meaning but no external argument. The bieventive analysis (Cause = relation between two events) is required by such data; the θ-role analysis (Cause = relation between a causer and a caused event) cannot accommodate them. -Formalizing the bieventive vs. θ-role contrast at the level of -detail Pylkkänen offers requires event semantics infrastructure -beyond this study file's scope; the substantive claim is recorded -here for cross-reference. -/ +The bieventive vs. θ-role contrast is formalized in +`Semantics/ArgumentStructure/ArgumentIntroduction.lean`: +`causeBieventive_no_external_arg` shows a causing event with no causer +participant (the Japanese adversity causative), while +`causeThetaRole_forces_causer` shows the θ-role denotation entails a causer +— so only the bieventive analysis accommodates the data, derived from the +denotations. -/ + +open Semantics.ArgumentStructure in +/-- @cite{pylkkanen-2008} §3.2: the Japanese adversity causative — a causing + event with no external argument — is admitted by the bieventive Cause + denotation, which the θ-role analysis (forcing a causer) cannot model. -/ +theorem cause_bieventive_admits_adversity_causative + {Time : Type*} [LinearOrder Time] + (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) + (e e' : Event Time) (hc : caused e') (hcause : cause e e') : + causeBieventive cause caused e := + causeBieventive_no_external_arg cause caused e e' hc hcause /-! ## §10. Hebrew possessor datives as low source applicatives (@cite{pylkkanen-2008} Ch. 2 §2.2, Table 2.2 p. 60) @@ -520,8 +537,11 @@ Japanese adversity passives split into *gapped* (low source applicative) and *gapless* (high applicative). The gapped/gapless distinction itself is Kubo's 1992 work (cited by @cite{pylkkanen-2008}; not yet in linglib bib)'s; @cite{pylkkanen-2008}'s contribution is the reanalysis as a low-source vs. high applicative typology. Both share -the *-rare-* morphology, but only the gapless type carries an obligatory -adversative entailment (Kubo's 1992 work (cited by @cite{pylkkanen-2008}; not yet in linglib bib)). The diagnostic bundle +the *-rare-* passive morphology; the distinguishing criterion is the +possessive/transfer relation to the direct object — the gapped (low +source) type requires it, the gapless (high malefactive) type bears a +malefactive relation to the event and no necessary relation to the +object. The diagnostic bundle distinguishing the two types is not formalized here; this section records the type-level split for cross-reference. -/ @@ -582,9 +602,11 @@ def CuervoLowAppl.isDynamic : CuervoLowAppl → Bool theorem static_not_dynamic : CuervoLowAppl.staticPossession.isDynamic = false := rfl -/-! ## §13. Causative typology (Pylkkänen Table 3.1, §3.4) +/-! ## §13. Causative typology (Pylkkänen Table 3.1, Ch. 3 intro p. 87) -Pylkkänen Table 3.1 (§3.4) is a 2 × 3 typology of causative constructions +Pylkkänen Table 3.1 (Chapter 3 introduction, p. 87 — *not* §3.4, which +argues the three-way *selection* split and carries the separate Table 3.2) +is a 2 × 3 typology of causative constructions parameterized by Voice-bundling × selection. The inventory (`VoiceBundlingChoice`, `CauseSelection`, `MorphologyAccess`, `CausativeCell` + 6 canonical instances + 4 prediction theorems) lives @@ -655,12 +677,14 @@ def CausativeCell.permitsUnaccusativeCausative (c : CausativeCell) : PredictsVer | some .independent => .predicts /-- Table 3.1 prediction (2): can the language causativize unergatives - and transitives? Only phase-selecting Cause can. -/ + and transitives? Verb- and phase-selecting Cause can; only + root-selecting Cause cannot. (Table 3.1's prediction (2) is identical + across both Voice-bundling columns, so it turns on selection alone.) -/ def CausativeCell.permitsUnergativeAndTransitiveCausativization (c : CausativeCell) : Bool := match c.selection with - | .phase => true - | .root | .verb => false + | .verb | .phase => true + | .root => false /-- Table 3.1 prediction (3): what morphology can intervene between root and Cause? -/ @@ -720,7 +744,7 @@ theorem japanese_lexical_predictions : theorem finnish_tta_predictions : finnishTtaCausative.permitsUnaccusativeCausative = .predicts ∧ - finnishTtaCausative.permitsUnergativeAndTransitiveCausativization = false ∧ + finnishTtaCausative.permitsUnergativeAndTransitiveCausativization = true ∧ finnishTtaCausative.morphologyAccess = .categoryDefiningOnly := ⟨rfl, rfl, rfl⟩ @@ -759,10 +783,11 @@ theorem pylkkanen_view_partitions_voice_flavors : refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide /-! ## §15. Transitivity restriction grounded in EntailmentProfile - (@cite{pylkkanen-2008} Diagnostic 1; semantic argument at eq. 103 / - p. 55; -- UNVERIFIED: eq. 17 number) + (@cite{pylkkanen-2008} Diagnostic 1 = eq. 17, p. 18; semantic + argument at eq. 103, p. 55) -Pylkkänen's *predicted* generalization (book Ch. 2 §2.1.1, Diagnostic 1): +Pylkkänen's *predicted* generalization (book Ch. 2 §2.1.1, Diagnostic 1, +eq. 17, p. 18): "Only high applicative heads should be able to combine with unergatives. Since low applicative heads denote a relation between the direct object and the indirect object, a low applicative head @@ -772,18 +797,17 @@ The semantic argument (eq. 103, p. 55): combining low Appl (`λx.λy.λf.λe. f(e,x) ∧ theme(e,x) ∧ HAVE(x,y)`) with an unergative VP (`λe. agent(e, Mary) ∧ run(e)`) yields `agent(e, x) ∧ theme(e, x)` when both arguments bind the same variable — a thematic-uniqueness -contradiction (Carlson, Parsons). +contradiction. **Status of this formalization**: The composition predicate below uses -`Core.Verbs.EntailmentProfile.pPatientScore` to check whether a verb +`Semantics.ArgumentStructure.EntailmentProfile.pPatientScore` to check whether a verb has theme-like Proto-Patient entailments. An unergative has either no object profile (`objectEntailments = none`) or an empty one -(`pPatientScore = 0`). The composition theorem is structural — it -does *not* re-derive the type clash from event-semantic λ-calculus -(that requires the compositional type-driven semantics in -`Semantics/Composition/`, not yet wired in here). The -substantive content captured: "low Appl needs a theme; unergative -provides none; composition fails." -/ +(`pPatientScore = 0`). This `EntailmentProfile`-based predicate is the +structural surface; the event-semantic *derivation* of the eq. 103 type +clash is now wired in via `Semantics/ArgumentStructure/ArgumentIntroduction.lean` +and consumed in §15c below (`low_appl_blocks_unergative_denotational`, +`low_external_arg_clash`). -/ open Semantics.ArgumentStructure.EntailmentProfile (EntailmentProfile) @@ -869,6 +893,51 @@ theorem low_source_combines_with_transitive : right exact themeBearingProfile_has_unsaturated_theme +/-! ## §15c. Event-semantic grounding: the transitivity restriction derived + +The `applicativeComposition` predicate above captures the empirical content +structurally (via `ApplType.RequiresThemeInComplement`). The denotational +*derivation* of @cite{pylkkanen-2008}'s eq. 103 — the type clash that forces +the transitivity restriction — lives in +`Semantics/ArgumentStructure/ArgumentIntroduction.lean`. There the high/low +contrast is `IntroMode.toEvent`/`.toTheme`, the two diagnostics are +`toTheme_blocks_unergative` (Diagnostic 1, no internal argument) and +`toTheme_blocks_kimian` (Diagnostic 2, no event argument — Kimian states, +@cite{moltmann-2025}), and the thematic-uniqueness contradiction is +`low_external_arg_clash`. We record the correspondence: Pylkkänen's `ApplType` +projects to an `IntroMode`, and the empirical diagnostics are *instances* of +the substrate theorems rather than restatements of the `IsLow` predicate. -/ + +open Semantics.ArgumentStructure + +/-- Pylkkänen's high/low `ApplType` as a denotational introduction mode + (@cite{wood-marantz-2017}'s contextually-interpreted introducer). -/ +def applIntroMode : ApplType → IntroMode + | .high => .toEvent + | .lowRecipient => .toTheme + | .lowSource => .toTheme + +/-- The transitivity restriction, derived from the denotations: a low + applicative (recipient or source) cannot license an unergative verb, + because the low denotation has no event-internal theme to relate to. + This is `low_applicative_blocks_unergative` re-grounded in the + `ArgumentIntroduction` substrate rather than the `IsLow` alias. -/ +theorem low_appl_blocks_unergative_denotational + {Entity Time : Type*} [LinearOrder Time] (a : ApplType) (hLow : a.IsLow) + (body : Event Time → Prop) : + ¬ (applIntroMode a).Licenses (VerbDenot.unergative (Entity := Entity) body) := by + have h : applIntroMode a = .toTheme := by + rcases hLow with h | h <;> subst h <;> rfl + rw [h]; exact toTheme_blocks_unergative body + +/-- High applicatives license unergatives, derived denotationally + (Luganda/Venda/Albanian, PDF eq. 23a/24a/25a). -/ +theorem high_appl_licenses_unergative_denotational + {Entity Time : Type*} [LinearOrder Time] + (body : Event Time → Prop) : + (applIntroMode .high).Licenses (VerbDenot.unergative (Entity := Entity) body) := + toEvent_licenses_all _ + /-! ## §16. Voice × Appl licensing matrix (`Syntax/Minimalism/Applicative.lean.licensedWith`) diff --git a/Linglib/Studies/Rouillard2026.lean b/Linglib/Studies/Rouillard2026.lean index 29a4f7916..c55c482fb 100644 --- a/Linglib/Studies/Rouillard2026.lean +++ b/Linglib/Studies/Rouillard2026.lean @@ -87,7 +87,6 @@ namespace Rouillard2026 open Core.Time open Core.Time.Interval -open Semantics.Events open Semantics.Aspect open Semantics.Aspect.SubintervalProperty open Features @@ -154,7 +153,7 @@ def inETIA (e : Event Time) (bound : Interval Time) : Prop := /-- E-TIA derived property: at world `w`, value `n` is true iff there is a P-event whose runtime is included in some `n`-unit time, and that `n`-unit time falls within `g1`. @cite{rouillard-2026} eq. (77). -/ -def eTIAProperty (P : EventPred W Time) (μ : Interval Time → ℕ) +def eTIAProperty (P : W → Event Time → Prop) (μ : Interval Time → ℕ) [TimeMeasure Time μ] (g1 : Interval Time) : ℕ → W → Prop := fun n w => ∃ t : Interval Time, μ t = n ∧ ∃ e : Event Time, P w e ∧ e.τ.subinterval g1 ∧ e.τ.subinterval t @@ -172,7 +171,7 @@ def eTIAProperty (P : EventPred W Time) (μ : Interval Time → ℕ) explicitly noted "the openness constraint is enforced at the level of the G-TIA semantics rather than structurally" — i.e., not at all). @cite{rouillard-2026} eq. (94) revised with eq. (101). -/ -def gTIAPropertyOpen (P : EventPred W Time) (μ : Interval Time → ℕ) +def gTIAPropertyOpen (P : W → Event Time → Prop) (μ : Interval Time → ℕ) [TimeMeasure Time μ] (s : Time) : ℕ → W → Prop := fun n w => ∃ ptsGI : GInterval Time, ptsGI.isOpen ∧ @@ -183,7 +182,7 @@ def gTIAPropertyOpen (P : EventPred W Time) (μ : Interval Time → ℕ) /-- The negation of `gTIAPropertyOpen`, used for G-TIAs in negative contexts (where the property "no event in the n-unit open PTS" holds iff `gTIAPropertyOpen` is false). -/ -def gTIAPropertyOpenNeg (P : EventPred W Time) (μ : Interval Time → ℕ) +def gTIAPropertyOpenNeg (P : W → Event Time → Prop) (μ : Interval Time → ℕ) [TimeMeasure Time μ] (s : Time) : ℕ → W → Prop := fun n w => ¬ gTIAPropertyOpen P μ s n w @@ -209,7 +208,7 @@ def gTIAPropertyOpenNeg (P : EventPred W Time) (μ : Interval Time → ℕ) numeral yields a true proposition at any world where any does, so no numeral is more informative than another. @cite{rouillard-2026} §4.1.1. -/ theorem eTIA_atelic_collapse {μ : Interval Time → ℕ} [TimeMeasure Time μ] - (P : EventPred W Time) (g1 : Interval Time) + (P : W → Event Time → Prop) (g1 : Interval Time) (hSub : HasSubintervalProp P) : IsConstant (α := ℕ) (eTIAProperty P μ g1) := by suffices h : ∀ n m w, eTIAProperty P μ g1 n w → eTIAProperty P μ g1 m w from @@ -217,7 +216,7 @@ theorem eTIA_atelic_collapse {μ : Interval Time → ℕ} [TimeMeasure Time μ] intro n m w ⟨_, _, e, hP, hg1, _⟩ rcases le_total m (μ e.τ) with hle | hge · obtain ⟨j, hj_sub, hj_μ⟩ := TimeMeasure.subdivisible e.τ m hle - refine ⟨j, hj_μ, ⟨j, .action⟩, hSub e w hP j hj_sub ⟨j, .action⟩ rfl, + refine ⟨j, hj_μ, ⟨j, .dynamic⟩, hSub e w hP j hj_sub ⟨j, .dynamic⟩ rfl, ⟨?_, ?_⟩, ⟨le_refl _, le_refl _⟩⟩ · exact le_trans hg1.1 hj_sub.1 · exact le_trans hj_sub.2 hg1.2 @@ -226,14 +225,14 @@ theorem eTIA_atelic_collapse {μ : Interval Time → ℕ} [TimeMeasure Time μ] /-- Atelic E-TIA fails the `AdmitsOptimum` half of MIP licensing. -/ theorem eTIA_atelic_no_optimum {μ : Interval Time → ℕ} [TimeMeasure Time μ] - (P : EventPred W Time) (g1 : Interval Time) + (P : W → Event Time → Prop) (g1 : Interval Time) (hSub : HasSubintervalProp P) : ¬ AdmitsOptimum (eTIAProperty P μ g1) := fun h => h (eTIA_atelic_collapse P g1 hSub) /-- Atelic E-TIA is not MIP-licensed. -/ theorem eTIA_atelic_not_licensed {μ : Interval Time → ℕ} [TimeMeasure Time μ] - (P : EventPred W Time) (g1 : Interval Time) + (P : W → Event Time → Prop) (g1 : Interval Time) (hSub : HasSubintervalProp P) : ¬ MIP_Licensed (eTIAProperty P μ g1) := fun ⟨hAdm, _⟩ => eTIA_atelic_no_optimum P g1 hSub hAdm @@ -247,7 +246,7 @@ theorem eTIA_atelic_not_licensed {μ : Interval Time → ℕ} [TimeMeasure Time property is upward monotone — the same event witnesses larger measures via `TimeMeasure.extensible`. -/ theorem eTIA_telic_upwardMonotone {μ : Interval Time → ℕ} [TimeMeasure Time μ] - (P : EventPred W Time) (g1 : Interval Time) : + (P : W → Event Time → Prop) (g1 : Interval Time) : IsUpwardMonotone (eTIAProperty P μ g1) := by intro n m hnm w ⟨t, hμ, e, hP, hg1, hsub⟩ have h_le : μ t ≤ m := by rw [hμ]; exact hnm diff --git a/Linglib/Studies/Rudin2025LI.lean b/Linglib/Studies/Rudin2025LI.lean index ce58a8f0f..918cb1199 100644 --- a/Linglib/Studies/Rudin2025LI.lean +++ b/Linglib/Studies/Rudin2025LI.lean @@ -49,7 +49,6 @@ namespace Rudin2025LI open Semantics.Quotation.Demonstration open Dialogue.QuotationFBOntology open Discourse.Commitment.Table -open Semantics.Events -- ════════════════════════════════════════════════════ -- § 1. Empirical Taxonomy @@ -184,7 +183,7 @@ postulates hold by `rfl`. The discriminator for verb classes is witnesses and exclusions. -/ /-- A canonical event for each verb class, indexed by `runtime.start`. -/ -def E (n : ℕ) : Event ℕ := ⟨⟨n, n, le_refl _⟩, .action⟩ +def E (n : ℕ) : Event ℕ := ⟨⟨n, n, le_refl _⟩, .dynamic⟩ /-- The REENACT relation: per verb-class events have different REENACT targets, chosen so the postulates' universal quantifiers reduce to diff --git a/Linglib/Studies/Wellwood2015.lean b/Linglib/Studies/Wellwood2015.lean index 71298829e..d2403b62f 100644 --- a/Linglib/Studies/Wellwood2015.lean +++ b/Linglib/Studies/Wellwood2015.lean @@ -267,7 +267,6 @@ def patientPlaygroundDatum : StateModificationDatum := -- § 7. Compositional Pieces (§2.1 eqs. 37–38) -- ════════════════════════════════════════════════════ -open Semantics.Events (Event EvPred) open Semantics.ArgumentStructure (ThematicFrame EventModifier modifiedStativeLogicalForm stativeLogicalForm modify modified_stative_is_pm) open Semantics.Measurement @@ -459,7 +458,7 @@ def thanDegrees {Ent α Measured : Type*} Role: Agent. Extract: themeOf (the consumed/affected entity). -/ def nominalComparative {Entity Time : Type*} [LinearOrder Time] (frame : ThematicFrame Entity Time) - (P : EvPred Time) (themeOf : Event Time → Entity) + (P : Event Time → Prop) (themeOf : Event Time → Entity) (μ : Entity → ℚ) (a b : Entity) : Prop := comparativeTruth frame.agent P themeOf μ a b @@ -469,7 +468,7 @@ def nominalComparative {Entity Time : Type*} [LinearOrder Time] Measured domain: events directly (extract = id). Role: Agent. -/ def verbalComparative {Entity Time : Type*} [LinearOrder Time] (frame : ThematicFrame Entity Time) - (P : EvPred Time) (μ : Event Time → ℚ) (a b : Entity) : Prop := + (P : Event Time → Prop) (μ : Event Time → ℚ) (a b : Entity) : Prop := comparativeTruth frame.agent P id μ a b /-- Adjectival comparative (§3.2, eq. 65): @@ -478,7 +477,7 @@ def verbalComparative {Entity Time : Type*} [LinearOrder Time] Measured domain: states directly (extract = id). Role: Holder. -/ def adjectivalComparative {Entity Time : Type*} [LinearOrder Time] (frame : ThematicFrame Entity Time) - (P : EvPred Time) (μ : Event Time → ℚ) (a b : Entity) : Prop := + (P : Event Time → Prop) (μ : Event Time → ℚ) (a b : Entity) : Prop := comparativeTruth frame.holder P id μ a b -- ════════════════════════════════════════════════════ @@ -545,7 +544,7 @@ theorem comparativeTruth_max {Ent α Measured : Type*} /-- Adjectival comparative under maximality reduces to `μ(sb) < μ(sa)`. -/ theorem adjectival_max_reduces {Entity Time : Type*} [LinearOrder Time] {frame : ThematicFrame Entity Time} - {P : EvPred Time} {μ : Event Time → ℚ} + {P : Event Time → Prop} {μ : Event Time → ℚ} {a b : Entity} {sa sb : Event Time} (ha : frame.holder a sa ∧ P sa) (ha_unique : ∀ s, frame.holder a s → P s → s = sa) @@ -565,7 +564,7 @@ theorem statesComparativeSem_is_lt {S D : Type*} [Preorder S] [Preorder D] (Rett/Schwarzschild) on measured values. -/ theorem max_eq_comparativeSem {Entity Time Measured : Type*} [LinearOrder Time] {role : Entity → Event Time → Prop} - {P : EvPred Time} + {P : Event Time → Prop} {extract : Event Time → Measured} {μ : Measured → ℚ} {a b : Entity} {ea eb : Event Time} @@ -727,7 +726,7 @@ theorem droveMore_not_restricted : -- State modification bridge (§3.5) theorem state_mod_pm_bridge {Entity Time : Type*} [LinearOrder Time] - (P : EvPred Time) (frame : ThematicFrame Entity Time) + (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : modifiedStativeLogicalForm P frame x M ↔ stativeLogicalForm (modify P M) frame x := diff --git a/blog/references.bib b/blog/references.bib index 2494cf079..514b17c92 100644 --- a/blog/references.bib +++ b/blog/references.bib @@ -1481,6 +1481,33 @@ @article{giles-etal-2026 role = {formalized}, sources = {Phenomena/Reference/Studies/GilesEtAl2026.lean;Core/SearchEfficiency.lean;Core/PropertyDomain.lean;Pragmatics/RSA/Core/Noise.lean} } +@incollection{moltmann-2025, + author = {Moltmann, Friederike}, + year = {2025}, + title = {Events in Contemporary Semantics}, + booktitle = {21st-Century Philosophy of Events: Beyond the Analytic/Continental Divide}, + editor = {Bahoh, James and Cassina, Marta and Genovesi, Sergio}, + publisher = {Edinburgh University Press}, + url = {https://hal.science/hal-05014906}, + subfield = {semantics/lexical}, + validated = {true}, + role = {cited}, + sources = {Semantics/ArgumentStructure/ArgumentIntroduction.lean;Studies/Pylkkanen2008.lean} +} +@article{hopperdietzel-2024, + author = {Hopperdietzel, Jens}, + year = {2024}, + title = {Manner/result polysemy as contextual allosemy: Evidence from {Daakaka}}, + journal = {Natural Language \& Linguistic Theory}, + volume = {43}, + number = {1}, + pages = {273--330}, + doi = {10.1007/s11049-024-09616-6}, + subfield = {semantics/lexical}, + validated = {true}, + role = {cited}, + sources = {Semantics/ArgumentStructure/ArgumentIntroduction.lean} +} @article{regier-etal-2007, author = {Regier, Terry and Kay, Paul and Khetarpal, Naveen}, year = {2007},