From 6e327a3208889c3a307bc72aae5e4b8269986c6c Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 09:50:40 -0700 Subject: [PATCH 1/4] refactor(Syntax/Minimalist/Category): extended projections --- Linglib/Syntax/Cartography.lean | 6 +- Linglib/Syntax/Minimalist/Category/Basic.lean | 93 +++++---- .../Category/ExtendedProjection.lean | 177 ++++++++++++++++++ .../Category/FunctionalSequence.lean | 137 -------------- Linglib/Syntax/Minimalist/Clause/Spine.lean | 2 +- Studies/Borer2005.lean | 2 +- Studies/Borer2013.lean | 2 +- Studies/BrananErlewine2023.lean | 2 +- Studies/Dendikken1995.lean | 2 +- Studies/LiuYip2026.lean | 2 +- Studies/Major2024.lean | 2 +- Studies/Panagiotidis2015.lean | 2 +- references.bib | 24 ++- 13 files changed, 267 insertions(+), 186 deletions(-) create mode 100644 Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean delete mode 100644 Linglib/Syntax/Minimalist/Category/FunctionalSequence.lean diff --git a/Linglib/Syntax/Cartography.lean b/Linglib/Syntax/Cartography.lean index faf83e1308..dbcdc06f6d 100644 --- a/Linglib/Syntax/Cartography.lean +++ b/Linglib/Syntax/Cartography.lean @@ -1,7 +1,7 @@ module public import Linglib.Core.Order.OrdConnected -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Mathlib.Order.Interval.Set.LinearOrder public import Mathlib.Tactic.DeriveFintype @@ -22,8 +22,8 @@ form the interval `Set.Ioc a b` (`Set.Iic_sdiff_Iic`). A later proposal that add Cinque's refines the order: its hierarchy receives an order embedding of `Cartography.Head`, and a head it places immediately above or below one of Cinque's covers it or is covered by it. The categorial features of `Minimalist.Cat` coarsen the order: `Cartography.Head.cat` sends each head -to its category, and a higher head's category is at least as high in the functional sequence, -so each level of the sequence is an interval of the hierarchy. Cinque's own kinds of head are not: +to its category, and a higher head's category has at least as high an F-value in the verbal +extended projection, so each F-value is taken by an interval of the hierarchy. Cinque's own kinds of head are not: moods, modalities, tenses and aspects interleave. ## Main definitions diff --git a/Linglib/Syntax/Minimalist/Category/Basic.lean b/Linglib/Syntax/Minimalist/Category/Basic.lean index 8320e4386b..a78523f58e 100644 --- a/Linglib/Syntax/Minimalist/Category/Basic.lean +++ b/Linglib/Syntax/Minimalist/Category/Basic.lean @@ -28,45 +28,74 @@ namespace Minimalist /-- The categorial features, the head categories of the clausal spine and the nominal and adpositional extended projections. -/ inductive Cat where - | V -- verb - | N -- noun - | A -- adjective - | P -- preposition - | D -- determiner - | T -- tense - | C -- complementizer - | v -- little v: the verbal categorizer, or the light verb above the root - | n -- nominal categorizer / gender (little-n, [marantz-2001]; Distributed Morphology) - | a -- adjectival categorizer (little-a, [panagiotidis-2015]; DegP complement) - | Place -- locational head ([dendikken-2010]; PlaceP, F1 in adpositional EP) - | Path -- directional head ([dendikken-2010] [svenonius-2010]; PathP, F2 in adpositional EP) - | Num -- number ([ritter-1991]; NumP between nP and QP/DP) - | Dem -- demonstrative ([cinque-2005]; DemP above NumP in the nominal extended projection) - | Q -- quantity / classifier ([borer-2005]; QP between NumP and DP) - | Voice -- Voice head ([kratzer-1996]; [schaefer-2008]) - | Appl -- Applicative head ([pylkkanen-2008]; [cuervo-2003]) - | Foc -- focus ([rizzi-1997] split-CP; hosts [FoC] feature, triggers A-bar movement) - | Top -- topic ([rizzi-1997] split-CP; hosts [G]/givenness, topic fronting) - | Fin -- finiteness ([rizzi-1997] split-CP; allocutive probe in Magahi/Galician) - | SA -- speech act head ([speas-tenny-2003]; hosts speaker/addressee) + /-- The verb. -/ + | V + /-- The noun. -/ + | N + /-- The adjective. -/ + | A + /-- The adposition. -/ + | P + /-- The determiner. -/ + | D + /-- Tense. -/ + | T + /-- The complementizer. -/ + | C + /-- Little v, the verbal categorizer or the light verb above the root. -/ + | v + /-- Little n, the nominal categorizer ([marantz-2001]), also the head that bears gender. -/ + | n + /-- Little a, the adjectival categorizer ([panagiotidis-2015]). -/ + | a + /-- The locational head of the adposition ([dendikken-2010]). -/ + | Place + /-- The directional head of the adposition, above Place ([dendikken-2010], [svenonius-2010]). -/ + | Path + /-- Number ([ritter-1991]), Borer's counting head, above the dividing head `Q` + ([borer-2005]). -/ + | Num + /-- The demonstrative, above number ([cinque-2005]). -/ + | Dem + /-- Borer's dividing head, the classifier position, between little n and `Num` + ([borer-2005]). -/ + | Q + /-- Voice, which introduces the external argument ([kratzer-1996], [schaefer-2008]). -/ + | Voice + /-- The applicative head ([pylkkanen-2008], [cuervo-2003]). -/ + | Appl + /-- Focus, in Rizzi's split complementizer system ([rizzi-1997]). -/ + | Foc + /-- Topic, in Rizzi's split complementizer system ([rizzi-1997]). -/ + | Top + /-- Finiteness, the lowest head of Rizzi's split complementizer system ([rizzi-1997]). -/ + | Fin + /-- The speech-act head, which hosts the speaker and the addressee ([speas-tenny-2003]). -/ + | SA /-- The say/assertion layer ([major-2021], [krifka-2023], [moulton-2009]), embedding the - content of a verbal or representational sign. Unlike the root illocutionary layer `SA`, it - is clause-internal, in the embedded left periphery with Say > Foc > T, and requires no CP - ([kiss-2023], [egressy-2026]). -/ + content of a verbal or representational sign. Unlike the root illocutionary layer `SA`, it is + clause-internal, in the embedded left periphery with Say > Foc > T, and requires no CP + ([kiss-2023], [egressy-2026]). -/ | Say - | Force -- force ([rizzi-1997] split-CP; clause-typing [decl]/[interrog]) - | Neg -- negation ([pollock-1989]; [zanuttini-1997]; hosts [±neg]) - | Mod -- modality ([cinque-1999]; modal auxiliaries) - | Rel -- relative (cartographic left periphery, [rizzi-1997]) - | Pol -- polarity ([laka-1990]; ΣP for affirmation/negation) - | Asp -- outer aspect ([cinque-1999]; above Voice, inflectional) + /-- Force, the clause-typing head at the top of Rizzi's split complementizer system + ([rizzi-1997]). -/ + | Force + /-- Negation ([pollock-1989], [zanuttini-1997]). -/ + | Neg + /-- Modality ([cinque-1999]). -/ + | Mod + /-- Polarity, Laka's Σ, for affirmation and negation ([laka-1990]). -/ + | Pol + /-- Outer aspect, inflectional and above Voice ([cinque-1999]). -/ + | Asp /-- Inner aspect ([travis-2010]): Aktionsart in the v shell, below Voice. -/ | InnerAsp - | Evid -- evidential mood ([cinque-1999]; inflectional) + /-- Evidential mood, inflectional ([cinque-1999]). -/ + | Evid /-- Mood ([cinque-1999]): the speech-act, evaluative and irrealis moods, inflectional. -/ | Mood /-- The nominalizer ([keine-2020]): the Hindi nominalized clause, a clause type distinct from - CP. -/ + CP. -/ | Nmlz /-- The inherent-case shell ([newman-2024]): KP wraps DP for oblique or inherent case. -/ | K diff --git a/Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean b/Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean new file mode 100644 index 0000000000..90e1f61fb7 --- /dev/null +++ b/Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean @@ -0,0 +1,177 @@ +module + +public import Linglib.Syntax.Minimalist.Category.Basic +public import Mathlib.Data.Nat.Basic +public import Mathlib.Order.RelClasses + +/-! +# Extended projections + +Grimshaw takes a clause or a noun phrase to be one extended projection: a lexical head together +with the functional heads above it, all sharing the categorial features of the lexical head, at +functional levels, the F-values, that do not decrease going up. Each category here belongs to one +of four families, verbal, nominal, adjectival and adpositional, each with its lexical head, and has +an F-value, a natural number that is `0` exactly at the lexical head of its family. The families +carry the categorial features `[±V, ±N]`, and the two binary features have four combinations, one +for each family, so two categories share their features exactly when they share their family. A +category extends to another when the two are of one family and the second is at least as high. +Every category extends the lexical head of its family and any two categories of one family are +comparable, so an extended projection is a chain rising from its lexical head. + +## Main definitions + +* `Minimalist.CatFamily`, `Minimalist.Cat.family`: the four families of extended projections. +* `Minimalist.CatFamily.lexical`: the lexical head of a family. +* `Minimalist.CatFeatures`, `Minimalist.Cat.features`: the features `[±V, ±N]`, read off the + family. +* `Minimalist.Cat.fValue`: the functional level of a category. +* `Minimalist.Cat.ExtendsTo`: the step relation of an extended projection, a preorder. + +## Main results + +* `Minimalist.CatFamily.features_bijective`: the features cross-classify the families. +* `Minimalist.Cat.fValue_eq_zero_iff`: the categories at level `0` are the lexical heads. +* `Minimalist.Cat.lexical_extendsTo`: every category extends the lexical head of its family. +* `Minimalist.Cat.extendsTo_total`: the categories of one family form a chain. + +## Implementation notes + +An F-value ranks the heads of one family, as Grimshaw's F-values order the heads that share +categorial features [panagiotidis-2015]; heads of different families are never compared, and each +family counts up from its lexical head at `0`. In the verbal family the left periphery is Rizzi's +Fin < Foc < Top < Force, with one topic position, the one above the focus, of the two in which +his topics recur. The Say layer of embedded speech reports sits between Foc and C as in Egressy, +and Speas and Tenny's speech-act head closes the sequence. Tense, negation, mood, modality, +polarity, outer aspect and evidentiality share the inflectional level, inner aspect shares the +level of v, and `Cartography.Head` orders the clausal heads these levels collapse. In the nominal +family Borer's dividing head `Q` lies below the counting head `Num`. Prepositions form their own +family, with den Dikken's Place and Path above them, whereas Grimshaw places P in the nominal +extended projection. + +Chomsky's features first classified the noun, the verb and the adjective; the fourth combination, +`[−V, −N]`, was given to the adposition afterwards [baker-2003]. + +## References + +* [grimshaw-2005] +* [chomsky-1970] +* [baker-2003] +* [panagiotidis-2015] +* [rizzi-1997] +* [cinque-1999] +* [borer-2005] +* [speas-tenny-2003] +* [egressy-2026] +* [dendikken-2010] +-/ + +@[expose] public section + +namespace Minimalist + +/-- The four families of extended projections, each anchored by a lexical category. -/ +inductive CatFamily + | verbal + | nominal + | adjectival + | adpositional + deriving DecidableEq, Repr + +/-- The lexical head of a family, at the foot of its extended projections. -/ +def CatFamily.lexical : CatFamily → Cat + | .verbal => .V + | .nominal => .N + | .adjectival => .A + | .adpositional => .P + +/-- The family of a category, the extended projection it belongs to. -/ +def Cat.family : Cat → CatFamily + | .V | .v | .Voice | .Appl | .T | .Foc | .Top | .Fin | .C | .SA | .Say + | .Force | .Neg | .Mod | .Mood | .Pol | .Asp | .InnerAsp | .Evid | .Nmlz => .verbal + | .N | .n | .Num | .Dem | .Q | .D | .K => .nominal + | .A | .a => .adjectival + | .P | .Place | .Path => .adpositional + +@[simp] theorem CatFamily.family_lexical (f : CatFamily) : f.lexical.family = f := by + cases f <;> rfl + +/-- The categorial features `[±V, ±N]`, which cross-classify the four lexical categories: V is +`[+V, −N]`, N is `[−V, +N]`, A is `[+V, +N]` and P is `[−V, −N]`. -/ +structure CatFeatures where + plusV : Bool + plusN : Bool + deriving DecidableEq, Repr + +/-- The features of a family are those of its lexical head. -/ +def CatFamily.features : CatFamily → CatFeatures + | .verbal => ⟨true, false⟩ + | .nominal => ⟨false, true⟩ + | .adjectival => ⟨true, true⟩ + | .adpositional => ⟨false, false⟩ + +/-- Each of the four combinations of the two features is the features of exactly one family. -/ +theorem CatFamily.features_bijective : Function.Bijective CatFamily.features := + ⟨fun a b h ↦ by cases a <;> cases b <;> simp_all [features], fun + | ⟨true, false⟩ => ⟨.verbal, rfl⟩ + | ⟨false, true⟩ => ⟨.nominal, rfl⟩ + | ⟨true, true⟩ => ⟨.adjectival, rfl⟩ + | ⟨false, false⟩ => ⟨.adpositional, rfl⟩⟩ + +/-- The features of a category are those of its family, so that every functional head inherits +the features of its lexical head. -/ +def Cat.features (c : Cat) : CatFeatures := c.family.features + +theorem Cat.features_eq_iff {c d : Cat} : c.features = d.features ↔ c.family = d.family := + CatFamily.features_bijective.injective.eq_iff + +/-- The F-value of a category is its level in its extended projection: lexical heads are at `0`, +categorizers at `1`, the inflectional domain at `2` and the left periphery from `3` up. + +| level | verbal | nominal | adjectival | adpositional | +|-------|-----------------------------------|---------|------------|--------------| +| 0 | V | N | A | P | +| 1 | v, Voice, Appl, InnerAsp | n | a | Place | +| 2 | T, Neg, Mod, Mood, Pol, Asp, Evid | Q | | Path | +| 3 | Fin, Nmlz | Num | | | +| 4 | Foc | D, Dem | | | +| 5 | Top, Say | K | | | +| 6 | C, Force | | | | +| 7 | SA | | | | -/ +def Cat.fValue : Cat → ℕ + | .V | .N | .A | .P => 0 + | .v | .n | .a | .Voice | .Appl | .InnerAsp | .Place => 1 + | .T | .Q | .Neg | .Mod | .Mood | .Pol | .Asp | .Evid | .Path => 2 + | .Fin | .Num | .Nmlz => 3 + | .Foc | .D | .Dem => 4 + | .Top | .K | .Say => 5 + | .C | .Force => 6 + | .SA => 7 + +@[simp] theorem CatFamily.fValue_lexical (f : CatFamily) : f.lexical.fValue = 0 := by + cases f <;> rfl + +/-- The categories at level `0` are exactly the lexical heads. -/ +theorem Cat.fValue_eq_zero_iff {c : Cat} : c.fValue = 0 ↔ c = c.family.lexical := by + cases c <;> decide + +/-- `c.ExtendsTo d` holds when `d` extends the projection of `c`, the two categories being of one +family and `d` at least as high, so that the extended projections are the chains of this +relation. -/ +def Cat.ExtendsTo (c d : Cat) : Prop := c.family = d.family ∧ c.fValue ≤ d.fValue + +instance : DecidableRel Cat.ExtendsTo := fun _ _ ↦ inferInstanceAs (Decidable (_ ∧ _)) + +instance : IsPreorder Cat Cat.ExtendsTo where + refl _ := ⟨rfl, le_rfl⟩ + trans _ _ _ h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩ + +/-- Every category extends the lexical head of its family. -/ +theorem Cat.lexical_extendsTo (c : Cat) : c.family.lexical.ExtendsTo c := + ⟨CatFamily.family_lexical _, by simp⟩ + +/-- Any two categories of one family are comparable. -/ +theorem Cat.extendsTo_total {c d : Cat} (h : c.family = d.family) : + c.ExtendsTo d ∨ d.ExtendsTo c := + (le_total c.fValue d.fValue).imp (⟨h, ·⟩) (⟨h.symm, ·⟩) + +end Minimalist diff --git a/Linglib/Syntax/Minimalist/Category/FunctionalSequence.lean b/Linglib/Syntax/Minimalist/Category/FunctionalSequence.lean deleted file mode 100644 index dc0bcb6295..0000000000 --- a/Linglib/Syntax/Minimalist/Category/FunctionalSequence.lean +++ /dev/null @@ -1,137 +0,0 @@ -module - -public import Linglib.Syntax.Minimalist.Category.Basic -public import Mathlib.Data.Nat.Basic -public import Mathlib.Order.RelClasses - -/-! -# The functional sequence - -This file defines the height of a category in the functional sequence and the families of -extended projections. Grimshaw takes a clause or a noun phrase to be one extended projection, a -lexical head together with the functional heads above it, all of one category family and with a -functional level, the F-value, that does not decrease going up. The F-value of each category is -a natural number, with the lexical heads at `0`, and the four families, verbal, nominal, -adjectival and adpositional, carry Chomsky's `[±V, ±N]` features, so that two categories share -those features exactly when they are of one family. A category extends to another when the two -are of one family and the second is at least as high; the extended projections are the chains -of this relation. - -## Main definitions - -* `Minimalist.Cat.fValue`: the functional level of a category. -* `Minimalist.CatFamily`, `Minimalist.Cat.family`: the four families of extended projections. -* `Minimalist.CatFeatures`, `Minimalist.Cat.features`: Chomsky's `[±V, ±N]` features, read off - the family. -* `Minimalist.Cat.ExtendsTo`: the step relation of an extended projection, a preorder. - -## Main results - -* `Minimalist.Cat.features_eq_iff`: two categories share their features iff they share their - family. - -## Implementation notes - -The F-values place the families on one scale, `n` with `v`, `Q` with `T`, `Num` with `Fin` and -`D` with `Foc`. Rizzi's order Fin < Foc < Top < Force fixes the verbal left periphery, Borer's -individuation before counting puts `Q` below `Num`, the Say layer of embedded speech reports -sits between Foc and C as in Egressy, and Speas and Tenny's speech-act head closes the verbal -sequence. Tense, negation, mood, modality, polarity, outer aspect and evidentiality share the -inflectional level, inner aspect shares the level of v, and `Cartography.Head` orders the clausal -heads these levels collapse. Prepositions form their own family, with den Dikken's Place and Path -above them, following Chomsky's `[−V, −N]`, whereas Grimshaw places P in the nominal extended -projection. - -## References - -* [grimshaw-2005] -* [chomsky-1970] -* [rizzi-1997] -* [cinque-1999] -* [borer-2005] -* [speas-tenny-2003] -* [egressy-2026] -* [dendikken-2010] --/ - -@[expose] public section - -namespace Minimalist - -/-- The four families of extended projections, each anchored by a lexical category. -/ -inductive CatFamily - | verbal - | nominal - | adjectival - | adpositional - deriving DecidableEq, Repr - -/-- The family of a category, the extended projection it belongs to. -/ -def Cat.family : Cat → CatFamily - | .V | .v | .Voice | .Appl | .T | .Foc | .Top | .Fin | .C | .SA | .Say - | .Force | .Neg | .Mod | .Mood | .Rel | .Pol | .Asp | .InnerAsp | .Evid | .Nmlz => .verbal - | .N | .n | .Num | .Dem | .Q | .D | .K => .nominal - | .A | .a => .adjectival - | .P | .Place | .Path => .adpositional - -/-- Chomsky's categorial features `[±V, ±N]`, which cross-classify the four lexical categories: -V is `[+V, −N]`, N is `[−V, +N]`, A is `[+V, +N]` and P is `[−V, −N]`. -/ -structure CatFeatures where - plusV : Bool - plusN : Bool - deriving DecidableEq, Repr - -/-- The features of a family are those of its lexical anchor. -/ -def CatFamily.features : CatFamily → CatFeatures - | .verbal => ⟨true, false⟩ - | .nominal => ⟨false, true⟩ - | .adjectival => ⟨true, true⟩ - | .adpositional => ⟨false, false⟩ - -theorem CatFamily.features_injective : Function.Injective CatFamily.features := by - intro a b h - cases a <;> cases b <;> simp_all [CatFamily.features] - -/-- The features of a category are those of its family, so that every functional head inherits -the features of its lexical anchor. -/ -def Cat.features (c : Cat) : CatFeatures := c.family.features - -theorem Cat.features_eq_iff {c d : Cat} : c.features = d.features ↔ c.family = d.family := - CatFamily.features_injective.eq_iff - -/-- The F-value of a category is its level in the functional sequence: lexical heads are at `0`, -categorizers at `1`, the inflectional domain at `2` and the left periphery from `3` up, with the -nominal and adpositional levels aligned to the verbal ones. - -| level | verbal | nominal | adjectival | adpositional | -|-------|----------------------------|---------|------------|--------------| -| 0 | V | N | A | P | -| 1 | v, Voice, Appl, InnerAsp | n | a | Place | -| 2 | T, Neg, Mod, Mood, Pol, Asp, Evid | Q | | Path | -| 3 | Fin, Nmlz | Num | | | -| 4 | Foc | D, Dem | | | -| 5 | Top, Rel, Say | K | | | -| 6 | C, Force | | | | -| 7 | SA | | | | -/ -def Cat.fValue : Cat → ℕ - | .V | .N | .A | .P => 0 - | .v | .n | .a | .Voice | .Appl | .InnerAsp | .Place => 1 - | .T | .Q | .Neg | .Mod | .Mood | .Pol | .Asp | .Evid | .Path => 2 - | .Fin | .Num | .Nmlz => 3 - | .Foc | .D | .Dem => 4 - | .Top | .Rel | .K | .Say => 5 - | .C | .Force => 6 - | .SA => 7 - -/-- `c.ExtendsTo d` holds when `d` extends the projection of `c`, the two categories being of one -family and `d` at least as high, so that the extended projections are the chains of this -relation. -/ -def Cat.ExtendsTo (c d : Cat) : Prop := c.family = d.family ∧ c.fValue ≤ d.fValue - -instance : DecidableRel Cat.ExtendsTo := fun _ _ ↦ inferInstanceAs (Decidable (_ ∧ _)) - -instance : IsPreorder Cat Cat.ExtendsTo where - refl _ := ⟨rfl, le_rfl⟩ - trans _ _ _ h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩ - -end Minimalist diff --git a/Linglib/Syntax/Minimalist/Clause/Spine.lean b/Linglib/Syntax/Minimalist/Clause/Spine.lean index 0de915987f..1c80c965a5 100644 --- a/Linglib/Syntax/Minimalist/Clause/Spine.lean +++ b/Linglib/Syntax/Minimalist/Clause/Spine.lean @@ -5,7 +5,7 @@ Authors: Robert Hawkins -/ module -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Mathlib.Data.Finset.Dedup public import Mathlib.Data.List.Chain public import Mathlib.Data.List.DropRight diff --git a/Studies/Borer2005.lean b/Studies/Borer2005.lean index 49837b2acf..3e8689e0f2 100644 --- a/Studies/Borer2005.lean +++ b/Studies/Borer2005.lean @@ -1,7 +1,7 @@ module public import Linglib.Semantics.Mereology -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Mathlib.Data.Finset.Card /-! diff --git a/Studies/Borer2013.lean b/Studies/Borer2013.lean index 63e15539e4..8d3a7d3261 100644 --- a/Studies/Borer2013.lean +++ b/Studies/Borer2013.lean @@ -1,7 +1,7 @@ module public import Linglib.Data.Examples.Borer2013 -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Studies.Embick2010 /-! diff --git a/Studies/BrananErlewine2023.lean b/Studies/BrananErlewine2023.lean index ded280adda..1c4f349867 100644 --- a/Studies/BrananErlewine2023.lean +++ b/Studies/BrananErlewine2023.lean @@ -3,7 +3,7 @@ module public import Linglib.Core.Data.RoseTree.Positions public import Linglib.Data.Examples.BrananErlewine2023 public import Linglib.Semantics.Focus.Particles -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Linglib.Syntax.Reflex public import Linglib.Syntax.Tree.Basic diff --git a/Studies/Dendikken1995.lean b/Studies/Dendikken1995.lean index 9cf239de0d..198c0b3b6f 100644 --- a/Studies/Dendikken1995.lean +++ b/Studies/Dendikken1995.lean @@ -1,6 +1,6 @@ module -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Linglib.Syntax.Voice.Basic public import Linglib.Fragments.Norwegian.Verbs public import Linglib.Data.Examples.Dendikken1995 diff --git a/Studies/LiuYip2026.lean b/Studies/LiuYip2026.lean index 61b42f2121..08a478088e 100644 --- a/Studies/LiuYip2026.lean +++ b/Studies/LiuYip2026.lean @@ -1,6 +1,6 @@ module -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection public import Linglib.Syntax.Minimalist.Clause.Size public import Linglib.Syntax.Clause.Complementation public import Linglib.Fragments.Mandarin.Adverbs diff --git a/Studies/Major2024.lean b/Studies/Major2024.lean index 5f0f6ed51c..9aa6b3deb7 100644 --- a/Studies/Major2024.lean +++ b/Studies/Major2024.lean @@ -5,7 +5,7 @@ public import Linglib.Fragments.Uyghur.Complementizers public import Linglib.Fragments.Washo.Clause public import Linglib.Semantics.Presupposition.Verb public import Studies.BakerVinokurova2010 -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection /-! # Major (2024): Re-analyzing 'say' complementation: Implications for case theory and beyond diff --git a/Studies/Panagiotidis2015.lean b/Studies/Panagiotidis2015.lean index eef201bd84..f78ef95aa0 100644 --- a/Studies/Panagiotidis2015.lean +++ b/Studies/Panagiotidis2015.lean @@ -1,7 +1,7 @@ module public import Linglib.Morphology.Word.Basic -public import Linglib.Syntax.Minimalist.Category.FunctionalSequence +public import Linglib.Syntax.Minimalist.Category.ExtendedProjection /-! # Panagiotidis (2015): Categorial Features diff --git a/references.bib b/references.bib index 5f80782e53..d4142a4a2a 100644 --- a/references.bib +++ b/references.bib @@ -8107,10 +8107,10 @@ @book{grimshaw-2005 publisher = {CSLI Publications}, isbn = {9781575864211}, url = {https://press.uchicago.edu/ucp/books/book/distributed/W/bo3626523.html}, - subfield = {semantics/compositional}, + subfield = {syntax}, role = {cited}, validated = {true}, - sources = {Studies/Borer2005.lean;Syntax/Minimalist/ExtendedProjection/ClauseSpine.lean} + sources = {Studies/Borer2005.lean;Syntax/Minimalist/Category/ExtendedProjection.lean;Syntax/Minimalist/Clause/Size.lean;Syntax/Minimalist/Clause/Spine.lean} } @article{lewis-vasishth-2005, author = {Lewis, Richard L. and Vasishth, Shravan}, @@ -20163,7 +20163,7 @@ @incollection{chomsky-1970 subfield = {syntax}, validated = {true}, role = {foundational}, - sources = {Studies/Deal2026.lean;Studies/Embick2021.lean;Studies/Panagiotidis2015.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean} + sources = {Studies/Deal2026.lean;Studies/Embick2021.lean;Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} } @book{may-1985, author = {May, Robert}, @@ -20366,6 +20366,18 @@ @book{baker-2015 role = {formalized}, sources = {Studies/Baker2015.lean;Studies/ClemDeal2024.lean} } +@book{baker-2003, + author = {Baker, Mark C.}, + year = {2003}, + title = {Lexical Categories: Verbs, Nouns, and Adjectives}, + series = {Cambridge Studies in Linguistics}, + number = {102}, + publisher = {Cambridge University Press}, + doi = {10.1017/CBO9780511615047}, + subfield = {syntax}, + role = {cited}, + sources = {Syntax/Minimalist/Category/ExtendedProjection.lean} +} @phdthesis{baier-2018, author = {Baier, Nicholas Bowen}, year = {2018}, @@ -20704,7 +20716,7 @@ @book{panagiotidis-2015 doi = {10.1017/CBO9781139811927}, validated = {true}, role = {cited}, - sources = {Studies/Panagiotidis2015.lean} + sources = {Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} } @book{borer-2005, author = {Borer, Hagit}, @@ -20716,7 +20728,7 @@ @book{borer-2005 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Studies/Borer2005.lean;Studies/DeBelderVanCraenenbroeck2015.lean;Studies/LittleMoroneyRoyer2022.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Category/FunctionalSequence.lean} + sources = {Studies/Borer2005.lean;Studies/DeBelderVanCraenenbroeck2015.lean;Studies/LittleMoroneyRoyer2022.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} } @book{borik-2006, author = {Borik, Olga}, @@ -21501,7 +21513,7 @@ @incollection{dendikken-2010 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Syntax/Minimalist/Category/FunctionalSequence.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Syntax/Minimalist/Category/ExtendedProjection.lean;Syntax/Minimalist/Category/Basic.lean} } @article{svenonius-2006, author = {Svenonius, Peter}, From 22b100b5640769ee1d91395bd7b7d878c5cfdcce Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 09:59:51 -0700 Subject: [PATCH 2/4] refactor(Syntax/Minimalist): categories and extended projections --- Linglib/Syntax/Cartography.lean | 2 +- Linglib/Syntax/Minimalist/Case/Dependent.lean | 2 +- Linglib/Syntax/Minimalist/Category.lean | 189 ++++++++++++++++++ Linglib/Syntax/Minimalist/Category/Basic.lean | 107 ---------- Linglib/Syntax/Minimalist/Clause/Spine.lean | 2 +- .../{Category => }/ExtendedProjection.lean | 81 +------- Linglib/Syntax/Minimalist/LexicalItem.lean | 2 +- .../Syntax/Minimalist/Verbal/Applicative.lean | 2 +- Studies/Borer2005.lean | 2 +- Studies/Borer2013.lean | 2 +- Studies/BrananErlewine2023.lean | 2 +- Studies/Bruening2021.lean | 2 +- Studies/Dendikken1995.lean | 2 +- Studies/Hewett2026.lean | 2 +- Studies/Landau2026.lean | 2 +- Studies/LiuYip2026.lean | 2 +- Studies/Major2024.lean | 2 +- Studies/Newman2024.lean | 2 +- Studies/Panagiotidis2015.lean | 2 +- references.bib | 42 ++-- 20 files changed, 233 insertions(+), 218 deletions(-) create mode 100644 Linglib/Syntax/Minimalist/Category.lean delete mode 100644 Linglib/Syntax/Minimalist/Category/Basic.lean rename Linglib/Syntax/Minimalist/{Category => }/ExtendedProjection.lean (56%) diff --git a/Linglib/Syntax/Cartography.lean b/Linglib/Syntax/Cartography.lean index dbcdc06f6d..7d489e1e44 100644 --- a/Linglib/Syntax/Cartography.lean +++ b/Linglib/Syntax/Cartography.lean @@ -1,7 +1,7 @@ module public import Linglib.Core.Order.OrdConnected -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection public import Mathlib.Order.Interval.Set.LinearOrder public import Mathlib.Tactic.DeriveFintype diff --git a/Linglib/Syntax/Minimalist/Case/Dependent.lean b/Linglib/Syntax/Minimalist/Case/Dependent.lean index 176c3a9b4a..fa0523eb0c 100644 --- a/Linglib/Syntax/Minimalist/Case/Dependent.lean +++ b/Linglib/Syntax/Minimalist/Case/Dependent.lean @@ -6,7 +6,7 @@ Authors: Robert Hawkins module public import Linglib.Syntax.Case.Dependent -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Linglib.Syntax.Minimalist.Probe.Basic /-! diff --git a/Linglib/Syntax/Minimalist/Category.lean b/Linglib/Syntax/Minimalist/Category.lean new file mode 100644 index 0000000000..ddb8e3d88e --- /dev/null +++ b/Linglib/Syntax/Minimalist/Category.lean @@ -0,0 +1,189 @@ +/- +Copyright (c) 2026 Robert Hawkins. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robert Hawkins +-/ +module + +public import Mathlib.Logic.Function.Basic + +/-! +# Categories + +The categories that label heads, those of the clausal spine and of the nominal and adpositional +extended projections, and the selectional stack, the categories a head selects, consumed left to +right. Each category belongs to one of four families, verbal, nominal, adjectival and +adpositional, each with its lexical head, V, N, A and P, and a functional head belongs to the +family of the lexical head it extends. The families carry the categorial features `[±V, ±N]`, and +the two binary features have four combinations, one for each family, so two categories share their +features exactly when they share their family. + +## Main definitions + +* `Minimalist.Cat`, `Minimalist.SelStack`: the categories and the selectional stack. +* `Minimalist.CatFamily`, `Minimalist.Cat.family`: the four families. +* `Minimalist.CatFamily.lexical`: the lexical head of a family. +* `Minimalist.CatFeatures`, `Minimalist.Cat.features`: the features `[±V, ±N]`, read off the + family. + +## Main results + +* `Minimalist.CatFamily.features_bijective`: the features cross-classify the families. +* `Minimalist.Cat.features_eq_iff`: two categories share their features exactly when they share + their family. + +## Implementation notes + +Chomsky's features first classified the noun, the verb and the adjective; the fourth combination, +`[−V, −N]`, was given to the adposition afterwards [baker-2003]. + +## References + +* [chomsky-1970] +* [baker-2003] +* [chomsky-2013] +-/ + +@[expose] public section + +namespace Minimalist + +/-- The categories that label heads, those of the clausal spine and of the nominal and +adpositional extended projections. -/ +inductive Cat where + /-- The verb. -/ + | V + /-- The noun. -/ + | N + /-- The adjective. -/ + | A + /-- The adposition. -/ + | P + /-- The determiner. -/ + | D + /-- Tense. -/ + | T + /-- The complementizer. -/ + | C + /-- Little v, the verbal categorizer or the light verb above the root. -/ + | v + /-- Little n, the nominal categorizer ([marantz-2001]), also the head that bears gender. -/ + | n + /-- Little a, the adjectival categorizer ([panagiotidis-2015]). -/ + | a + /-- The locational head of the adposition ([dendikken-2010]). -/ + | Place + /-- The directional head of the adposition, above Place ([dendikken-2010], [svenonius-2010]). -/ + | Path + /-- Number ([ritter-1991]), Borer's counting head, above the dividing head `Q` + ([borer-2005]). -/ + | Num + /-- The demonstrative, above number ([cinque-2005]). -/ + | Dem + /-- Borer's dividing head, the classifier position, between little n and `Num` + ([borer-2005]). -/ + | Q + /-- Voice, which introduces the external argument ([kratzer-1996], [schaefer-2008]). -/ + | Voice + /-- The applicative head ([pylkkanen-2008], [cuervo-2003]). -/ + | Appl + /-- Focus, in Rizzi's split complementizer system ([rizzi-1997]). -/ + | Foc + /-- Topic, in Rizzi's split complementizer system ([rizzi-1997]). -/ + | Top + /-- Finiteness, the lowest head of Rizzi's split complementizer system ([rizzi-1997]). -/ + | Fin + /-- The speech-act head, which hosts the speaker and the addressee ([speas-tenny-2003]). -/ + | SA + /-- The say/assertion layer ([major-2021], [krifka-2023], [moulton-2009]), embedding the + content of a verbal or representational sign. Unlike the root illocutionary layer `SA`, it is + clause-internal, in the embedded left periphery with Say > Foc > T, and requires no CP + ([kiss-2023], [egressy-2026]). -/ + | Say + /-- Force, the clause-typing head at the top of Rizzi's split complementizer system + ([rizzi-1997]). -/ + | Force + /-- Negation ([pollock-1989], [zanuttini-1997]). -/ + | Neg + /-- Modality ([cinque-1999]). -/ + | Mod + /-- Polarity, Laka's Σ, for affirmation and negation ([laka-1990]). -/ + | Pol + /-- Outer aspect, inflectional and above Voice ([cinque-1999]). -/ + | Asp + /-- Inner aspect ([travis-2010]): Aktionsart in the v shell, below Voice. -/ + | InnerAsp + /-- Evidential mood, inflectional ([cinque-1999]). -/ + | Evid + /-- Mood ([cinque-1999]): the speech-act, evaluative and irrealis moods, inflectional. -/ + | Mood + /-- The nominalizer ([keine-2020]): the Hindi nominalized clause, a clause type distinct from + CP. -/ + | Nmlz + /-- The inherent-case shell ([newman-2024]): KP wraps DP for oblique or inherent case. -/ + | K + deriving Repr, DecidableEq, Inhabited + +/-- A selectional stack, consumed left to right. -/ +abbrev SelStack := List Cat + +/-! ### Families -/ + +/-- The four families of extended projections, each anchored by a lexical category. -/ +inductive CatFamily + | verbal + | nominal + | adjectival + | adpositional + deriving DecidableEq, Repr + +/-- The lexical head of a family, at the foot of its extended projections. -/ +def CatFamily.lexical : CatFamily → Cat + | .verbal => .V + | .nominal => .N + | .adjectival => .A + | .adpositional => .P + +/-- The family of a category, the extended projection it belongs to. -/ +def Cat.family : Cat → CatFamily + | .V | .v | .Voice | .Appl | .T | .Foc | .Top | .Fin | .C | .SA | .Say + | .Force | .Neg | .Mod | .Mood | .Pol | .Asp | .InnerAsp | .Evid | .Nmlz => .verbal + | .N | .n | .Num | .Dem | .Q | .D | .K => .nominal + | .A | .a => .adjectival + | .P | .Place | .Path => .adpositional + +@[simp] theorem CatFamily.family_lexical (f : CatFamily) : f.lexical.family = f := by + cases f <;> rfl + +/-! ### Categorial features -/ + +/-- The categorial features `[±V, ±N]`, which cross-classify the four lexical categories: V is +`[+V, −N]`, N is `[−V, +N]`, A is `[+V, +N]` and P is `[−V, −N]`. -/ +structure CatFeatures where + plusV : Bool + plusN : Bool + deriving DecidableEq, Repr + +/-- The features of a family are those of its lexical head. -/ +def CatFamily.features : CatFamily → CatFeatures + | .verbal => ⟨true, false⟩ + | .nominal => ⟨false, true⟩ + | .adjectival => ⟨true, true⟩ + | .adpositional => ⟨false, false⟩ + +/-- Each of the four combinations of the two features is the features of exactly one family. -/ +theorem CatFamily.features_bijective : Function.Bijective CatFamily.features := + ⟨fun a b h ↦ by cases a <;> cases b <;> simp_all [features], fun + | ⟨true, false⟩ => ⟨.verbal, rfl⟩ + | ⟨false, true⟩ => ⟨.nominal, rfl⟩ + | ⟨true, true⟩ => ⟨.adjectival, rfl⟩ + | ⟨false, false⟩ => ⟨.adpositional, rfl⟩⟩ + +/-- The features of a category are those of its family, so that every functional head inherits +the features of its lexical head. -/ +def Cat.features (c : Cat) : CatFeatures := c.family.features + +theorem Cat.features_eq_iff {c d : Cat} : c.features = d.features ↔ c.family = d.family := + CatFamily.features_bijective.injective.eq_iff + +end Minimalist diff --git a/Linglib/Syntax/Minimalist/Category/Basic.lean b/Linglib/Syntax/Minimalist/Category/Basic.lean deleted file mode 100644 index a78523f58e..0000000000 --- a/Linglib/Syntax/Minimalist/Category/Basic.lean +++ /dev/null @@ -1,107 +0,0 @@ -/- -Copyright (c) 2026 Robert Hawkins. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Robert Hawkins --/ -module - -/-! -# Categories - -The categorial features that label heads, the categories of the clausal spine and of the nominal -and adpositional extended projections, and the selectional stack, the categories a head selects, -consumed left to right. - -## Main definitions - -* `Minimalist.Cat`, `Minimalist.SelStack` - -## References - -* [chomsky-2013] --/ - -@[expose] public section - -namespace Minimalist - -/-- The categorial features, the head categories of the clausal spine and the nominal and - adpositional extended projections. -/ -inductive Cat where - /-- The verb. -/ - | V - /-- The noun. -/ - | N - /-- The adjective. -/ - | A - /-- The adposition. -/ - | P - /-- The determiner. -/ - | D - /-- Tense. -/ - | T - /-- The complementizer. -/ - | C - /-- Little v, the verbal categorizer or the light verb above the root. -/ - | v - /-- Little n, the nominal categorizer ([marantz-2001]), also the head that bears gender. -/ - | n - /-- Little a, the adjectival categorizer ([panagiotidis-2015]). -/ - | a - /-- The locational head of the adposition ([dendikken-2010]). -/ - | Place - /-- The directional head of the adposition, above Place ([dendikken-2010], [svenonius-2010]). -/ - | Path - /-- Number ([ritter-1991]), Borer's counting head, above the dividing head `Q` - ([borer-2005]). -/ - | Num - /-- The demonstrative, above number ([cinque-2005]). -/ - | Dem - /-- Borer's dividing head, the classifier position, between little n and `Num` - ([borer-2005]). -/ - | Q - /-- Voice, which introduces the external argument ([kratzer-1996], [schaefer-2008]). -/ - | Voice - /-- The applicative head ([pylkkanen-2008], [cuervo-2003]). -/ - | Appl - /-- Focus, in Rizzi's split complementizer system ([rizzi-1997]). -/ - | Foc - /-- Topic, in Rizzi's split complementizer system ([rizzi-1997]). -/ - | Top - /-- Finiteness, the lowest head of Rizzi's split complementizer system ([rizzi-1997]). -/ - | Fin - /-- The speech-act head, which hosts the speaker and the addressee ([speas-tenny-2003]). -/ - | SA - /-- The say/assertion layer ([major-2021], [krifka-2023], [moulton-2009]), embedding the - content of a verbal or representational sign. Unlike the root illocutionary layer `SA`, it is - clause-internal, in the embedded left periphery with Say > Foc > T, and requires no CP - ([kiss-2023], [egressy-2026]). -/ - | Say - /-- Force, the clause-typing head at the top of Rizzi's split complementizer system - ([rizzi-1997]). -/ - | Force - /-- Negation ([pollock-1989], [zanuttini-1997]). -/ - | Neg - /-- Modality ([cinque-1999]). -/ - | Mod - /-- Polarity, Laka's Σ, for affirmation and negation ([laka-1990]). -/ - | Pol - /-- Outer aspect, inflectional and above Voice ([cinque-1999]). -/ - | Asp - /-- Inner aspect ([travis-2010]): Aktionsart in the v shell, below Voice. -/ - | InnerAsp - /-- Evidential mood, inflectional ([cinque-1999]). -/ - | Evid - /-- Mood ([cinque-1999]): the speech-act, evaluative and irrealis moods, inflectional. -/ - | Mood - /-- The nominalizer ([keine-2020]): the Hindi nominalized clause, a clause type distinct from - CP. -/ - | Nmlz - /-- The inherent-case shell ([newman-2024]): KP wraps DP for oblique or inherent case. -/ - | K - deriving Repr, DecidableEq, Inhabited - -/-- A selectional stack, consumed left to right. -/ -abbrev SelStack := List Cat - -end Minimalist diff --git a/Linglib/Syntax/Minimalist/Clause/Spine.lean b/Linglib/Syntax/Minimalist/Clause/Spine.lean index 1c80c965a5..caed764fa0 100644 --- a/Linglib/Syntax/Minimalist/Clause/Spine.lean +++ b/Linglib/Syntax/Minimalist/Clause/Spine.lean @@ -5,7 +5,7 @@ Authors: Robert Hawkins -/ module -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection public import Mathlib.Data.Finset.Dedup public import Mathlib.Data.List.Chain public import Mathlib.Data.List.DropRight diff --git a/Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean b/Linglib/Syntax/Minimalist/ExtendedProjection.lean similarity index 56% rename from Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean rename to Linglib/Syntax/Minimalist/ExtendedProjection.lean index 90e1f61fb7..1c97fe52c1 100644 --- a/Linglib/Syntax/Minimalist/Category/ExtendedProjection.lean +++ b/Linglib/Syntax/Minimalist/ExtendedProjection.lean @@ -1,6 +1,6 @@ module -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Mathlib.Data.Nat.Basic public import Mathlib.Order.RelClasses @@ -9,27 +9,20 @@ public import Mathlib.Order.RelClasses Grimshaw takes a clause or a noun phrase to be one extended projection: a lexical head together with the functional heads above it, all sharing the categorial features of the lexical head, at -functional levels, the F-values, that do not decrease going up. Each category here belongs to one -of four families, verbal, nominal, adjectival and adpositional, each with its lexical head, and has -an F-value, a natural number that is `0` exactly at the lexical head of its family. The families -carry the categorial features `[±V, ±N]`, and the two binary features have four combinations, one -for each family, so two categories share their features exactly when they share their family. A -category extends to another when the two are of one family and the second is at least as high. -Every category extends the lexical head of its family and any two categories of one family are -comparable, so an extended projection is a chain rising from its lexical head. +functional levels, the F-values, that do not decrease going up. The F-value of a category is a +natural number that is `0` exactly at the lexical head of its family. A category extends to +another when the two are of one family and the second is at least as high. Every category extends +the lexical head of its family and any two categories of one family are comparable, so an extended +projection is a chain rising from its lexical head; `Minimalist.ClauseSpine.IsExtendedProjection` +is a spine that is such a chain. ## Main definitions -* `Minimalist.CatFamily`, `Minimalist.Cat.family`: the four families of extended projections. -* `Minimalist.CatFamily.lexical`: the lexical head of a family. -* `Minimalist.CatFeatures`, `Minimalist.Cat.features`: the features `[±V, ±N]`, read off the - family. * `Minimalist.Cat.fValue`: the functional level of a category. * `Minimalist.Cat.ExtendsTo`: the step relation of an extended projection, a preorder. ## Main results -* `Minimalist.CatFamily.features_bijective`: the features cross-classify the families. * `Minimalist.Cat.fValue_eq_zero_iff`: the categories at level `0` are the lexical heads. * `Minimalist.Cat.lexical_extendsTo`: every category extends the lexical head of its family. * `Minimalist.Cat.extendsTo_total`: the categories of one family form a chain. @@ -48,14 +41,9 @@ family Borer's dividing head `Q` lies below the counting head `Num`. Preposition family, with den Dikken's Place and Path above them, whereas Grimshaw places P in the nominal extended projection. -Chomsky's features first classified the noun, the verb and the adjective; the fourth combination, -`[−V, −N]`, was given to the adposition afterwards [baker-2003]. - ## References * [grimshaw-2005] -* [chomsky-1970] -* [baker-2003] * [panagiotidis-2015] * [rizzi-1997] * [cinque-1999] @@ -69,61 +57,6 @@ Chomsky's features first classified the noun, the verb and the adjective; the fo namespace Minimalist -/-- The four families of extended projections, each anchored by a lexical category. -/ -inductive CatFamily - | verbal - | nominal - | adjectival - | adpositional - deriving DecidableEq, Repr - -/-- The lexical head of a family, at the foot of its extended projections. -/ -def CatFamily.lexical : CatFamily → Cat - | .verbal => .V - | .nominal => .N - | .adjectival => .A - | .adpositional => .P - -/-- The family of a category, the extended projection it belongs to. -/ -def Cat.family : Cat → CatFamily - | .V | .v | .Voice | .Appl | .T | .Foc | .Top | .Fin | .C | .SA | .Say - | .Force | .Neg | .Mod | .Mood | .Pol | .Asp | .InnerAsp | .Evid | .Nmlz => .verbal - | .N | .n | .Num | .Dem | .Q | .D | .K => .nominal - | .A | .a => .adjectival - | .P | .Place | .Path => .adpositional - -@[simp] theorem CatFamily.family_lexical (f : CatFamily) : f.lexical.family = f := by - cases f <;> rfl - -/-- The categorial features `[±V, ±N]`, which cross-classify the four lexical categories: V is -`[+V, −N]`, N is `[−V, +N]`, A is `[+V, +N]` and P is `[−V, −N]`. -/ -structure CatFeatures where - plusV : Bool - plusN : Bool - deriving DecidableEq, Repr - -/-- The features of a family are those of its lexical head. -/ -def CatFamily.features : CatFamily → CatFeatures - | .verbal => ⟨true, false⟩ - | .nominal => ⟨false, true⟩ - | .adjectival => ⟨true, true⟩ - | .adpositional => ⟨false, false⟩ - -/-- Each of the four combinations of the two features is the features of exactly one family. -/ -theorem CatFamily.features_bijective : Function.Bijective CatFamily.features := - ⟨fun a b h ↦ by cases a <;> cases b <;> simp_all [features], fun - | ⟨true, false⟩ => ⟨.verbal, rfl⟩ - | ⟨false, true⟩ => ⟨.nominal, rfl⟩ - | ⟨true, true⟩ => ⟨.adjectival, rfl⟩ - | ⟨false, false⟩ => ⟨.adpositional, rfl⟩⟩ - -/-- The features of a category are those of its family, so that every functional head inherits -the features of its lexical head. -/ -def Cat.features (c : Cat) : CatFeatures := c.family.features - -theorem Cat.features_eq_iff {c d : Cat} : c.features = d.features ↔ c.family = d.family := - CatFamily.features_bijective.injective.eq_iff - /-- The F-value of a category is its level in its extended projection: lexical heads are at `0`, categorizers at `1`, the inflectional domain at `2` and the left periphery from `3` up. diff --git a/Linglib/Syntax/Minimalist/LexicalItem.lean b/Linglib/Syntax/Minimalist/LexicalItem.lean index 4ee40fc4fc..6e0474bed2 100644 --- a/Linglib/Syntax/Minimalist/LexicalItem.lean +++ b/Linglib/Syntax/Minimalist/LexicalItem.lean @@ -6,7 +6,7 @@ Authors: Robert Hawkins module public import Mathlib.Data.Nat.Notation -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category /-! # Lexical items diff --git a/Linglib/Syntax/Minimalist/Verbal/Applicative.lean b/Linglib/Syntax/Minimalist/Verbal/Applicative.lean index 00fc2a02a8..ade49964e6 100644 --- a/Linglib/Syntax/Minimalist/Verbal/Applicative.lean +++ b/Linglib/Syntax/Minimalist/Verbal/Applicative.lean @@ -6,7 +6,7 @@ Authors: Robert Hawkins module public import Linglib.Syntax.Case.Basic -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Linglib.Syntax.Minimalist.Verbal.LittleV public import Linglib.Syntax.Minimalist.Verbal.Voice diff --git a/Studies/Borer2005.lean b/Studies/Borer2005.lean index 3e8689e0f2..1a584f4ff3 100644 --- a/Studies/Borer2005.lean +++ b/Studies/Borer2005.lean @@ -1,7 +1,7 @@ module public import Linglib.Semantics.Mereology -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection public import Mathlib.Data.Finset.Card /-! diff --git a/Studies/Borer2013.lean b/Studies/Borer2013.lean index 8d3a7d3261..6383529009 100644 --- a/Studies/Borer2013.lean +++ b/Studies/Borer2013.lean @@ -1,7 +1,7 @@ module public import Linglib.Data.Examples.Borer2013 -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.Category public import Studies.Embick2010 /-! diff --git a/Studies/BrananErlewine2023.lean b/Studies/BrananErlewine2023.lean index 1c4f349867..fbfcefe80e 100644 --- a/Studies/BrananErlewine2023.lean +++ b/Studies/BrananErlewine2023.lean @@ -3,7 +3,7 @@ module public import Linglib.Core.Data.RoseTree.Positions public import Linglib.Data.Examples.BrananErlewine2023 public import Linglib.Semantics.Focus.Particles -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection public import Linglib.Syntax.Reflex public import Linglib.Syntax.Tree.Basic diff --git a/Studies/Bruening2021.lean b/Studies/Bruening2021.lean index 6ac1646450..4d24cd505b 100644 --- a/Studies/Bruening2021.lean +++ b/Studies/Bruening2021.lean @@ -3,7 +3,7 @@ module public import Linglib.Fragments.English.Verbs.Inventory public import Linglib.Data.Examples.Bruening2021 public import Linglib.Semantics.Composition.Tree -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category /-! # Bruening (2021): implicit arguments in English double object constructions diff --git a/Studies/Dendikken1995.lean b/Studies/Dendikken1995.lean index 198c0b3b6f..238aaae1c7 100644 --- a/Studies/Dendikken1995.lean +++ b/Studies/Dendikken1995.lean @@ -1,6 +1,6 @@ module -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.Category public import Linglib.Syntax.Voice.Basic public import Linglib.Fragments.Norwegian.Verbs public import Linglib.Data.Examples.Dendikken1995 diff --git a/Studies/Hewett2026.lean b/Studies/Hewett2026.lean index 6941ff762c..abbc42000b 100644 --- a/Studies/Hewett2026.lean +++ b/Studies/Hewett2026.lean @@ -1,7 +1,7 @@ module public import Linglib.Data.Examples.Hewett2026 -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Linglib.Syntax.Minimalist.Feature.Basic public import Mathlib.Logic.Function.Basic public import Mathlib.Tactic.DeriveFintype diff --git a/Studies/Landau2026.lean b/Studies/Landau2026.lean index 9a18c27627..7921774b84 100644 --- a/Studies/Landau2026.lean +++ b/Studies/Landau2026.lean @@ -1,7 +1,7 @@ module public import Linglib.Syntax.Anaphora.Basic -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Linglib.Data.Examples.Landau2026 public import Mathlib.Data.Finset.Disjoint diff --git a/Studies/LiuYip2026.lean b/Studies/LiuYip2026.lean index 08a478088e..dfce135aaa 100644 --- a/Studies/LiuYip2026.lean +++ b/Studies/LiuYip2026.lean @@ -1,6 +1,6 @@ module -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection public import Linglib.Syntax.Minimalist.Clause.Size public import Linglib.Syntax.Clause.Complementation public import Linglib.Fragments.Mandarin.Adverbs diff --git a/Studies/Major2024.lean b/Studies/Major2024.lean index 9aa6b3deb7..f07c83b6e9 100644 --- a/Studies/Major2024.lean +++ b/Studies/Major2024.lean @@ -5,7 +5,7 @@ public import Linglib.Fragments.Uyghur.Complementizers public import Linglib.Fragments.Washo.Clause public import Linglib.Semantics.Presupposition.Verb public import Studies.BakerVinokurova2010 -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection /-! # Major (2024): Re-analyzing 'say' complementation: Implications for case theory and beyond diff --git a/Studies/Newman2024.lean b/Studies/Newman2024.lean index 54437d79c9..25417c20b2 100644 --- a/Studies/Newman2024.lean +++ b/Studies/Newman2024.lean @@ -2,7 +2,7 @@ module public import Mathlib.Data.Finset.Card public import Mathlib.Data.Finset.Max -public import Linglib.Syntax.Minimalist.Category.Basic +public import Linglib.Syntax.Minimalist.Category public import Linglib.Syntax.Tree.Projection public import Linglib.Syntax.Binding.Basic public import Linglib.Syntax.Case.Dependent diff --git a/Studies/Panagiotidis2015.lean b/Studies/Panagiotidis2015.lean index f78ef95aa0..8d4c85e33b 100644 --- a/Studies/Panagiotidis2015.lean +++ b/Studies/Panagiotidis2015.lean @@ -1,7 +1,7 @@ module public import Linglib.Morphology.Word.Basic -public import Linglib.Syntax.Minimalist.Category.ExtendedProjection +public import Linglib.Syntax.Minimalist.ExtendedProjection /-! # Panagiotidis (2015): Categorial Features diff --git a/references.bib b/references.bib index d4142a4a2a..0a9ed27f09 100644 --- a/references.bib +++ b/references.bib @@ -8110,7 +8110,7 @@ @book{grimshaw-2005 subfield = {syntax}, role = {cited}, validated = {true}, - sources = {Studies/Borer2005.lean;Syntax/Minimalist/Category/ExtendedProjection.lean;Syntax/Minimalist/Clause/Size.lean;Syntax/Minimalist/Clause/Spine.lean} + sources = {Studies/Borer2005.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/Clause/Size.lean;Syntax/Minimalist/Clause/Spine.lean} } @article{lewis-vasishth-2005, author = {Lewis, Richard L. and Vasishth, Shravan}, @@ -13443,7 +13443,7 @@ @article{egressy-2026 subfield = {semantics/tense}, validated = {true}, role = {formalized}, - sources = {Data/Examples/Egressy2026.json;Fragments/Hungarian/Verbs.lean;Studies/Egressy2026.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Data/Examples/Egressy2026.json;Fragments/Hungarian/Verbs.lean;Studies/Egressy2026.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category.lean} } @incollection{sharvit-2020, author = {Sharvit, Yael}, @@ -13477,7 +13477,7 @@ @phdthesis{major-2021 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Fragments/Uyghur/Complementizers.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Fragments/Uyghur/Complementizers.lean;Syntax/Minimalist/Category.lean} } @phdthesis{moulton-2009, author = {Moulton, Keir}, @@ -13487,7 +13487,7 @@ @phdthesis{moulton-2009 subfield = {semantics/attitudes}, validated = {true}, role = {cited}, - sources = {Studies/Halpert2019.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Studies/Halpert2019.lean;Syntax/Minimalist/Category.lean} } @incollection{krifka-2023, author = {Krifka, Manfred}, @@ -13525,7 +13525,7 @@ @article{kiss-2023 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Studies/Egressy2026.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Studies/Egressy2026.lean;Syntax/Minimalist/Category.lean} } @inproceedings{kauf-zeijlstra-2018, author = {Kauf, Carina and Zeijlstra, Hedde}, @@ -19683,7 +19683,7 @@ @incollection{kratzer-1996 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Morphology/DistributedMorphology/Allosemy.lean;Semantics/ArgumentStructure/Linking.lean;Semantics/ArgumentStructure/Unaccusativity.lean;Semantics/ArgumentStructure/Valency.lean;Semantics/Composition/EventIdentification.lean;Semantics/Composition/Tree.lean;Semantics/Composition/Ty.lean;Studies/Bruening2001.lean;Studies/Coon2019.lean;Studies/Embick2010.lean;Studies/Kalyakin2026.lean;Studies/Kratzer1996.lean;Studies/MartinRoseNichols2025.lean;Studies/Merchant2013.lean;Studies/Ozaki2026.lean;Studies/Pylkkanen2008.lean;Studies/StapsRooryck2024.lean;Studies/Storment2026.lean;Studies/Wellwood2015.lean;Studies/White2014.lean;Syntax/Category/Verb/Defs.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Voice.lean} + sources = {Morphology/DistributedMorphology/Allosemy.lean;Semantics/ArgumentStructure/Linking.lean;Semantics/ArgumentStructure/Unaccusativity.lean;Semantics/ArgumentStructure/Valency.lean;Semantics/Composition/EventIdentification.lean;Semantics/Composition/Tree.lean;Semantics/Composition/Ty.lean;Studies/Bruening2001.lean;Studies/Coon2019.lean;Studies/Embick2010.lean;Studies/Kalyakin2026.lean;Studies/Kratzer1996.lean;Studies/MartinRoseNichols2025.lean;Studies/Merchant2013.lean;Studies/Ozaki2026.lean;Studies/Pylkkanen2008.lean;Studies/StapsRooryck2024.lean;Studies/Storment2026.lean;Studies/Wellwood2015.lean;Studies/White2014.lean;Syntax/Category/Verb/Defs.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Voice.lean} } @book{schaefer-2008, author = {Sch\"{a}fer, Florian}, @@ -20163,7 +20163,7 @@ @incollection{chomsky-1970 subfield = {syntax}, validated = {true}, role = {foundational}, - sources = {Studies/Deal2026.lean;Studies/Embick2021.lean;Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} + sources = {Studies/Deal2026.lean;Studies/Embick2021.lean;Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category.lean} } @book{may-1985, author = {May, Robert}, @@ -20323,7 +20323,7 @@ @article{chomsky-2013 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Studies/Boskovic2018.lean;Studies/Chomsky2013.lean;Studies/Chomsky2015.lean;Data/Examples/Chomsky2013.json;Syntax/Minimalist/Label/MinimalSearch.lean;Syntax/Minimalist/Locality/Phase.lean;Syntax/Minimalist/SyntacticObject/Position.lean;Syntax/Projection.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Studies/Boskovic2018.lean;Studies/Chomsky2013.lean;Studies/Chomsky2015.lean;Data/Examples/Chomsky2013.json;Syntax/Minimalist/Label/MinimalSearch.lean;Syntax/Minimalist/Locality/Phase.lean;Syntax/Minimalist/SyntacticObject/Position.lean;Syntax/Projection.lean;Syntax/Minimalist/Category.lean} } @incollection{chomsky-2015, author = {Chomsky, Noam}, @@ -20376,7 +20376,7 @@ @book{baker-2003 doi = {10.1017/CBO9780511615047}, subfield = {syntax}, role = {cited}, - sources = {Syntax/Minimalist/Category/ExtendedProjection.lean} + sources = {Syntax/Minimalist/Category.lean} } @phdthesis{baier-2018, author = {Baier, Nicholas Bowen}, @@ -20701,7 +20701,7 @@ @incollection{ritter-1991 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Ellipsis.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Ellipsis.lean;Syntax/Minimalist/Category.lean} } @book{panagiotidis-2015, author = {Panagiotidis, Phoevos}, @@ -20716,7 +20716,7 @@ @book{panagiotidis-2015 doi = {10.1017/CBO9781139811927}, validated = {true}, role = {cited}, - sources = {Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} + sources = {Studies/Panagiotidis2015.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean} } @book{borer-2005, author = {Borer, Hagit}, @@ -20728,7 +20728,7 @@ @book{borer-2005 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Studies/Borer2005.lean;Studies/DeBelderVanCraenenbroeck2015.lean;Studies/LittleMoroneyRoyer2022.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Category/ExtendedProjection.lean} + sources = {Studies/Borer2005.lean;Studies/DeBelderVanCraenenbroeck2015.lean;Studies/LittleMoroneyRoyer2022.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean} } @book{borik-2006, author = {Borik, Olga}, @@ -21513,7 +21513,7 @@ @incollection{dendikken-2010 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Syntax/Minimalist/Category/ExtendedProjection.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/Category.lean} } @article{svenonius-2006, author = {Svenonius, Peter}, @@ -21540,7 +21540,7 @@ @incollection{svenonius-2010 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Syntax/Category/Adposition/Basic.lean;Syntax/Category/Adposition/Spatial.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Syntax/Category/Adposition/Basic.lean;Syntax/Category/Adposition/Spatial.lean;Syntax/Minimalist/Category.lean} } @incollection{broekhuis-corver-2026a, author = {Broekhuis, Hans and Corver, Norbert}, @@ -22232,7 +22232,7 @@ @article{pollock-1989 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Data/Examples/ArregiPietraszko2021.json;Data/Examples/HarizanovGribanova2019.json;Fragments/Ga/Clause.lean;Studies/ArregiPietraszko2021.lean;Studies/Pollock1989.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Data/Examples/ArregiPietraszko2021.json;Data/Examples/HarizanovGribanova2019.json;Fragments/Ga/Clause.lean;Studies/ArregiPietraszko2021.lean;Studies/Pollock1989.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Category.lean} } @book{henry-1995, author = {Henry, Alison}, @@ -23944,7 +23944,7 @@ @book{pylkkanen-2008 subfield = {syntax}, role = {cited}, validated = {true}, - sources = {Semantics/ArgumentStructure/Linking.lean;Studies/Bruening2001.lean;Studies/Bruening2021.lean;Studies/Hewett2026.lean;Studies/Pylkkanen2008.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Applicative.lean;Syntax/Minimalist/Verbal/LittleV.lean;Syntax/Minimalist/Verbal/Voice.lean;Syntax/Minimalist/Category/Basic.lean;Studies/Harley2017.lean} + sources = {Semantics/ArgumentStructure/Linking.lean;Studies/Bruening2001.lean;Studies/Bruening2021.lean;Studies/Hewett2026.lean;Studies/Pylkkanen2008.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Applicative.lean;Syntax/Minimalist/Verbal/LittleV.lean;Syntax/Minimalist/Verbal/Voice.lean;Syntax/Minimalist/Category.lean;Studies/Harley2017.lean} } @article{stiebels-2006, author = {Stiebels, Barbara}, @@ -24978,7 +24978,7 @@ @book{keine-2020 subfield = {syntax}, role = {formalized}, validated = {true}, - sources = {Studies/Egressy2026.lean;Studies/Keine2019.lean;Studies/Keine2020.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/ClauseSpine.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Locality/Horizon.lean} + sources = {Studies/Egressy2026.lean;Studies/Keine2019.lean;Studies/Keine2020.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/ClauseSpine.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/Locality/Horizon.lean} } @article{keine-2019, author = {Keine, Stefan}, @@ -26670,7 +26670,7 @@ @article{cinque-2005 subfield = {syntax}, role = {formalized}, validated = {true}, - sources = {Studies/Cinque2005.lean;Studies/Cinque2020.lean;Studies/StanojevicSteedman2021.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/Linearization/Replay.lean} + sources = {Studies/Cinque2005.lean;Studies/Cinque2020.lean;Studies/StanojevicSteedman2021.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/Linearization/Replay.lean} } @book{cinque-2020, author = {Cinque, Guglielmo}, @@ -27926,7 +27926,7 @@ @book{cinque-1999 role = {formalized}, doi = {10.1093/oso/9780195115260.001.0001}, validated = {true}, - sources = {Fragments/Romance/Italian/PolarityItems.lean;Studies/Cinque1999.lean;Studies/Erlewine2016.lean;Studies/Hacquard2010.lean;Studies/HoleFraser2026.lean;Studies/Narrog2012.lean;Studies/RamchandSvenonius2014.lean;Studies/SpeasTenny2003.lean;Syntax/Cartography.lean;Syntax/Minimalist/Category/Basic.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean} + sources = {Fragments/Romance/Italian/PolarityItems.lean;Studies/Cinque1999.lean;Studies/Erlewine2016.lean;Studies/Hacquard2010.lean;Studies/HoleFraser2026.lean;Studies/Narrog2012.lean;Studies/RamchandSvenonius2014.lean;Studies/SpeasTenny2003.lean;Syntax/Cartography.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean} } @incollection{keefe-smith-1997, author = {Keefe, Rosanna and Smith, Peter}, @@ -28022,7 +28022,7 @@ @incollection{rizzi-1997 subfield = {syntax/minimalism}, validated = {true}, role = {cited}, - sources = {Studies/Allotey2021.lean;Studies/Erlewine2016.lean;Studies/Fortuny2024.lean;Studies/FuscoSgrizzi2026.lean;Studies/Greco2020.lean;Studies/Holmberg2016.lean;Studies/SpeasTenny2003.lean;Studies/Westergaard2009.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Feature/Basic.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Studies/Allotey2021.lean;Studies/Erlewine2016.lean;Studies/Fortuny2024.lean;Studies/FuscoSgrizzi2026.lean;Studies/Greco2020.lean;Studies/Holmberg2016.lean;Studies/SpeasTenny2003.lean;Studies/Westergaard2009.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Feature/Basic.lean;Syntax/Minimalist/Category.lean} } @inproceedings{zeijlstra-2007, @@ -44489,7 +44489,7 @@ @book{travis-2010 subfield = {syntax}, validated = {true}, role = {cited}, - sources = {Studies/LiuYip2026.lean;Syntax/Minimalist/Category/Basic.lean} + sources = {Studies/LiuYip2026.lean;Syntax/Minimalist/Category.lean} } @book{macdonald-2008, From fed6ad77b822d97888d316abbe9df5f83020f445 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 11:15:52 -0700 Subject: [PATCH 3/4] refactor(Syntax/Minimalist): extension order read from cited structures (#5863) --- Linglib/Syntax/Cartography.lean | 34 +-- Linglib/Syntax/Minimalist/Category.lean | 3 +- Linglib/Syntax/Minimalist/Clause/Size.lean | 81 ++++--- Linglib/Syntax/Minimalist/Clause/Spine.lean | 4 +- .../Syntax/Minimalist/ExtendedProjection.lean | 226 ++++++++++++------ Studies/Borer2005.lean | 2 +- Studies/Egressy2026.lean | 66 ++--- Studies/FuscoSgrizzi2026.lean | 12 +- Studies/LiuYip2026.lean | 81 ++++--- Studies/Major2024.lean | 9 +- Studies/Panagiotidis2015.lean | 5 +- references.bib | 28 +-- 12 files changed, 320 insertions(+), 231 deletions(-) diff --git a/Linglib/Syntax/Cartography.lean b/Linglib/Syntax/Cartography.lean index 7d489e1e44..e899221d81 100644 --- a/Linglib/Syntax/Cartography.lean +++ b/Linglib/Syntax/Cartography.lean @@ -1,7 +1,7 @@ module public import Linglib.Core.Order.OrdConnected -public import Linglib.Syntax.Minimalist.ExtendedProjection +public import Linglib.Syntax.Minimalist.Category public import Mathlib.Order.Interval.Set.LinearOrder public import Mathlib.Tactic.DeriveFintype @@ -20,10 +20,10 @@ A clause that projects up to a head contains every head below it, so the heads o `h` are the lower set `Set.Iic h`, and the heads in a clause of size `b` but not in one of size `a` form the interval `Set.Ioc a b` (`Set.Iic_sdiff_Iic`). A later proposal that adds heads to Cinque's refines the order: its hierarchy receives an order embedding of `Cartography.Head`, and a -head it places immediately above or below one of Cinque's covers it or is covered by it. The -categorial features of `Minimalist.Cat` coarsen the order: `Cartography.Head.cat` sends each head -to its category, and a higher head's category has at least as high an F-value in the verbal -extended projection, so each F-value is taken by an interval of the hierarchy. Cinque's own kinds of head are not: +head it places immediately above or below one of Cinque's covers it or is covered by it. +`Cartography.Head.cat` sends each head to its category in `Minimalist.Cat`, and the list +`Cartography.Head.hierarchy` of the heads bottom-up is one of the structures the extension order +of `Minimalist.Cat` is read from. Cinque's own kinds of head are not intervals of the hierarchy: moods, modalities, tenses and aspects interleave. ## Main definitions @@ -31,11 +31,12 @@ moods, modalities, tenses and aspects interleave. * `Cartography.Head`: the heads of the universal hierarchy, with its linear order. * `Cartography.Head.family`: the kind of head, `Cartography.Family`. * `Cartography.Head.cat`: the category of a head in `Minimalist.Cat`. +* `Cartography.Head.hierarchy`: the heads bottom-up, as a list. ## Main statements -* `Cartography.Head.monotone_fValue_cat`: the F-values of the categories are monotone in the - hierarchy. +* `Cartography.Head.mem_hierarchy`, `Cartography.Head.pairwise_hierarchy`: the list holds every + head once, in order. * `Cartography.Head.not_isContiguous_family`: the kinds of head are not intervals of it. ## Implementation notes @@ -48,12 +49,14 @@ moods, modalities, tenses and aspects interleave. * Cinque marks the pairing of *characteristically* with generic or progressive aspect, and the head of *always*, as uncertain. * `Head.cat` sends Cinque's four aspect heads below Voice to inner aspect, the aspect of the v - shell, the other aspect heads to outer aspect, and the moods other than the evidential to - `Cat.Mood`. + shell, the other aspect heads to outer aspect, the speech-act mood to the speech-act head, as + Speas and Tenny project their speech-act phrase from Cinque's speech-act mood head, and the + other moods but the evidential to `Cat.Mood`. ## References * [cinque-1999] +* [speas-tenny-2003] -/ @[expose] public section @@ -154,18 +157,19 @@ def cat : Head → Minimalist.Cat | tAnterior | tFuture | tPast => .T | modVolitional | modPossibility | modNecessity | modEpistemic => .Mod | moodEvidential => .Evid - | moodIrrealis | moodEvaluative | moodSpeechAct => .Mood + | moodSpeechAct => .SA + | moodIrrealis | moodEvaluative => .Mood | _ => .Asp theorem family_cat (h : Head) : h.cat.family = .verbal := by cases h <;> rfl -theorem monotone_fValue_cat : Monotone fun h : Head ↦ h.cat.fValue := by - unfold Monotone - decide +/-- The heads, bottom-up. -/ +def hierarchy : List Head := (List.range 30).map Head.ofNat + +theorem mem_hierarchy (h : Head) : h ∈ hierarchy := by cases h <;> decide -theorem isContiguous_fValue_cat : IsContiguous fun h : Head ↦ h.cat.fValue := - monotone_fValue_cat.isContiguous +theorem pairwise_hierarchy : hierarchy.Pairwise (· < ·) := by decide /-- No order on the kinds of head is coarsened by the hierarchy (`isContiguous_iff_exists_monotone`): the anterior tense and the volitional modality sit among the diff --git a/Linglib/Syntax/Minimalist/Category.lean b/Linglib/Syntax/Minimalist/Category.lean index ddb8e3d88e..ffc9cafd4c 100644 --- a/Linglib/Syntax/Minimalist/Category.lean +++ b/Linglib/Syntax/Minimalist/Category.lean @@ -80,8 +80,7 @@ inductive Cat where | Num /-- The demonstrative, above number ([cinque-2005]). -/ | Dem - /-- Borer's dividing head, the classifier position, between little n and `Num` - ([borer-2005]). -/ + /-- Borer's dividing head, the classifier position, below `Num` ([borer-2005]). -/ | Q /-- Voice, which introduces the external argument ([kratzer-1996], [schaefer-2008]). -/ | Voice diff --git a/Linglib/Syntax/Minimalist/Clause/Size.lean b/Linglib/Syntax/Minimalist/Clause/Size.lean index a9ae9b3fae..73532285f2 100644 --- a/Linglib/Syntax/Minimalist/Clause/Size.lean +++ b/Linglib/Syntax/Minimalist/Clause/Size.lean @@ -13,16 +13,16 @@ public import Linglib.Syntax.Minimalist.Clause.Spine A clausal complement is measured by its highest projected head. Wurmbrand classifies infinitival complements by the structure they project, a bare vP for restructuring, a TP for propositional attitudes and a modal projection for future infinitives, beside the full CP of a finite clause, -and a complement is at most as large as another when its highest head is no higher in the -functional sequence. Two sizes with distinct heads at one level, tense and negation for instance, -are then equivalent but not equal, so the order is a preorder. The size of a clause spine is its -highest head. On extended projections the extension order of spines, inclusion of labels, refines -the size order, and the standard sizes are those of the standard spines. +and a complement is at most as large as another when its highest head is extended by the other's. +Two sizes with distinct heads at one level, tense and negation for instance, are then equivalent +but not equal, so the order is a preorder, and two sizes no source relates, a nominalized clause +and a CP, are incomparable. The size of a clause spine is its highest head. On extended +projections the extension order of spines, inclusion of labels, refines the size order, and the +standard sizes are those of the standard spines. ## Main definitions * `Minimalist.ComplementSize`: a clausal complement measured by its highest head. -* `Minimalist.ComplementSize.fLevel`: the functional level of the highest head. * `Minimalist.ClauseSpine.size`: the size of a spine, its highest head. * `Minimalist.ComplementSize.vP`, `Minimalist.ComplementSize.tP`, `Minimalist.ComplementSize.modP`, `Minimalist.ComplementSize.finP`, @@ -30,8 +30,7 @@ the size order, and the standard sizes are those of the standard spines. ## Main results -* `Minimalist.ComplementSize.le_def`, `Minimalist.ComplementSize.lt_def`: the order is that of - functional levels. +* `Minimalist.ComplementSize.le_def`: the order is the extension order of the highest heads. * `Minimalist.ClauseSpine.size_le_size`: on extended projections, the extension order refines the size order, so that the standard sizes ascend as their spines do (`Minimalist.ComplementSize.vP_le_tP`, `Minimalist.ComplementSize.tP_le_cP`). @@ -56,20 +55,21 @@ namespace ComplementSize variable {a b : ComplementSize} -/-- The functional level of a complement is that of its highest head. -/ -def fLevel (cs : ComplementSize) : ℕ := cs.highestHead.fValue +/-- Complement sizes are ordered by the extension order of their highest heads, so that a +complement is at most another when the other's highest head extends its own. -/ +instance : Preorder ComplementSize where + le a b := a.highestHead.ExtendsTo b.highestHead + le_refl _ := refl_of Cat.ExtendsTo _ + le_trans _ _ _ := trans_of Cat.ExtendsTo -/-- Complement sizes are ordered by functional level, so that a complement is at most another when -it projects no higher in the functional sequence. -/ -instance : Preorder ComplementSize := Preorder.lift fLevel +instance : DecidableLE ComplementSize := fun a b ↦ + inferInstanceAs (Decidable (a.highestHead.ExtendsTo b.highestHead)) -instance : DecidableLE ComplementSize := fun a b ↦ inferInstanceAs (Decidable (a.fLevel ≤ b.fLevel)) +instance : DecidableLT ComplementSize := fun a b ↦ + inferInstanceAs (Decidable (a.highestHead.ExtendsTo b.highestHead ∧ + ¬ b.highestHead.ExtendsTo a.highestHead)) -instance : DecidableLT ComplementSize := fun a b ↦ inferInstanceAs (Decidable (a.fLevel < b.fLevel)) - -theorem le_def : a ≤ b ↔ a.fLevel ≤ b.fLevel := Iff.rfl - -theorem lt_def : a < b ↔ a.fLevel < b.fLevel := Iff.rfl +theorem le_def : a ≤ b ↔ a.highestHead.ExtendsTo b.highestHead := Iff.rfl end ComplementSize @@ -83,29 +83,29 @@ variable {s t : ClauseSpine} {c : Cat} the least size. -/ def size (s : ClauseSpine) : ComplementSize := ⟨s.heads.getLastD .V⟩ -private theorem fValue_le_getLastD {l : List Cat} (hp : l.Pairwise Cat.ExtendsTo) (hc : c ∈ l) : - c.fValue ≤ (l.getLastD .V).fValue := by +private theorem extendsTo_getLastD {l : List Cat} (hp : l.Pairwise Cat.ExtendsTo) (hc : c ∈ l) : + c.ExtendsTo (l.getLastD .V) := by have hne : l ≠ [] := List.ne_nil_of_mem hc rw [List.getLastD_eq_getLast?, List.getLast?_eq_some_getLast hne, Option.getD_some] rw [← List.dropLast_append_getLast hne, List.mem_append, List.mem_singleton] at hc rcases hc with hc | rfl · rw [← List.dropLast_append_getLast hne, List.pairwise_append] at hp - exact (hp.2.2 c hc _ (List.mem_singleton_self _)).2 - · exact le_rfl - -theorem IsExtendedProjection.fValue_le_fLevel (hs : s.IsExtendedProjection) (hc : c ∈ s) : - c.fValue ≤ s.size.fLevel := - fValue_le_getLastD hs.pairwise hc - -/-- On extended projections, the extension order refines the size order: a spine whose heads -another projects is no larger. -/ -theorem size_le_size (h : s ≤ t) (ht : t.IsExtendedProjection) : s.size ≤ t.size := by - rcases List.eq_nil_or_concat s.heads with hs | ⟨l, c, hs⟩ - · show (s.heads.getLastD .V).fValue ≤ t.size.fLevel - simp [hs, Cat.fValue] - · show (s.heads.getLastD .V).fValue ≤ t.size.fLevel - rw [hs, List.concat_eq_append, List.getLastD_concat] - exact ht.fValue_le_fLevel (le_iff_forall_mem.1 h c (by simp [hs])) + exact hp.2.2 c hc _ (List.mem_singleton_self _) + · exact refl_of Cat.ExtendsTo _ + +/-- In an extended projection every head is extended by the highest one. -/ +theorem IsExtendedProjection.extendsTo_size (hs : s.IsExtendedProjection) (hc : c ∈ s) : + c.ExtendsTo s.size.highestHead := + extendsTo_getLastD hs.pairwise hc + +/-- On extended projections, the extension order refines the size order: a nonempty spine whose +heads another projects is no larger. -/ +theorem size_le_size (h : s ≤ t) (ht : t.IsExtendedProjection) (hs : s.heads ≠ []) : + s.size ≤ t.size := by + obtain ⟨l, c, hlc⟩ := (List.eq_nil_or_concat s.heads).resolve_left hs + show (s.heads.getLastD .V).ExtendsTo t.size.highestHead + rw [hlc, List.concat_eq_append, List.getLastD_concat] + exact ht.extendsTo_size (le_iff_forall_mem.1 h c (by simp [hlc])) end ClauseSpine @@ -129,9 +129,12 @@ def finP : ComplementSize := ⟨.Fin⟩ def cP : ComplementSize := ClauseSpine.cP.size /-- The standard sizes ascend as their spines do. -/ -theorem vP_le_tP : vP ≤ tP := ClauseSpine.size_le_size ClauseSpine.vP_le_tP (by decide) +theorem vP_le_tP : vP ≤ tP := + ClauseSpine.size_le_size ClauseSpine.vP_le_tP (by decide +kernel) (List.cons_ne_nil _ _) -theorem tP_le_cP : tP ≤ cP := ClauseSpine.size_le_size ClauseSpine.tP_le_cP (by decide) +theorem tP_le_cP : tP ≤ cP := + ClauseSpine.size_le_size ClauseSpine.tP_le_cP ClauseSpine.cP_isExtendedProjection + (List.cons_ne_nil _ _) end ComplementSize diff --git a/Linglib/Syntax/Minimalist/Clause/Spine.lean b/Linglib/Syntax/Minimalist/Clause/Spine.lean index caed764fa0..aa358d1faf 100644 --- a/Linglib/Syntax/Minimalist/Clause/Spine.lean +++ b/Linglib/Syntax/Minimalist/Clause/Spine.lean @@ -86,7 +86,7 @@ instance (P : Cat → Prop) [DecidablePred P] (s : ClauseSpine) : Decidable (∃ /-! ### Extended projections -/ /-- A spine is an extended projection when each head extends the one below it, so that its heads -are of one family and their F-values do not decrease. -/ +are of one family. -/ def IsExtendedProjection (s : ClauseSpine) : Prop := s.heads.IsChain Cat.ExtendsTo instance (s : ClauseSpine) : Decidable s.IsExtendedProjection := @@ -171,7 +171,7 @@ theorem vP_le_tP : vP ≤ tP := by decide theorem tP_le_cP : tP ≤ cP := by decide -theorem cP_isExtendedProjection : cP.IsExtendedProjection := by decide +theorem cP_isExtendedProjection : cP.IsExtendedProjection := by decide +kernel end ClauseSpine diff --git a/Linglib/Syntax/Minimalist/ExtendedProjection.lean b/Linglib/Syntax/Minimalist/ExtendedProjection.lean index 1c97fe52c1..4a847205b5 100644 --- a/Linglib/Syntax/Minimalist/ExtendedProjection.lean +++ b/Linglib/Syntax/Minimalist/ExtendedProjection.lean @@ -1,55 +1,75 @@ module -public import Linglib.Syntax.Minimalist.Category -public import Mathlib.Data.Nat.Basic +public import Linglib.Core.Order.Antisymmetrization +public import Linglib.Core.Relation.ReflTransGen +public import Linglib.Syntax.Cartography public import Mathlib.Order.RelClasses /-! # Extended projections Grimshaw takes a clause or a noun phrase to be one extended projection: a lexical head together -with the functional heads above it, all sharing the categorial features of the lexical head, at -functional levels, the F-values, that do not decrease going up. The F-value of a category is a -natural number that is `0` exactly at the lexical head of its family. A category extends to -another when the two are of one family and the second is at least as high. Every category extends -the lexical head of its family and any two categories of one family are comparable, so an extended -projection is a chain rising from its lexical head; `Minimalist.ClauseSpine.IsExtendedProjection` -is a spine that is such a chain. +with the functional heads above it, all sharing the categorial features of the lexical head, each +at a functional level no lower than the one below it. The order of the levels is read off here +from the structures the sources draw rather than assigned head by head. Each cited structure is a +sequence of heads, bottom-up, and a source may also take two categories to be one head; a category +extends to another when a chain of cited steps leads from the first to the second. Every cited step +stays within one family, so [a category extends only to categories of its +family](##Minimalist.Cat.ExtendsTo.family_eq), and every category is reached from the lexical head +of its family, so [it extends that head](##Minimalist.Cat.lexical_extendsTo). + +Since the order collects the structures of several sources, a category one source places above +another and another source below it comes out level with it. Cinque interleaves tense, mood, +modality and aspect, Zanuttini places negation on both sides of tense and Laka places polarity +below tense in English and above it in Basque, so [these heads are mutually +level](##Minimalist.Cat.antisymmRel_T); Rizzi's topics recur on both sides of the focus, so [topic +and focus are level](##Minimalist.Cat.antisymmRel_Top_Foc). Where the sources agree the order is +strict, as along the verbal spine from the verb to Force and the nominal spine from the noun to K, +and where no source relates two heads they are incomparable: Keine's nominalized clause [neither +contains nor is contained in a CP](##Minimalist.Cat.not_extendsTo_Nmlz_C). ## Main definitions -* `Minimalist.Cat.fValue`: the functional level of a category. -* `Minimalist.Cat.ExtendsTo`: the step relation of an extended projection, a preorder. +* `Minimalist.citedSequences`, `Minimalist.citedIdentifications`: the structures the sources draw. +* `Minimalist.Cat.Step`: a cited step, from a head to the one a source merges directly above it. +* `Minimalist.Cat.ExtendsTo`: the extension order, the reflexive-transitive closure of the steps. -## Main results +## Implementation notes -* `Minimalist.Cat.fValue_eq_zero_iff`: the categories at level `0` are the lexical heads. -* `Minimalist.Cat.lexical_extendsTo`: every category extends the lexical head of its family. -* `Minimalist.Cat.extendsTo_total`: the categories of one family form a chain. +A root, a VP and the verb of a cited structure are its lexical head, an IP is `T`, Cinque's heads +are read through `Cartography.Head.cat`, and the heads of a structure that are not categories here +(Agr, Cause, Deg, Laka's English AP) are left out, its other heads kept in order. Cinque's +demonstrative and numeral are specifiers, taken as heads as his footnote allows; Zanuttini's +numbered negations are all `Neg`; Laka's Σ is `Pol`. Only the high applicative is cited: +Pylkkänen's low applicative sits below the verb, and with one `Appl` category citing both would +make the verb, v and the applicative one level. -## Implementation notes +## TODO -An F-value ranks the heads of one family, as Grimshaw's F-values order the heads that share -categorial features [panagiotidis-2015]; heads of different families are never compared, and each -family counts up from its lexical head at `0`. In the verbal family the left periphery is Rizzi's -Fin < Foc < Top < Force, with one topic position, the one above the focus, of the two in which -his topics recur. The Say layer of embedded speech reports sits between Foc and C as in Egressy, -and Speas and Tenny's speech-act head closes the sequence. Tense, negation, mood, modality, -polarity, outer aspect and evidentiality share the inflectional level, inner aspect shares the -level of v, and `Cartography.Head` orders the clausal heads these levels collapse. In the nominal -family Borer's dividing head `Q` lies below the counting head `Num`. Prepositions form their own -family, with den Dikken's Place and Path above them, whereas Grimshaw places P in the nominal -extended projection. +Inner aspect is placed by Liu and Yip's clause sizes, which follow Travis; Travis's own +structure, Kratzer's Voice, Svenonius's adpositional heads and Grimshaw's definitions are not +yet read from the sources. No cited structure relates little n to the dividing head or D to the +demonstrative, so those pairs are incomparable. ## References * [grimshaw-2005] * [panagiotidis-2015] -* [rizzi-1997] +* [harley-2013] +* [harley-2017] +* [pylkkanen-2008] +* [liu-yip-2026] +* [pollock-1989] +* [zanuttini-1997] +* [laka-1990] +* [keine-2020] * [cinque-1999] -* [borer-2005] -* [speas-tenny-2003] +* [rizzi-1997] * [egressy-2026] +* [speas-tenny-2003] +* [borer-2005] +* [cinque-2005] +* [newman-2024] * [dendikken-2010] -/ @@ -57,54 +77,108 @@ extended projection. namespace Minimalist -/-- The F-value of a category is its level in its extended projection: lexical heads are at `0`, -categorizers at `1`, the inflectional domain at `2` and the left periphery from `3` up. - -| level | verbal | nominal | adjectival | adpositional | -|-------|-----------------------------------|---------|------------|--------------| -| 0 | V | N | A | P | -| 1 | v, Voice, Appl, InnerAsp | n | a | Place | -| 2 | T, Neg, Mod, Mood, Pol, Asp, Evid | Q | | Path | -| 3 | Fin, Nmlz | Num | | | -| 4 | Foc | D, Dem | | | -| 5 | Top, Say | K | | | -| 6 | C, Force | | | | -| 7 | SA | | | | -/ -def Cat.fValue : Cat → ℕ - | .V | .N | .A | .P => 0 - | .v | .n | .a | .Voice | .Appl | .InnerAsp | .Place => 1 - | .T | .Q | .Neg | .Mod | .Mood | .Pol | .Asp | .Evid | .Path => 2 - | .Fin | .Num | .Nmlz => 3 - | .Foc | .D | .Dem => 4 - | .Top | .K | .Say => 5 - | .C | .Force => 6 - | .SA => 7 - -@[simp] theorem CatFamily.fValue_lexical (f : CatFamily) : f.lexical.fValue = 0 := by - cases f <;> rfl - -/-- The categories at level `0` are exactly the lexical heads. -/ -theorem Cat.fValue_eq_zero_iff {c : Cat} : c.fValue = 0 ↔ c = c.family.lexical := by - cases c <;> decide - -/-- `c.ExtendsTo d` holds when `d` extends the projection of `c`, the two categories being of one -family and `d` at least as high, so that the extended projections are the chains of this -relation. -/ -def Cat.ExtendsTo (c d : Cat) : Prop := c.family = d.family ∧ c.fValue ≤ d.fValue - -instance : DecidableRel Cat.ExtendsTo := fun _ _ ↦ inferInstanceAs (Decidable (_ ∧ _)) - -instance : IsPreorder Cat Cat.ExtendsTo where - refl _ := ⟨rfl, le_rfl⟩ - trans _ _ _ h₁ h₂ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩ +/-! ### The cited structures -/ + +/-- The sequences of heads the sources draw, each bottom-up. -/ +def citedSequences : List (List Cat) := + [[.V, .v], [.N, .n], [.A, .a], -- [panagiotidis-2015] (11), p. 18 + [.V, .v, .Voice, .T], -- [harley-2013] (2), p. 35 + [.V, .Appl, .Voice], -- [pylkkanen-2008] (6a), pp. 13–14 + [.v, .Appl, .Voice], -- [harley-2017] (18), p. 13 + [.V, .InnerAsp, .v, .Asp, .T, .C], -- [liu-yip-2026] (1a), p. 25 + [.V, .Neg, .T, .C], -- [pollock-1989] (77), p. 397 + [.Mod, .Mood, .Neg, .T, .Mod, .Mod], -- [zanuttini-1997] (106), p. 141 + [.Neg, .Asp, .Asp, .Neg, .T, .Neg], -- [zanuttini-1997] (139), p. 99 + [.V, .Pol, .T], [.V, .T, .Pol], -- [laka-1990] (16), p. 101 + [.T, .Pol, .C], -- [laka-1990] (46)–(47), p. 127 + [.v, .T, .Nmlz], -- [keine-2020] (106), p. 74 + [.v, .T, .C], -- [keine-2020] (238), p. 156 + [.T, .Fin, .Top, .Foc, .Top, .Force], -- [rizzi-1997] (41), p. 297 + [.T, .Foc, .Say], -- [egressy-2026] p. 14 + [.Mood, .SA], -- [speas-tenny-2003] p. 332 + [.N, .Q, .Num, .D], -- [borer-2005] (8a), p. 96 + [.N, .Num, .Dem], -- [cinque-2005] (7a), p. 321 + [.D, .K], -- [newman-2024] (217), p. 129 + [.P, .Place, .Path]] -- [dendikken-2010] (20c), p. 81 + +/-- The pairs of categories a source takes to be one head: Rizzi's *che* manifests the force +position, and Speas and Tenny's speech-act phrase is the projection that encodes force. -/ +def citedIdentifications : List (Cat × Cat) := + [(.C, .Force), -- [rizzi-1997] p. 288 + (.SA, .Force)] -- [speas-tenny-2003] p. 317 + +/-- The cited steps: each head of Cinque's hierarchy or of a cited sequence to the next one up, +and each cited identification in both directions. -/ +def citedSteps : List (Cat × Cat) := + ((Cartography.Head.hierarchy.map Cartography.Head.cat) :: citedSequences).flatMap + (fun l ↦ l.zip l.tail) ++ + citedIdentifications.flatMap fun p ↦ [p, p.swap] + +namespace Cat + +variable {c d : Cat} + +/-- `c.Step d` holds when a source merges `d` directly above `c` or takes the two to be one +head. -/ +def Step (c d : Cat) : Prop := (c, d) ∈ citedSteps + +instance : DecidableRel Step := fun c d ↦ inferInstanceAs (Decidable ((c, d) ∈ citedSteps)) + +/-- `c.ExtendsTo d` holds when a chain of cited steps leads from `c` to `d`, so that `d` can +extend the projection of `c`. -/ +def ExtendsTo : Cat → Cat → Prop := Relation.ReflTransGen Step + +/-- Reachability along the cited steps, irreducible so that elaboration never computes the +closure; `decide +kernel` evaluates it. -/ +@[irreducible] def decidableExtendsTo : DecidableRel ExtendsTo := fun c d ↦ + Relation.ReflTransGen.decidable_of_finite_step + (fun x ↦ (citedSteps.filter (·.1 == x)).map (·.2)) (citedSteps.map (·.2)) + (fun x y ↦ by simp [Step]) (fun _ _ h ↦ by + obtain ⟨p, hp, rfl⟩ := List.mem_map.1 h + exact List.mem_map_of_mem (List.mem_filter.1 hp).1) c d + +instance : DecidableRel ExtendsTo := decidableExtendsTo + +instance : IsPreorder Cat ExtendsTo where + refl _ := .refl + trans _ _ _ := .trans + +theorem Step.extendsTo (h : c.Step d) : c.ExtendsTo d := .single h + +theorem Step.family_eq (h : c.Step d) : c.family = d.family := + (by decide +kernel : ∀ p ∈ citedSteps, p.1.family = p.2.family) _ h + +/-- A category extends only to categories of its family. -/ +theorem ExtendsTo.family_eq (h : c.ExtendsTo d) : c.family = d.family := by + induction h with + | refl => rfl + | tail _ hs ih => exact ih.trans hs.family_eq /-- Every category extends the lexical head of its family. -/ -theorem Cat.lexical_extendsTo (c : Cat) : c.family.lexical.ExtendsTo c := - ⟨CatFamily.family_lexical _, by simp⟩ +theorem lexical_extendsTo (c : Cat) : c.family.lexical.ExtendsTo c := by + cases c <;> decide +kernel + +/-- Tense, aspect, modality, mood, the evidential, negation and polarity are mutually level. -/ +theorem antisymmRel_T : ∀ c ∈ [Cat.Asp, .Mod, .Mood, .Evid, .Neg, .Pol], + AntisymmRel ExtendsTo c .T := by + decide +kernel + +/-- Topic and focus are level, since Rizzi's topics recur on both sides of the focus. -/ +theorem antisymmRel_Top_Foc : AntisymmRel ExtendsTo .Top .Foc := by decide +kernel + +/-- The complementizer, Force and the speech-act head are one level. -/ +theorem antisymmRel_Force : ∀ c ∈ [Cat.C, .SA], AntisymmRel ExtendsTo c .Force := by decide +kernel + +/-- The verbal spine rises strictly from the verb through v, Voice, tense, finiteness and focus to +Force, and the nominal spine from the noun through the dividing and counting heads and D to K. -/ +theorem isChain_asymmRel : + [Cat.V, .v, .Voice, .T, .Fin, .Foc, .Force].IsChain (AsymmRel ExtendsTo) ∧ + [Cat.N, .Q, .Num, .D, .K].IsChain (AsymmRel ExtendsTo) := by + decide +kernel + +/-- Keine's nominalized clause and the CP are incomparable. -/ +theorem not_extendsTo_Nmlz_C : ¬ ExtendsTo .Nmlz .C ∧ ¬ ExtendsTo .C .Nmlz := by decide +kernel -/-- Any two categories of one family are comparable. -/ -theorem Cat.extendsTo_total {c d : Cat} (h : c.family = d.family) : - c.ExtendsTo d ∨ d.ExtendsTo c := - (le_total c.fValue d.fValue).imp (⟨h, ·⟩) (⟨h.symm, ·⟩) +end Cat end Minimalist diff --git a/Studies/Borer2005.lean b/Studies/Borer2005.lean index 1a584f4ff3..4870d3f0aa 100644 --- a/Studies/Borer2005.lean +++ b/Studies/Borer2005.lean @@ -241,6 +241,6 @@ theorem status_truncations : status [.N, .n] = some .stuff ∧ status [.N, .n, .Q] = some .divided := by decide -theorem fValue_Q_lt_Num : Cat.fValue .Q < Cat.fValue .Num := by decide +theorem asymmRel_Q_Num : AsymmRel Cat.ExtendsTo .Q .Num := by decide +kernel end Borer2005 diff --git a/Studies/Egressy2026.lean b/Studies/Egressy2026.lean index aa093b5e72..ffca4e256b 100644 --- a/Studies/Egressy2026.lean +++ b/Studies/Egressy2026.lean @@ -30,7 +30,7 @@ size-insensitive Sequence of Tense of English in its CP complements sitting insi ## Implementation notes -* Clause size is `Minimalist.ComplementSize` on the shared functional sequence `Cat.fValue`, where +* Clause size is `Minimalist.ComplementSize` in the extension order of `Minimalist.Cat`, where `Cat.Say` sits at Say > Foc > T. The Williams Cycle (26) and its version for Agree (35) are one relation, `WilliamsCycle x y`, between the head of a dependency and the crossed projection. * Readings are positions of the embedded reference time against the attitude's now, an @@ -90,34 +90,35 @@ def ClauseType.size : ClauseType → ComplementSize -- §3.1 theorem size_nonSpeech_lt_speech : - ClauseType.nonSpeechReporting.size.fLevel < ClauseType.speechReporting.size.fLevel := by - decide + ClauseType.nonSpeechReporting.size < ClauseType.speechReporting.size := by + decide +kernel /-! ### The Williams Cycle (26) and the Williams Cycle in Agree (35) -/ /-- A dependency headed at `x`, movement to Spec,XP or Agree from X or XP, may cross or search a projection of `y` unless Y is above X in the functional sequence. -/ -def WilliamsCycle (x y : Cat) : Prop := y.fValue ≤ x.fValue +def WilliamsCycle (x y : Cat) : Prop := ¬ AsymmRel Cat.ExtendsTo x y -instance (x y : Cat) : Decidable (WilliamsCycle x y) := inferInstanceAs (Decidable (_ ≤ _)) +instance (x y : Cat) : Decidable (WilliamsCycle x y) := + inferInstanceAs (Decidable (¬ (x.ExtendsTo y ∧ ¬ y.ExtendsTo x))) -theorem WilliamsCycle.refl (x : Cat) : WilliamsCycle x x := le_rfl +theorem WilliamsCycle.refl (x : Cat) : WilliamsCycle x x := fun h ↦ h.2 h.1 -theorem WilliamsCycle.of_le {x y y' : Cat} (h : y'.fValue ≤ y.fValue) (hxy : WilliamsCycle x y) : - WilliamsCycle x y' := - h.trans hxy +theorem WilliamsCycle.of_extendsTo {x y y' : Cat} (h : y'.ExtendsTo y) + (hxy : WilliamsCycle x y) : WilliamsCycle x y' := + fun hxy' ↦ hxy (hxy'.trans_le h) -- (24), (25) [egressy-2025] -theorem focus_crosses_TP : WilliamsCycle .Foc .T := by decide +theorem focus_crosses_TP : WilliamsCycle .Foc .T := by decide +kernel -- (24), (25) -theorem focus_blocked_by_SayP : ¬ WilliamsCycle .Foc .Say := by decide +theorem focus_blocked_by_SayP : ¬ WilliamsCycle .Foc .Say := by decide +kernel -- (27) theorem raising_crosses_TP : WilliamsCycle .T .T := WilliamsCycle.refl _ -- (28) -theorem raising_blocked_by_CP : ¬ WilliamsCycle .T .C := by decide +theorem raising_blocked_by_CP : ¬ WilliamsCycle .T .C := by decide +kernel /-- The complement size crossed in a raising row. -/ def crossed? (e : Datum) : Option ComplementSize := @@ -125,11 +126,11 @@ def crossed? (e : Datum) : Option ComplementSize := theorem raising_rows : ∀ e ∈ [ex_27, ex_28], ∀ cs ∈ crossed? e, e.judgment = .acceptable ↔ WilliamsCycle .T cs.highestHead := by - decide + decide +kernel /-- (23): evaluative adverbs such as *sajnos* sit in the Say layer above foci, so a clause hosts one iff it is at least a SayP. -/ -def HostsEvaluativeAdverb (cs : ComplementSize) : Prop := Cat.fValue .Say ≤ cs.fLevel +def HostsEvaluativeAdverb (cs : ComplementSize) : Prop := ⟨.Say⟩ ≤ cs instance (cs : ComplementSize) : Decidable (HostsEvaluativeAdverb cs) := inferInstanceAs (Decidable (_ ≤ _)) @@ -137,7 +138,7 @@ instance (cs : ComplementSize) : Decidable (HostsEvaluativeAdverb cs) := -- (23) theorem hostsEvaluativeAdverb_iff (ct : ClauseType) : HostsEvaluativeAdverb ct.size ↔ ct = .speechReporting := by - cases ct <;> decide + cases ct <;> decide +kernel /-! ### The Sequence of Tense Rule (31) and size-dependent adjunction (41) -/ @@ -149,17 +150,18 @@ inductive Attachment | vpInternal deriving DecidableEq -/-- The functional-sequence level of the matrix projection an embedded clause attaches to. -/ -def Attachment.level : Attachment → ComplementSize → ℕ - | .sizeDependent, cs => cs.fLevel - | .vpInternal, _ => Cat.fValue .V +/-- The head of the matrix projection an embedded clause attaches to. -/ +def Attachment.level : Attachment → ComplementSize → Cat + | .sizeDependent, cs => cs.highestHead + | .vpInternal, _ => .V /-- The Sequence of Tense Rule (31) can delete an embedded PAST iff the embedded T is contained in a projection of the matrix PAST T, that is, iff the clause attaches no higher than TP. -/ -def SOTRule.Applicable (a : Attachment) (cs : ComplementSize) : Prop := a.level cs ≤ Cat.fValue .T +def SOTRule.Applicable (a : Attachment) (cs : ComplementSize) : Prop := + WilliamsCycle .T (a.level cs) instance (a : Attachment) (cs : ComplementSize) : Decidable (SOTRule.Applicable a cs) := - inferInstanceAs (Decidable (_ ≤ _)) + inferInstanceAs (Decidable (WilliamsCycle _ _)) -- §3.3, §4 theorem applicable_sizeDependent_iff (cs : ComplementSize) : @@ -169,7 +171,7 @@ theorem applicable_sizeDependent_iff (cs : ComplementSize) : -- §4 theorem applicable_vpInternal_cP : SOTRule.Applicable .vpInternal .cP ∧ ¬ WilliamsCycle .T .C := by - decide + decide +kernel /-! ### Readings: the language-wide parameter realized clause-internally (§1, §2.4) -/ @@ -180,17 +182,17 @@ def readings (a : Attachment) (cs : ComplementSize) : Finset Ordering := theorem applicable_nonSpeech : SOTRule.Applicable .sizeDependent ClauseType.nonSpeechReporting.size := by - decide + decide +kernel theorem not_applicable_speech : ¬ SOTRule.Applicable .sizeDependent ClauseType.speechReporting.size := by - decide + decide +kernel -- §2.4 theorem simultaneous_iff (ct : ClauseType) : .eq ∈ readings .sizeDependent ct.size ↔ ct = .nonSpeechReporting := by - cases ct <;> decide + cases ct <;> decide +kernel theorem shifted_mem (a : Attachment) (cs : ComplementSize) : .lt ∈ readings a cs := @@ -199,7 +201,7 @@ theorem shifted_mem (a : Attachment) (cs : ComplementSize) : -- (19) theorem english_simultaneous : .eq ∈ readings .vpInternal .cP := by - decide + decide +kernel /-! ### Direct perception (§2.1) -/ @@ -255,7 +257,7 @@ def singleRows : List Datum := theorem singleRows_predicted : ∀ e ∈ singleRows, ∀ ct : ClauseType, clauseType? e = some ct → Agrees e "" (predicted e ct) := by - decide + decide +kernel /-- The matrix word of a row with its verb: among the words before the first complementizer glossed *that*, the past-tense one whose stem is a stem the fragment declares, so *álmod-t-a* @@ -356,13 +358,13 @@ def chain (ct₁ ct₂ : ClauseType) : List Clause := [⟨⟦past⟧, ct₁.size theorem ex16_profile : profile .sizeDependent ⟦past⟧ (chain .speechReporting .nonSpeechReporting) = [⟦past⟧, ⟦past⟧ ⊔ ⟦present⟧] := by - decide + decide +kernel -- (17), (16) theorem ex17_profile : profile .sizeDependent ⟦past⟧ (chain .nonSpeechReporting .speechReporting) = [⟦past⟧ ⊔ ⟦present⟧, ⟦past⟧] := by - decide + decide +kernel -- (10), (15), (16), (17) theorem doubleRows_predicted : ∀ e ∈ [ex_10, ex_15, ex_16, ex_17], ∀ ct₁ ct₂ : ClauseType, @@ -372,7 +374,7 @@ theorem doubleRows_predicted : ∀ e ∈ [ex_10, ex_15, ex_16, ex_17], ∀ ct₁ ((profile .sizeDependent ⟦past⟧ (chain ct₁ ct₂)).getD 0 ⊥)) ∧ Agrees e "deepest " (observed (DirectPerceptionAt e "deepestDirectPerception") ((profile .sizeDependent ⟦past⟧ (chain ct₁ ct₂)).getD 1 ⊥)) := by - decide + decide +kernel -- (18) [ogihara-1996] theorem ex18_profile : @@ -383,7 +385,7 @@ theorem ex18_predicted : Agrees ex_18 "deepest " ⟦past⟧ := by decide /-! ### Rival mechanisms (§3.3, §4) -/ -theorem resMovement_blocked_by_TP : ¬ WilliamsCycle .V .T := by decide +theorem resMovement_blocked_by_TP : ¬ WilliamsCycle .V .T := by decide +kernel /-- Sequence of Tense as a probe of [keine-2020]: a probe on T whose horizon is Say. -/ def sotProbe : Probe.Profile := ⟨.T, some .Say⟩ @@ -396,7 +398,7 @@ theorem sotProbe_clauseTypes : -- §4, footnote 9 theorem horizon_admits_FocP : sotProbe.TransparentTo (ClauseSpine.tP.append [.Foc]).label ∧ ¬ WilliamsCycle .T .Foc := by - decide + decide +kernel /-! ### Recognition by witness diff --git a/Studies/FuscoSgrizzi2026.lean b/Studies/FuscoSgrizzi2026.lean index bf7cbf3c65..c29ef8f593 100644 --- a/Studies/FuscoSgrizzi2026.lean +++ b/Studies/FuscoSgrizzi2026.lean @@ -29,14 +29,14 @@ circumstantial base ordered by inertia ([dowty-1979], [kratzer-2013]). This is t self-referentiality of intention ([searle-1983]): in every inertia world the intended event is caused by the attitude state, hence later than it, the future orientation of *a*-infinitives ([wurmbrand-2014]; `intention_future`). Complement size is the extended projection's -`ComplementSize`, ordered by functional level; the reading is read off the CP threshold, and the -diagnostics of sections 3 and 3.1 are predicted by the heads the complement reaches -(`rows_predicted`). +`ComplementSize`, ordered by the extension order of its highest head; the reading is read off the +CP threshold, and the diagnostics of sections 3 and 3.1 are predicted by the heads the complement +reaches (`rows_predicted`). ## Implementation notes * The *a*-infinitive is recorded with negation as its highest head, the highest the paper places - inside it. The functional sequence does not separate negation from tense and modal heads, so + inside it. The extension order makes negation level with tense and the modal heads, so the absence of modal auxiliaries ((9) and (10)) and the ban on past-oriented complements ((5)) stay in the prose and in `intention_future`. * The two heads are stated over abstract eventualities and worlds, with the content background, @@ -164,7 +164,7 @@ def readings (v : Italian.Verb) : List Reading := -- (4) theorem convincere_pensare_readings : readings convincere = [.belief, .intention] ∧ readings pensare = [.belief, .intention] := by - decide + decide +kernel /-! ### The diagnostics of sections 3 and 3.1 -/ @@ -220,6 +220,6 @@ def Row.ofDatum (ex : Datum) : Option Row := do def rows : List Row := Examples.all.filterMap Row.ofDatum theorem rows_predicted : ∀ r ∈ rows, (r.grammatical = true ↔ r.diagnostic.Predicted r.size) := by - decide + decide +kernel end FuscoSgrizzi2026 diff --git a/Studies/LiuYip2026.lean b/Studies/LiuYip2026.lean index dfce135aaa..8bb7cb581b 100644 --- a/Studies/LiuYip2026.lean +++ b/Studies/LiuYip2026.lean @@ -42,8 +42,8 @@ embeddability of *you* (`Pred.embedsYou`) and into the blocking of aspect loweri ## Main definitions -* `AspProjection`, `AspProjection.level` — the outer and inner aspect projections of the split - aspect approach and their heights in the functional sequence. +* `AspProjection`, `AspProjection.head` — the outer and inner aspect projections of the split + aspect approach and their heads. * `Contains`, `ExceptionalScope` — a complement size contains an aspect projection, and an element associated with it takes exceptional scope across it. * `Again`, `Again.projection`, `Again.NeedsDynamic` — the six *again*-elements, the projection each @@ -56,12 +56,11 @@ embeddability of *you* (`Pred.embedsYou`) and into the blocking of aspect loweri ## Implementation notes -The two projections are the binary split of Travis, MacDonald, Tsai and Sybesma; their -heights are those of `Cat.Asp` and `Cat.InnerAsp` in the functional sequence, outer aspect at -the level of T and inner aspect at the level of v, so containment is a -comparison of levels. Chomsky's defective intervention is not a -relation between heads: an embedded projection blocks association whatever its features, which -is the paper's claim. The semicomplementizer and Exfoliation, the restitutive reading, the +The two projections are the binary split of Travis, MacDonald, Tsai and Sybesma; their heads +are `Cat.Asp` and `Cat.InnerAsp`, outer aspect level with T and inner aspect below v as (1a) draws +it, so containment is the extension order of `Minimalist.Cat`. Chomsky's defective intervention +is not a relation between heads: an embedded projection blocks association whatever its features, +which is the paper's claim. The semicomplementizer and Exfoliation, the restitutive reading, the Italian parallel and the crosstype ambiguity of *dasuan* 'plan' are not represented. ## References @@ -91,10 +90,10 @@ inductive AspProjection where | inner deriving DecidableEq, Repr -/-- The height of a projection in the functional sequence, that of outer and of inner aspect. -/ -def AspProjection.level : AspProjection → ℕ - | .outer => Cat.fValue .Asp - | .inner => Cat.fValue .InnerAsp +/-- The head of a projection, outer or inner aspect. -/ +def AspProjection.head : AspProjection → Cat + | .outer => .Asp + | .inner => .InnerAsp /-- Type I, the finite CP. -/ def typeI : ComplementSize := .cP @@ -105,17 +104,19 @@ def typeII : ComplementSize := .tP /-- Type III, the nonfinite vP with aspect restructuring. -/ def typeIII : ComplementSize := .vP -/-- A complement of size `s` contains the aspect projection `f` when it reaches the -projection's height, the level of T for the outer one and the level of v for the inner one. -/ -def Contains (s : ComplementSize) (f : AspProjection) : Prop := f.level ≤ s.fLevel +/-- A complement of size `s` contains the aspect projection `f` when it reaches the projection's +head, outer aspect at the level of T and inner aspect below v. -/ +def Contains (s : ComplementSize) (f : AspProjection) : Prop := ⟨f.head⟩ ≤ s instance (s : ComplementSize) (f : AspProjection) : Decidable (Contains s f) := inferInstanceAs (Decidable (_ ≤ _)) -theorem contains_inner {s : ComplementSize} (h : ComplementSize.vP ≤ s) : Contains s .inner := h +theorem contains_inner {s : ComplementSize} (h : ComplementSize.vP ≤ s) : Contains s .inner := + le_trans (show (⟨.InnerAsp⟩ : ComplementSize) ≤ .vP by decide +kernel) h theorem contains_outer_iff (s : ComplementSize) : Contains s .outer ↔ ComplementSize.tP ≤ s := - Iff.rfl + ⟨le_trans (show ComplementSize.tP ≤ ⟨.Asp⟩ by decide +kernel), + le_trans (show (⟨.Asp⟩ : ComplementSize) ≤ .tP by decide +kernel)⟩ /-- An element associated with the projection `f` takes exceptional scope across a complement of size `s`, skipping the matrix predicate or lowering onto it, when the complement @@ -131,11 +132,13 @@ hierarchy, so what crosses a larger complement crosses a smaller one. -/ theorem antitone_exceptionalScope (f : AspProjection) : Antitone (ExceptionalScope f) := fun _ _ h hs hc ↦ hs (hc.trans h) -/-- Outer-associated elements take exceptional scope across a complement smaller than a TP, -the vP, and across nothing larger. -/ -theorem exceptionalScope_outer_iff (s : ComplementSize) : - ExceptionalScope .outer s ↔ s < ComplementSize.tP := - Nat.not_le +/-- Outer-associated elements take exceptional scope across a verbal complement smaller than a +TP, the vP, and across nothing larger. -/ +theorem exceptionalScope_outer_iff {s : ComplementSize} (hs : s.highestHead.family = .verbal) : + ExceptionalScope .outer s ↔ s < ComplementSize.tP := by + rw [ExceptionalScope, contains_outer_iff, lt_iff_le_not_ge, iff_and_self] + obtain ⟨c⟩ := s + cases c <;> first | exact absurd hs (by decide) | decide +kernel /-- Inner-associated elements never take exceptional scope, since every complement contains inner aspect, so vP is the minimal size of a nonfinite clause. -/ @@ -148,7 +151,7 @@ a finite CP. -/ theorem generalization_II : ExceptionalScope .outer typeIII ∧ ¬ ExceptionalScope .outer typeII ∧ ¬ ExceptionalScope .outer typeI := by - decide + decide +kernel /-- The sizes a clausal complement of the frame can have, a CP (Type I) for a finite clause and a TP (Type II) or a vP (Type III) for a nonfinite one. -/ @@ -159,12 +162,12 @@ theorem vP_le_of_mem_sizes {fr : ArgumentFrame} {s : ComplementSize} (h : s ∈ ComplementSize.vP ≤ s := by unfold sizes at h split_ifs at h <;> simp only [Finset.mem_singleton, Finset.mem_insert, - Finset.notMem_empty] at h <;> rcases h with rfl | rfl <;> decide + Finset.notMem_empty] at h <;> rcases h with rfl | rfl <;> decide +kernel theorem exists_mem_sizes_exceptionalScope_outer_iff (fr : ArgumentFrame) : (∃ s ∈ sizes fr, ExceptionalScope .outer s) ↔ fr.HasClausal ∧ ¬ fr.HasFinite := by unfold sizes - split_ifs <;> simp_all <;> decide + split_ifs <;> simp_all <;> decide +kernel /-! ### The *again*-elements and their projections -/ @@ -210,27 +213,29 @@ def Again.Skips (a : Again) : Prop := instance : DecidablePred Again.Skips := fun _ ↦ inferInstanceAs (Decidable (∃ _ ∈ _, _)) -theorem skips_iff (a : Again) : a.Skips ↔ a.projection = some .outer := by cases a <;> decide +theorem skips_iff (a : Again) : a.Skips ↔ a.projection = some .outer := by + cases a <;> decide +kernel /-- Generalization I says that exceptional scope is found with *you* but not with *zai*. -/ -theorem generalization_I : Again.you.Skips ∧ ¬ Again.zai.Skips := by decide +theorem generalization_I : Again.you.Skips ∧ ¬ Again.zai.Skips := by decide +kernel /-- In Cantonese *-faan* lowers, repetitive *-gwo* does not, and neither preverbal adverb has exceptional scope. -/ theorem cantonese_lowering : Again.faan.Skips ∧ ¬ Again.gwo.Skips ∧ ¬ Again.jau.Skips ∧ ¬ Again.zoi.Skips := by - decide + decide +kernel /-- Correlation I says that a Mandarin *again*-element has exceptional scope iff it cannot surface in an embedded nonfinite clause without a dynamic aspect, that is, iff it carries `[u+D]`. -/ -theorem correlation_I : ∀ a ∈ [Again.you, Again.zai], (a.Skips ↔ a.NeedsDynamic) := by decide +theorem correlation_I : ∀ a ∈ [Again.you, Again.zai], (a.Skips ↔ a.NeedsDynamic) := by + decide +kernel /-- Correlation II says that an *again*-element has exceptional scope iff its projection is at -least as high as the aspectual heads, the level of `Asp` in the functional sequence. -/ +least as high as the aspectual heads, so that its head extends outer aspect. -/ theorem correlation_II (a : Again) : - a.Skips ↔ ∃ f ∈ a.projection, Cat.fValue .Asp ≤ f.level := by - cases a <;> decide + a.Skips ↔ ∃ f ∈ a.projection, Cat.Asp.ExtendsTo f.head := by + cases a <;> decide +kernel /-! ### Aspect suffixes and phase complements -/ @@ -250,7 +255,7 @@ predicate, and the continuous *-zyu* alone is not. -/ theorem aspect_lowering : ∀ m ∈ Cantonese.Aspect.markers, (ExceptionalScope (aspectProjection m) typeIII ↔ m ≠ Cantonese.Aspect.zyu) := by - decide + decide +kernel /-- No phase complement lowers across any complement. -/ theorem no_phaseComplement_lowering (pc : Cantonese.ResultativeComplements.PhaseComplement) @@ -284,7 +289,7 @@ instance : DecidablePred Complement.LicensesDynamic := fun _ ↦ inferInstanceAs exceptional scope across it, and an embedded *you* blocks aspect lowering. -/ theorem not_exceptionalScope_of_licensesDynamic {c : Complement} (h : c.LicensesDynamic) : ¬ ExceptionalScope .outer c.size := by - rcases h with rfl | rfl <;> decide + rcases h with rfl | rfl <;> decide +kernel /-- The three Mandarin predicates of the selectional table. -/ inductive Pred where @@ -322,7 +327,7 @@ instance : DecidablePred Pred.SkipsYou := fun _ ↦ inferInstanceAs (Decidable ( theorem embedsYou : (¬ Pred.xiang.EmbedsYou ∧ Pred.xiang.SkipsYou) ∧ (Pred.rang.EmbedsYou ∧ Pred.rang.SkipsYou) ∧ (Pred.xiangxin.EmbedsYou ∧ ¬ Pred.xiangxin.SkipsYou) := by - decide + decide +kernel theorem Pred.size_mem_sizes (p : Pred) : ∀ c ∈ p.selects, ∃ fr ∈ p.entry.valency.frames, c.size ∈ sizes fr := by @@ -360,7 +365,7 @@ theorem not_gwo_crossesComplement (v : Verb) : ¬ Again.gwo.CrossesComplement v theorem faan_ambiguous {fr : ArgumentFrame} (hc : fr.HasClausal) (hf : ¬ fr.HasFinite) : (∃ s ∈ sizes fr, Contains s .outer) ∧ ∃ s ∈ sizes fr, ExceptionalScope .outer s := by simp only [sizes, hf, hc, ↓reduceIte] - decide + decide +kernel open Cantonese.Verbs in /-- An embedded *-faan* scopes over the nonfinite-complement verbs of (79) and not over the @@ -368,7 +373,7 @@ finite-complement verbs of (80). -/ theorem faan_lowering : (∀ v ∈ [soeng, hyun, bik, giu, daasyun], Again.faan.CrossesComplement v) ∧ ∀ v ∈ [seon, gong, geidak], ¬ Again.faan.CrossesComplement v := by - decide + decide +kernel /-! ### The implicational complementation hierarchy -/ @@ -379,7 +384,7 @@ def minimalSize : Clause.Size → ComplementSize | .situation => .tP | .proposition => .cP -theorem monotone_minimalSize : Monotone minimalSize := by decide +theorem monotone_minimalSize : Monotone minimalSize := by decide +kernel theorem exceptionalScope_of_le {f : AspProjection} {c c' : Clause.Size} (h : c ≤ c') (hs : ExceptionalScope f (minimalSize c')) : ExceptionalScope f (minimalSize c) := diff --git a/Studies/Major2024.lean b/Studies/Major2024.lean index f07c83b6e9..615ad299ce 100644 --- a/Studies/Major2024.lean +++ b/Studies/Major2024.lean @@ -115,14 +115,15 @@ theorem washo_parallel : /-! ### Two heights -/ theorem adjoined_below : - ∀ h ∈ [Cat.v, .Asp, .Neg, .T], Cat.V.fValue < h.fValue ∧ ¬ Cat.T.fValue < h.fValue := by - decide + ∀ h ∈ [Cat.v, .Asp, .Neg, .T], + AsymmRel Cat.ExtendsTo .V h ∧ ¬ AsymmRel Cat.ExtendsTo .T h := by + decide +kernel theorem height_diagnostics : ∀ r ∈ Examples.all, ∀ s ∈ r.parse? "height" [("VP", Cat.V), ("TP", .T)], ∃ h ∈ r.parse? "diagnostic" [("nci", Cat.Neg), ("proform", .v)], - (r.judgment = .acceptable ↔ s.fValue < h.fValue) := by - decide + (r.judgment = .acceptable ↔ AsymmRel Cat.ExtendsTo s h) := by + decide +kernel /-! ### Accusative from `v` -/ diff --git a/Studies/Panagiotidis2015.lean b/Studies/Panagiotidis2015.lean index 8d4c85e33b..f998b6dc1f 100644 --- a/Studies/Panagiotidis2015.lean +++ b/Studies/Panagiotidis2015.lean @@ -91,8 +91,9 @@ theorem chomsky_panagiotidis_agree (c₁ c₂ : Cat) : categorialFeatures c₁ = categorialFeatures c₂ ↔ c₁.features = c₂.features := by rw [categorialFeatures_eq_iff, Cat.features_eq_iff] -theorem fValue_of_isCategorizer {c : Cat} (h : IsCategorizer c) : c.fValue = 1 := by - cases c <;> first | rfl | exact h.elim +/-- A categorizer merges directly with the root, the lexical head of its family. -/ +theorem step_of_isCategorizer {c : Cat} (h : IsCategorizer c) : c.family.lexical.Step c := by + cases c <;> first | decide +kernel | exact h.elim /-- A category-neutral root with the surface words it projects across the lexical categories, each stamped with its Universal Dependencies category ([marantz-1997]). -/ diff --git a/references.bib b/references.bib index 0a9ed27f09..ffc8170bc6 100644 --- a/references.bib +++ b/references.bib @@ -2201,7 +2201,7 @@ @incollection{speas-tenny-2003 subfield = {syntax}, role = {formalized}, validated = {true}, - sources = {Semantics/Mood/SpeechEvent.lean;Studies/Dayal2025.lean;Studies/SpeasTenny2003.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean} + sources = {Semantics/Mood/SpeechEvent.lean;Studies/Dayal2025.lean;Studies/SpeasTenny2003.lean;Syntax/Cartography.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean} } @article{speas-2004, author = {Speas, Margaret}, @@ -13443,7 +13443,7 @@ @article{egressy-2026 subfield = {semantics/tense}, validated = {true}, role = {formalized}, - sources = {Data/Examples/Egressy2026.json;Fragments/Hungarian/Verbs.lean;Studies/Egressy2026.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category.lean} + sources = {Data/Examples/Egressy2026.json;Fragments/Hungarian/Verbs.lean;Studies/Egressy2026.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/Probe/Profile.lean} } @incollection{sharvit-2020, author = {Sharvit, Yael}, @@ -22232,7 +22232,7 @@ @article{pollock-1989 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Data/Examples/ArregiPietraszko2021.json;Data/Examples/HarizanovGribanova2019.json;Fragments/Ga/Clause.lean;Studies/ArregiPietraszko2021.lean;Studies/Pollock1989.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Category.lean} + sources = {Data/Examples/ArregiPietraszko2021.json;Data/Examples/HarizanovGribanova2019.json;Fragments/Ga/Clause.lean;Studies/ArregiPietraszko2021.lean;Studies/Pollock1989.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean} } @book{henry-1995, author = {Henry, Alison}, @@ -23944,7 +23944,7 @@ @book{pylkkanen-2008 subfield = {syntax}, role = {cited}, validated = {true}, - sources = {Semantics/ArgumentStructure/Linking.lean;Studies/Bruening2001.lean;Studies/Bruening2021.lean;Studies/Hewett2026.lean;Studies/Pylkkanen2008.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Applicative.lean;Syntax/Minimalist/Verbal/LittleV.lean;Syntax/Minimalist/Verbal/Voice.lean;Syntax/Minimalist/Category.lean;Studies/Harley2017.lean} + sources = {Semantics/ArgumentStructure/Linking.lean;Studies/Bruening2001.lean;Studies/Bruening2021.lean;Studies/Harley2017.lean;Studies/Hewett2026.lean;Studies/Pylkkanen2008.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Verbal/Applicative.lean;Syntax/Minimalist/Verbal/LittleV.lean;Syntax/Minimalist/Verbal/Voice.lean} } @article{stiebels-2006, author = {Stiebels, Barbara}, @@ -24978,7 +24978,7 @@ @book{keine-2020 subfield = {syntax}, role = {formalized}, validated = {true}, - sources = {Studies/Egressy2026.lean;Studies/Keine2019.lean;Studies/Keine2020.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/ClauseSpine.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Probe/Profile.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/Locality/Horizon.lean} + sources = {Studies/Egressy2026.lean;Studies/Keine2019.lean;Studies/Keine2020.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/ClauseSpine.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Locality/Horizon.lean;Syntax/Minimalist/Probe/Profile.lean} } @article{keine-2019, author = {Keine, Stefan}, @@ -26670,7 +26670,7 @@ @article{cinque-2005 subfield = {syntax}, role = {formalized}, validated = {true}, - sources = {Studies/Cinque2005.lean;Studies/Cinque2020.lean;Studies/StanojevicSteedman2021.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/Linearization/Replay.lean} + sources = {Studies/Cinque2005.lean;Studies/Cinque2020.lean;Studies/StanojevicSteedman2021.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/Linearization/Replay.lean} } @book{cinque-2020, author = {Cinque, Guglielmo}, @@ -27926,7 +27926,7 @@ @book{cinque-1999 role = {formalized}, doi = {10.1093/oso/9780195115260.001.0001}, validated = {true}, - sources = {Fragments/Romance/Italian/PolarityItems.lean;Studies/Cinque1999.lean;Studies/Erlewine2016.lean;Studies/Hacquard2010.lean;Studies/HoleFraser2026.lean;Studies/Narrog2012.lean;Studies/RamchandSvenonius2014.lean;Studies/SpeasTenny2003.lean;Syntax/Cartography.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean} + sources = {Fragments/Romance/Italian/PolarityItems.lean;Studies/Cinque1999.lean;Studies/Erlewine2016.lean;Studies/Hacquard2010.lean;Studies/HoleFraser2026.lean;Studies/Narrog2012.lean;Studies/RamchandSvenonius2014.lean;Studies/SpeasTenny2003.lean;Syntax/Cartography.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean} } @incollection{keefe-smith-1997, author = {Keefe, Rosanna and Smith, Peter}, @@ -28022,7 +28022,7 @@ @incollection{rizzi-1997 subfield = {syntax/minimalism}, validated = {true}, role = {cited}, - sources = {Studies/Allotey2021.lean;Studies/Erlewine2016.lean;Studies/Fortuny2024.lean;Studies/FuscoSgrizzi2026.lean;Studies/Greco2020.lean;Studies/Holmberg2016.lean;Studies/SpeasTenny2003.lean;Studies/Westergaard2009.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Feature/Basic.lean;Syntax/Minimalist/Category.lean} + sources = {Studies/Allotey2021.lean;Studies/Erlewine2016.lean;Studies/Fortuny2024.lean;Studies/FuscoSgrizzi2026.lean;Studies/Greco2020.lean;Studies/Holmberg2016.lean;Studies/SpeasTenny2003.lean;Studies/Westergaard2009.lean;Syntax/Minimalist/Category.lean;Syntax/Minimalist/ExtendedProjection.lean;Syntax/Minimalist/ExtendedProjection/Basic.lean;Syntax/Minimalist/ExtendedProjection/Properties.lean;Syntax/Minimalist/Feature/Basic.lean} } @inproceedings{zeijlstra-2007, @@ -28203,7 +28203,7 @@ @phdthesis{laka-1990 subfield = {syntax/minimalism}, validated = {true}, role = {cited}, - sources = {Studies/Wilder2013.lean} + sources = {Studies/Wilder2013.lean;Syntax/Minimalist/ExtendedProjection.lean} } @article{weicker-schulz-2024, author = {Weicker, Merle and Schulz, Petra}, @@ -30395,7 +30395,7 @@ @book{zanuttini-1997 doi = {10.1093/oso/9780195080544.001.0001}, subfield = {syntax/negation}, role = {cited}, - sources = {Fragments/Romance/Italian/Negation.lean} + sources = {Fragments/Romance/Italian/Negation.lean;Syntax/Minimalist/ExtendedProjection.lean} } @unpublished{marantz-2001, author = {Marantz, Alec}, @@ -35692,7 +35692,7 @@ @book{newman-2024 subfield = {syntax/minimalism}, role = {formalized}, validated = {true}, - sources = {Studies/Newman2024.lean} + sources = {Studies/Newman2024.lean;Syntax/Minimalist/ExtendedProjection.lean} } @inproceedings{paille-2020, author = {Paill{\'e}, Mathieu}, @@ -44340,7 +44340,7 @@ @article{liu-yip-2026 subfield = {syntax}, validated = {true}, role = {formalized}, - sources = {Fragments/Cantonese/Aspect.lean;Fragments/Cantonese/Verbs.lean;Fragments/Mandarin/Verbs.lean;Studies/LiuYip2026.lean} + sources = {Fragments/Cantonese/Aspect.lean;Fragments/Cantonese/Verbs.lean;Fragments/Mandarin/Verbs.lean;Studies/LiuYip2026.lean;Syntax/Minimalist/ExtendedProjection.lean} } @incollection{wurmbrand-lohninger-2023, @@ -48022,7 +48022,7 @@ @incollection{harley-2017 address = {Oxford}, subfield = {syntax/argument-structure}, role = {cited}, - sources = {Studies/Coon2019.lean;Studies/Harley2017.lean;Studies/ChengCheng2026.lean} + sources = {Studies/ChengCheng2026.lean;Studies/Coon2019.lean;Studies/Harley2017.lean;Syntax/Minimalist/ExtendedProjection.lean} } @phdthesis{key-2013, author = {Key, Gregory}, @@ -48290,7 +48290,7 @@ @article{harley-2013 doi = {10.1016/j.lingua.2012.09.010}, subfield = {syntax}, role = {cited}, - sources = {Studies/CoonMateoPedroPreminger2014.lean} + sources = {Studies/CoonMateoPedroPreminger2014.lean;Syntax/Minimalist/ExtendedProjection.lean} } @article{massam-2001, From 66781e0c998b410a1aa4411ee00c00c230ba5058 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 11:16:52 -0700 Subject: [PATCH 4/4] chore(Syntax/Minimalist): run CI on the derived extension order