From ee31dc0a5d424b2422864a9432aa22f24b944e54 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 10:36:08 -0700 Subject: [PATCH] refactor(Syntax/Minimalist): extension order read from cited structures --- 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,