diff --git a/Linglib.lean b/Linglib.lean index 833e6f2c4..964cd44dd 100644 --- a/Linglib.lean +++ b/Linglib.lean @@ -1080,6 +1080,7 @@ import Linglib.Fragments.Swedish.QuestionParticles import Linglib.Fragments.Mayan.Params import Linglib.Fragments.Mayan.Mam.VoiceSystem import Linglib.Fragments.Mayan.Mam.Agreement +import Linglib.Fragments.Mayan.Mam.Pronouns import Linglib.Fragments.Mayan.Mam.ExtractionMorphology import Linglib.Fragments.Kawapanan.Shawi.Basic import Linglib.Fragments.Mixtec.SMPM.Basic @@ -1220,7 +1221,6 @@ import Linglib.Studies.CoonMateoPedroPreminger2014 import Linglib.Studies.Imanishi2014 import Linglib.Studies.Imanishi2020 import Linglib.Studies.Bohnemeyer2004 -import Linglib.Studies.Scott2023Ergativity import Linglib.Phenomena.ArgumentStructure.DativeAlternation import Linglib.Phenomena.ArgumentStructure.Passive import Linglib.Phenomena.ArgumentStructure.Subcategorization @@ -1902,7 +1902,6 @@ import Linglib.Syntax.CCG.Basic import Linglib.Syntax.CCG.Combinators import Linglib.Syntax.CCG.Interface import Linglib.Studies.Cysouw2009 -import Linglib.Studies.Scott2023Agreement import Linglib.Phenomena.Agreement.DifferentialIndexing import Linglib.Studies.Aissen2003Agreement import Linglib.Studies.PrasertsonSmithCulbertson2026 diff --git a/Linglib/Fragments/Mayan/Mam/Agreement.lean b/Linglib/Fragments/Mayan/Mam/Agreement.lean index 654f7aee5..48d9f7df4 100644 --- a/Linglib/Fragments/Mayan/Mam/Agreement.lean +++ b/Linglib/Fragments/Mayan/Mam/Agreement.lean @@ -1,5 +1,6 @@ import Linglib.Features.Case import Linglib.Features.Prominence +import Linglib.Fragments.Mayan.Mam.Pronouns import Linglib.Fragments.Mayan.Params import Linglib.Syntax.Agreement.Paradigm import Linglib.Typology.Extraction @@ -178,7 +179,7 @@ instance : DecidablePred ArgPosition.IsPhiAgreed := fun p => by Non-first person pronouns are NOT reduced — their subj/poss forms are identical to their independent forms (Table 4.25, p. 200). Whether actual reduction occurs depends on person (see - `derivePronounForm`), but only agreed-with positions are eligible. -/ + `realizedPronoun`), but only agreed-with positions are eligible. -/ def ArgPosition.CanBeReduced (pos : ArgPosition) : Prop := pos.IsPhiAgreed @@ -236,142 +237,99 @@ example : Features.Case.IsValidInventory caseInventory := by decide -- § 6: Pronoun Internal Structure ([scott-2023], ch. 4) -- ============================================================================ -/-- Person features relevant for pronoun reduction. - - Scott decomposes person into binary features following - [harbour-2016] (Table 4.3-4.4): - - [±author]: distinguishes 1st from non-1st - - [±participant]: distinguishes local (1st/2nd) from 3rd - - [±singular]: number - - Agreement (Set A and Set B) copies only [±author] and [±singular] - (Tables 4.7-4.8). It does NOT copy [±participant]. - - The =i enclitic is the **disagreement enclitic** — it realizes - *disagreeing* values of [±author] and [±participant] (ex. 59, - adapting [noyer-1992] / [harbour-2016]): - - 1SG/1PL.EXCL: [+author, -participant] → disagree → =i - - 2SG/2PL: [-author, +participant] → disagree → =i - - 1PL.INCL: [+author, +participant] → agree → no =i - - 3SG/3PL: [-author, -participant] → agree → no =i -/ -inductive PersonFeature where - | person -- person category (1st/2nd/3rd) - | number -- number category (sg/pl) - | participant -- [±participant]: local (1st/2nd) vs non-local (3rd) +/-- φ-dimensions of the SJA Mam pronominal system ([scott-2023] Table 4.4, + adopting [harbour-2016]'s bivalent features): [±author], [±participant], + [±singular]. Per-cell *values* live in `Mam.ScottFeatures` + (`Fragments/Mayan/Mam/Pronouns.lean`, where the disagreement + distribution of the =i enclitic is verified); this enum names the + *dimensions*, for the redundancy calculus below. -/ +inductive PhiDimension where + | author + | participant + | singular deriving DecidableEq, Repr -/-- The pronominal base morpheme's features. -/ -def baseFeatures : List PersonFeature := [.person, .number] - -/-- The =i enclitic's feature: [participant]. -/ -def encliticFeature : PersonFeature := .participant - -/-- Features that agreement morphology copies (person and number only). -/ -def agreedFeatures : List PersonFeature := [.person, .number] - -/-- A feature is redundantly expressed by agreement iff agreement copies it. -/ -def isRedundant (f : PersonFeature) : Bool := - agreedFeatures.any (· == f) - -/-- A morpheme is deleted when ALL its features are redundantly expressed - by agreement. -/ -def allRedundant (feats : List PersonFeature) : Bool := - feats.all isRedundant - -/-- The pronominal base is deleted: [person, number] are both copied by - agreement, making the base fully redundant. -/ -theorem base_is_redundant : allRedundant baseFeatures = true := by native_decide - -/-- The =i enclitic survives: [participant] is NOT copied by agreement. -/ -theorem enclitic_survives : isRedundant encliticFeature = false := by native_decide - -/-- Pronoun realization after impoverishment ([scott-2023], §4.4.3). - - - `reduced`: 1st person agreed-with — impoverishment deletes - [±singular] in the context of [+author]^F, bleeding insertion of - pronominal base morphemes *qin*/*qo*. Only =i remains. - - `full`: unreduced — the full independent pronoun form. This - covers 2nd/3rd person subj/poss (which ARE identical to their - independent forms, Table 4.25), as well as all object pronouns - (which are not agreed-with and thus not eligible for reduction). -/ -inductive PronounForm where - | reduced -- 1st person agreed-with: base deleted, only =i remains - | full -- full independent pronoun (all other cases) - deriving DecidableEq, Repr - -/-- Is this person 1st (= [+author])? Only [+author] persons are - eligible for the impoverishment rule (84) that deletes [±singular] - and bleeds base morpheme insertion. -/ -def isFirstPerson : Features.Prominence.PersonLevel → Prop - | .first => True - | _ => False - -instance : DecidablePred isFirstPerson := fun p => by - cases p <;> unfold isFirstPerson <;> infer_instance - -/-- Derive pronoun form from agreement status and person. - - The impoverishment rule (ex. 84/94) targets [+author] features - that bear the F diacritic (indicating agreement has occurred): - `[+/−singular] → ∅ / [+author]^F` - - This deletes [±singular] from 1st person agreed-with pronouns, - bleeding insertion of *qin* ([+author,+singular]) and *qo* - ([+author,−singular]). Only =i remains. - - For 2nd/3rd person, the rule does not apply (they are [-author]), - so their subj/poss forms equal their independent forms (Table 4.25). - For unagreed-with positions (objects), there is no F diacritic, - so impoverishment does not apply regardless of person. -/ -def derivePronounForm (pos : ArgPosition) (person : Features.Prominence.PersonLevel) : - PronounForm := - if pos.IsPhiAgreed then - if isFirstPerson person then .reduced - else .full -- 2nd/3rd: subj/poss = independent form (no reduction) - else .full - -/-- 1st person agent: reduced (base deleted, only =i remains). -/ +/-- Dimensions referenced by Set A/Set B agreement vocabulary items: only + [±author] and [±singular] (Tables 4.7-4.8) — agreement never copies + [±participant]. -/ +def agreedDimensions : List PhiDimension := [.author, .singular] + +/-- Dimensions realized by the pronominal base morphemes *qin* + [+author,+sg] and *qo* [+author,−sg] (Table 4.10). -/ +def baseDimensions : List PhiDimension := [.author, .singular] + +/-- Dimensions whose disagreement the =i enclitic realizes + ([noyer-1992]; [scott-2023] §4.3.3): [±author] and [±participant]. -/ +def encliticDimensions : List PhiDimension := [.author, .participant] + +/-- A dimension is copied back to the probe by agreement. -/ +def PhiDimension.Copied (d : PhiDimension) : Prop := d ∈ agreedDimensions + +instance : DecidablePred PhiDimension.Copied := fun d => by + unfold PhiDimension.Copied; infer_instance + +/-- The pronominal base is fully redundant under agreement: every dimension + it realizes is copied — the configuration in which impoverishment bleeds + base insertion (§4.4). -/ +theorem base_is_redundant : ∀ d ∈ baseDimensions, d.Copied := by decide + +/-- The =i enclitic is not fully redundant: [±participant] is never copied + by agreement — so the enclitic survives reduction. -/ +theorem enclitic_survives : ¬ (∀ d ∈ encliticDimensions, d.Copied) := by decide + +/-- Pronoun realization by argument position ([scott-2023], her (3)/(8): + nominative alignment of reduction). φ-agreed positions (A, S — and + possessors) take the subject/possessor series; the unagreed object + position takes the independent series. The impoverishment rule + (ex. 84/94) `[±singular] → ∅ / [+author]^F` targets [+author] features + bearing the agreed-with diacritic F, bleeding insertion of the bases + *qin*/*qo* — so agreed-with first person surfaces as bare *=i* + (or ∅ for 1PL.INCL), while everything else keeps its independent + form. Realization is *selection among the API's `PersonalPronoun` + entries*, not a separate form classification. -/ +def realizedPronoun (pos : ArgPosition) (c : PronCell) : Option PersonalPronoun := + if pos.IsPhiAgreed then subjPoss c else independent c + +/-- 1SG agent: reduced to the bare disagreement enclitic (base bled by + impoverishment). -/ theorem first_A_reduced : - derivePronounForm .A .first = .reduced := rfl - -/-- 3rd person agent: full independent form (impoverishment does not - apply to [-author]). -/ -theorem third_A_full : - derivePronounForm .A .third = .full := rfl + realizedPronoun .A .firstSg = some iDisagr := by decide -/-- 2nd person agent: full independent form (=i IS the independent - 2SG pronoun, not a reduction). -/ -theorem second_A_full : - derivePronounForm .A .second = .full := rfl +/-- 1SG intransitive subject: likewise reduced (Set B agreement). -/ +theorem first_S_reduced : + realizedPronoun .S .firstSg = some iDisagr := by decide -/-- 1st person patient: full pronoun (no agreement → no F diacritic). -/ +/-- 1SG patient: the full independent pronoun *qini* (no agreement → no + F diacritic → no impoverishment). -/ theorem first_P_full : - derivePronounForm .P .first = .full := rfl + realizedPronoun .P .firstSg = some qini := by decide -/-- 3rd person patient: full pronoun (no agreement → no F diacritic). -/ -theorem third_P_full : - derivePronounForm .P .third = .full := rfl +/-- 2SG agent: unreduced — *=i* IS the independent 2SG form (Scott's + fn. 2), so the agreed-with cell coincides with the independent one. -/ +theorem second_A_unreduced : + realizedPronoun .A .secondSg = independent .secondSg := by decide -/-- 1st person intransitive S: reduced (Set B agreement triggers - impoverishment, deleting base). -/ -theorem first_S_reduced : - derivePronounForm .S .first = .reduced := rfl +/-- 3PL agent: full *qa* (impoverishment does not apply to [−author]). -/ +theorem third_A_full : + realizedPronoun .A .thirdPl = some qa := by decide -/-- 3rd person intransitive S: full independent form. -/ -theorem third_S_full : - derivePronounForm .S .third = .full := rfl +/-- The nominative-alignment contrast: the same 1SG argument is *=i* as + agent but *qini* as patient. -/ +theorem first_A_vs_P : + realizedPronoun .A .firstSg ≠ realizedPronoun .P .firstSg := by decide -/-- Key asymmetry: for agreed-with positions, 1st person is reduced - while 2nd/3rd retain full independent forms. This follows from the - impoverishment rule targeting [+author] only. -/ +/-- Agreed-with first person differs from agreed-with third person — the + impoverishment rule targets [+author] only. -/ theorem first_vs_nonfirst_asymmetry : - (derivePronounForm .A .first ≠ derivePronounForm .A .third) ∧ - (derivePronounForm .S .first ≠ derivePronounForm .S .third) := by + realizedPronoun .A .firstSg ≠ realizedPronoun .A .thirdSg ∧ + realizedPronoun .S .firstSg ≠ realizedPronoun .S .thirdSg := by exact ⟨by decide, by decide⟩ -/-- For unagreed-with positions, person is irrelevant: all get full pronouns. -/ -theorem patient_person_irrelevant : - derivePronounForm .P .first = derivePronounForm .P .third := rfl +/-- The unagreed object position realizes the independent series, for + every cell — person is irrelevant without the F diacritic. -/ +theorem patient_takes_independent (c : PronCell) : + realizedPronoun .P c = independent c := by + cases c <;> decide -- ============================================================================ -- § 7: Mayan Absolutive Parameter diff --git a/Linglib/Fragments/Mayan/Mam/Pronouns.lean b/Linglib/Fragments/Mayan/Mam/Pronouns.lean new file mode 100644 index 000000000..782aacadc --- /dev/null +++ b/Linglib/Fragments/Mayan/Mam/Pronouns.lean @@ -0,0 +1,213 @@ +import Linglib.Syntax.Pronoun.Basic + +/-! # San Juan Atitán Mam Pronouns + +Pronoun lexicon for San Juan Atitán Mam (SJA Mam, Mayan), from [scott-2023] +ch. 4. Scott's central claim is that the reduced subject/possessor forms are +**true pronouns** in argument position — not agreement markers (contra her own +Scott 2020 analysis) and not a special clitic series (she explicitly prefers an +impoverishment derivation over "positing a unique series of 'clitic' pronouns", +p. 162, citing the Agree-affects-pronouns family: Cardinaletti & Starke, Nevins, +Kramer, Stegovec, Yuan). The entries therefore live here as `PersonalPronoun` +values flowing through the shared Pronoun API. + +Two series (her Table 4.1 / 4.9, p. 160 / 185): + +* **Independent** ("most morphosyntactically rich", her fn. 2 — the 2SG + "independent" form is the enclitic *=i* itself): *qini* (= *qin+=i*), + *qoy* (= *qo'+=y*), *qo*, *=i*, *qi* (= *q+=i*), 3SG ∅, *qa*. +* **Subject/possessor** (reduced): first-person cells lose their base + morphemes (*qin* [+author,+sg], *qo* [+author,−sg], Table 4.10) via an + impoverishment rule conditioned on agreement (§4.4); 2nd/3rd cells are + identical to the independent series. + +The disagreement enclitic *=i* (gloss DISAGR; [noyer-1992], [harbour-2016]; +her §4.3.3) realizes *disagreeing* values of [±author]/[±participant] — +`enclitic_iff_disagrees` verifies the XOR distribution across the paradigm. +`reduction_iff_author` verifies that the two series differ exactly at +[+author] cells. + +Feature values follow her Table 4.4 (p. 183). NB the convention: +Harbour's [±participant] "functions more like a [+/−hearer] or +[+/−addressee] feature" (p. 182), so 1EXCL is [−participant] — this +deliberately diverges from `Features.Person.Features`, whose `wellFormed` +invariant (author → participant) encodes the speech-act-participant +convention; hence the fragment-local `ScottFeatures`. + +Wordhood: *=i* is a morphological enclitic with promiscuous attachment +(nouns, verbs, pronouns, other clitics; allomorphs /, =ni after [m]); +whether *qi*/*qa* are words or enclitics is left open by Scott (p. 163, her +p. 39) — none of this is a Cardinaletti–Starke deficiency classification, +so `strength` is left unset throughout. +-/ + +set_option autoImplicit false + +namespace Mam + +/-! ### Lexical entries -/ + +/-- *=i* — the disagreement enclitic pronoun (DISAGR): realizes disagreeing + [±author]/[±participant] values, hence φ-underspecified (it serves 1SG, + 1PL.EXCL, 2SG, and — with the plural piece *q* — 2PL; Table 4.11). + Doubles as the 2SG "independent" form (her fn. 2). -/ +def iDisagr : PersonalPronoun := + { form := "=i", person := none, number := none } + +/-- *qini* — 1SG independent pronoun; bimorphemic *qin+=i* (base *qin* + [+author,+sg] + disagreement enclitic, Table 4.9). -/ +def qini : PersonalPronoun := + { form := "qini", person := some .first, number := some .Sing } + +/-- *qoy* — 1PL exclusive independent pronoun; bimorphemic *qo'+=y* + (base *qo* [+author,−sg] + enclitic; glottalization from the enclitic, + her fn. 7). -/ +def qoy : PersonalPronoun := + { form := "qoy", person := some .first, number := some .Plur, + clusivity := some .exclusive } + +/-- *qo* — 1PL inclusive independent pronoun; monomorphemic (1INCL's + [+author,+participant] values *agree*, so no enclitic). -/ +def qo : PersonalPronoun := + { form := "qo", person := some .first, number := some .Plur, + clusivity := some .inclusive } + +/-- *qi* — 2PL pronoun, both series; bimorphemic *q+=i* (§4.3.3.2). + Word-vs-enclitic status left open by Scott (p. 163). -/ +def qi : PersonalPronoun := + { form := "qi", person := some .second, number := some .Plur } + +/-- *qa* — 3PL pronoun, both series; also the generic plural marker of the + language (her (42)–(44)). Word-vs-enclitic status left open. -/ +def qa : PersonalPronoun := + { form := "qa", person := some .third, number := some .Plur } + +/-- The clusivity-marked entries satisfy the API's well-formedness invariant + (clusivity only on 1st-person non-singular). -/ +theorem clusive_entries_wellFormed : + qoy.toPronoun.WellFormed ∧ qo.toPronoun.WellFormed := by + constructor <;> decide + +/-! ### The paradigm -/ + +/-- A cell of the SJA Mam pronominal paradigm: the quadripartition + (1EXCL/1INCL/2/3, Table 4.3) crossed with number, minus the principled + gap *1SG-inclusive (Table 4.4). -/ +inductive PronCell where + | firstSg | firstPlExcl | firstPlIncl + | secondSg | secondPl + | thirdSg | thirdPl + deriving DecidableEq, Repr + +/-- PronCell person, in the API's vocabulary. -/ +def PronCell.person : PronCell → Features.Person + | .firstSg | .firstPlExcl | .firstPlIncl => .first + | .secondSg | .secondPl => .second + | .thirdSg | .thirdPl => .third + +/-- PronCell number, in the API's vocabulary. -/ +def PronCell.number : PronCell → Features.Number + | .firstSg | .secondSg | .thirdSg => .Sing + | _ => .Plur + +/-- PronCell clusivity (1PL cells only), in the API's vocabulary. -/ +def PronCell.clusivity : PronCell → Option Features.Clusivity.Value + | .firstPlExcl => some .exclusive + | .firstPlIncl => some .inclusive + | _ => none + +/-- [scott-2023]'s bivalent φ-features (Table 4.4, after [harbour-2016]): + [±author], [±participant], [±singular]. Fragment-local because the + participant convention (≈ [±hearer]: 1EXCL is [−participant]) is + incompatible with `Features.Person.Features`' author → participant + invariant. -/ +structure ScottFeatures where + author : Bool + participant : Bool + singular : Bool + deriving DecidableEq, Repr + +/-- Feature values per cell — a transcription of Table 4.4. -/ +def PronCell.features : PronCell → ScottFeatures + | .firstSg => ⟨true, false, true⟩ + | .firstPlExcl => ⟨true, false, false⟩ + | .firstPlIncl => ⟨true, true, false⟩ + | .secondSg => ⟨false, true, true⟩ + | .secondPl => ⟨false, true, false⟩ + | .thirdSg => ⟨false, false, true⟩ + | .thirdPl => ⟨false, false, false⟩ + +/-- [±author]/[±participant] values disagree — the condition under which the + enclitic *=i* is inserted ([noyer-1992]; [scott-2023] §4.3.3). -/ +def PronCell.Disagrees (c : PronCell) : Prop := + c.features.author ≠ c.features.participant + +instance : DecidablePred PronCell.Disagrees := fun c => by + unfold PronCell.Disagrees; infer_instance + +/-- The feature table is faithful to the API-side person values: + [+author] exactly at first person. -/ +theorem author_iff_first (c : PronCell) : + c.features.author = true ↔ c.person = .first := by + cases c <;> simp [PronCell.features, PronCell.person] + +/-- The feature table is faithful to the API-side number values: + [+singular] exactly at singular cells. -/ +theorem singular_iff_sing (c : PronCell) : + c.features.singular = true ↔ c.number = .Sing := by + cases c <;> simp [PronCell.features, PronCell.number] + +/-- Independent pronoun by cell (Table 4.1 right column; 3SG has no overt + pronoun). -/ +def independent : PronCell → Option PersonalPronoun + | .firstSg => some qini + | .firstPlExcl => some qoy + | .firstPlIncl => some qo + | .secondSg => some iDisagr + | .secondPl => some qi + | .thirdSg => none + | .thirdPl => some qa + +/-- Subject/possessor (reduced) pronoun by cell (Table 4.1 left column): + first-person bases are bled by impoverishment (§4.4), so 1SG/1PL.EXCL + surface as bare *=i* and 1PL.INCL as ∅; 2nd/3rd are identical to the + independent series. -/ +def subjPoss : PronCell → Option PersonalPronoun + | .firstSg => some iDisagr + | .firstPlExcl => some iDisagr + | .firstPlIncl => none + | .secondSg => some iDisagr + | .secondPl => some qi + | .thirdSg => none + | .thirdPl => some qa + +/-- Morphological-parse data (Table 4.9): the form contains the disagreement + enclitic. *qini* = *qin+=i*, *qoy* = *qo'+=y*, *qi* = *q+=i*, and *=i* + itself; *qo* and *qa* contain no enclitic. -/ +def bearsEnclitic (p : PersonalPronoun) : Bool := + p == iDisagr || p == qini || p == qoy || p == qi + +/-! ### Verification theorems -/ + +/-- Noyer/Scott's disagreement generalization, verified across the whole + paradigm: a cell's independent form contains *=i* iff its + [±author]/[±participant] values disagree (Table 4.4 × Table 4.9/4.11). -/ +theorem enclitic_iff_disagrees (c : PronCell) : + (independent c).any bearsEnclitic = true ↔ c.Disagrees := by + cases c <;> decide + +/-- Reduction is exactly first-personhood: the subject/possessor form differs + from the independent form precisely at [+author] cells (Table 4.1; + the impoverishment rule targets [+author] under agreement, §4.4). -/ +theorem reduction_iff_author (c : PronCell) : + subjPoss c ≠ independent c ↔ c.features.author = true := by + cases c <;> decide + +/-- What reduction leaves behind is never a base: every reduced (≠ independent) + cell surfaces as bare *=i* or as ∅ — the enclitic is all that survives + impoverishment. -/ +theorem reduced_residue (c : PronCell) (h : subjPoss c ≠ independent c) : + subjPoss c = some iDisagr ∨ subjPoss c = none := by + cases c <;> simp_all [subjPoss, independent] <;> decide + +end Mam diff --git a/Linglib/Fragments/Mayan/Mam/VoiceSystem.lean b/Linglib/Fragments/Mayan/Mam/VoiceSystem.lean index 218b2b68d..03aa80264 100644 --- a/Linglib/Fragments/Mayan/Mam/VoiceSystem.lean +++ b/Linglib/Fragments/Mayan/Mam/VoiceSystem.lean @@ -14,7 +14,7 @@ moved to: ([elkins-torrence-brown-2026]); also houses the antipassive Voice apparatus from [scott-2023] §2.5.4.1. - Cross-Studies consumer: - `Studies/Scott2023Agreement.lean` imports the Minimalist + `Studies/Scott2023.lean` imports the Minimalist Mam Voice from ETB2026 to compare φ-Agree and oblique-Agree pipelines. This Fragment file retains only `mamVoiceSystem : VoiceSystemProfile` — diff --git a/Linglib/Morphology/DM/Impoverishment.lean b/Linglib/Morphology/DM/Impoverishment.lean index cda0f3cb9..c9a93133c 100644 --- a/Linglib/Morphology/DM/Impoverishment.lean +++ b/Linglib/Morphology/DM/Impoverishment.lean @@ -28,7 +28,7 @@ deletion of the pronominal base morpheme when its features are redundantly expressed by agreement. This is structurally parallel to Impoverishment: features on the pronoun node are deleted (at PF) when they are recoverable from agreement, yielding a reduced form. Mam's -rule is paradigmatic — see `Studies/Scott2023Agreement.lean`. +rule is paradigmatic — see `Studies/Scott2023.lean`. -/ namespace Morphology.DM.Impoverishment diff --git a/Linglib/Studies/ElkinsTorrenceBrown2026.lean b/Linglib/Studies/ElkinsTorrenceBrown2026.lean index 072f52d32..054858ab2 100644 --- a/Linglib/Studies/ElkinsTorrenceBrown2026.lean +++ b/Linglib/Studies/ElkinsTorrenceBrown2026.lean @@ -5,7 +5,7 @@ import Linglib.Syntax.Minimalist.ClauseSpine import Linglib.Syntax.Minimalist.Voice import Linglib.Syntax.Minimalist.Agree import Linglib.Morphology.DM.VocabSimple -import Linglib.Studies.Scott2023Agreement +import Linglib.Studies.Scott2023 /-! # Oblique Extraction in Mayan @@ -141,7 +141,7 @@ Fragments," these belong with the paper that anchors them [scott-2023] for the antipassive). The Fragment file retains only the theory-neutral `mamVoiceSystem : VoiceSystemProfile`. -`Studies/Scott2023Agreement.lean` consumes `mamVoice` and +`Studies/Scott2023.lean` consumes `mamVoice` and `eqYaVocab` from this file via cross-Studies import. -/ /-- Mam agentive Voice head with [uOblique] probe. diff --git a/Linglib/Studies/Preminger2014.lean b/Linglib/Studies/Preminger2014.lean index cf9758d2c..6e7e8ce38 100644 --- a/Linglib/Studies/Preminger2014.lean +++ b/Linglib/Studies/Preminger2014.lean @@ -98,7 +98,7 @@ transitives + K'ichee' fragment + Zulu fragment) to formalize. [preminger-2014], [pancheva-zubizarreta-2018]). - `Morphology/DM/VocabSimple.lean` — the substrate: `Vocabulary`, `VocabEntry`, `makePersonVocab`. -- `Studies/Scott2023Agreement.lean` — parallel +- `Studies/Scott2023.lean` — parallel application of the same DM/Agree machinery to Mam (where Infl's φ-probe is blocked in transitives). - `Studies/CoonMateoPedroPreminger2014.lean` — diff --git a/Linglib/Studies/Scott2023.lean b/Linglib/Studies/Scott2023.lean index cfec92ae0..3e8550435 100644 --- a/Linglib/Studies/Scott2023.lean +++ b/Linglib/Studies/Scott2023.lean @@ -1,67 +1,75 @@ import Linglib.Syntax.Case.Dependent import Linglib.Syntax.Case.Alignment import Linglib.Syntax.Minimalist.Voice +import Linglib.Syntax.Minimalist.Agree +import Linglib.Syntax.Minimalist.ObligatoryOperations +import Linglib.Morphology.DM.VocabSimple +import Linglib.Morphology.DM.Impoverishment import Linglib.Fragments.Mayan.Mam.Agreement +import Linglib.Fragments.Mayan.Params /-! -# [scott-2023] — Voice-Based Case in Mam -[scott-2023] [woolford-1997] [marantz-1991] [baker-2015] +# [scott-2023] — Pronouns and Agreement in San Juan Atitán Mam -[scott-2023]'s analysis of San Juan Atitán Mam treats case as assigned -directly by functional heads keyed to argument position, building on -[woolford-1997]'s claim that ergative is lexical/inherent Case -assigned with θ-role rather than configurationally derived. +[scott-2023] [woolford-1997] [marantz-1991] [baker-2015] [chomsky-2000] +[deal-2024] [elkins-torrence-brown-2026] [preminger-2014] [england-2017] -## Three Heads, Three Cases +Single study file for [scott-2023] (UC Berkeley dissertation), in three +sections. -In Scott's Mam architecture each case has a dedicated assigner: +## Voice-based case -- **Voice → ERG** (inherent, to the agent in Spec,VoiceP — extending - [woolford-1997]'s inherent-ERG claim into a modern Voice-based - architecture) -- **Voice → ACC** (structural, to the patient — low-abs syntax, - §3.4) +Scott treats case as assigned directly by functional heads keyed to argument +position, building on [woolford-1997]'s claim that ergative is +lexical/inherent Case assigned with θ-role rather than configurationally +derived. Each case has a dedicated assigner: + +- **Voice → ERG** (inherent, to the agent in Spec,VoiceP) +- **Voice → ACC** (structural, to the patient — low-abs syntax, §3.4) - **Infl → ABS** (structural, to the intransitive subject) This produces a tripartite underlying system (ERG ≠ ACC ≠ ABS) visible -through the Mam agreement patterns formalized in -`Studies/Scott2023Agreement.lean`. - -## Contrast with Other Case Theories - -The Mam data discriminates between three theories of case assignment: - -1. **Agree-based** ([chomsky-2000], [chomsky-2001]): Case is - assigned by Agree from a probing functional head. ACC requires v* as a - *phase head*; non-thematic Voice (e.g., anticausative) is not a phase - head and cannot assign ACC. - -2. **Dependent case** ([marantz-1991], [baker-2015]): Case is - determined by the configuration of caseless NPs in a Spell-Out domain; - Voice flavor is irrelevant to the algorithm. +through the Mam agreement patterns. The Mam data discriminate between three +theories of case assignment: Agree-based ([chomsky-2000], [chomsky-2001]: +ACC requires a phase head), dependent case ([marantz-1991], [baker-2015]: +Voice flavor is irrelevant), and Voice-based (this analysis: the Voice head +selects ERG vs. ACC by θ-role; neither phase-hood nor NP configuration does +the work). The theorems stage the contrast. See `Studies/Woolford1997.lean` +for the predecessor analysis. -3. **Voice-based** (this file): Case is keyed to argument position via - functional heads. Neither phase-hood nor NP configuration is doing - the work — the Voice head itself selects ERG vs. ACC by θ-role, and - Infl independently assigns ABS to the intransitive subject. +## Agree-conditioned pronoun spellout -The theorems below stage the contrast: Voice-based positional assignment, -the Agree-style phase-head sensitivity it sidesteps, and the Voice-blind -behavior of the dependent case algorithm. +Connects Agree (feature valuation) and probe restriction to the distribution +of overt vs. reduced pronouns. In a transitive clause: Voice probes the +agent (Set A spellout, inherent ERG); Infl's probe has a disjunctive +satisfaction condition [SAT: φ or Voice_TR] and **stops** at transitive +Voice, so no φ reaches Infl and the Set B slot falls to the Elsewhere form +"tz'=". Agreed-with arguments (A, S) undergo pronoun reduction — agreement +redundantly expresses their φ-features, triggering deletion of the +pronominal base (ch. 4) — while the unagreed patient must be a full overt +pronoun. The same "tz'=" thus arises by two paths: real agreement with a +3SG S (no more specific entry matches) vs. probe failure in transitives. -## See Also +## Super-extended ergativity -- `Studies/Scott2023Agreement.lean` — full Agree/Spellout - pipeline for the Mam agreement morphology, including the impoverishment - rule that bleeds reduced pronouns -- `Studies/Scott2023.lean` — super-extended - ergativity (clause-type-conditioned alignment shift) -- `Studies/Woolford1997.lean` — the predecessor analysis - treating ERG as inherent Case +Theory-neutral data on split ergativity. Matrix clauses are tripartite +(A: Set A; S: Set B; P: default Set B). In certain dependent clauses +(purpose *tu'n*, reason, *taj* 'when'), alignment shifts to what +[england-2017] calls **super-extended ergativity**: Set A extends to ALL +arguments — the system becomes neutral. The trigger is clause type, not +aspect or person. Only default 2/3SG Set A (t-) is allowed for objects +in SEE clauses ([scott-2023], §2.6.3, ex. 196). Mam's SEE split is not a +binary ergative/accusative toggle, so `Syntax.Case.SplitErgativity` does +not fit; the custom `MamAlignment` struct captures the +tripartite-to-neutral contrast directly. -/ namespace Scott2023 +/-! ### Voice-based case -/ + +section VoiceCase + open Minimalist open Syntax.Case @@ -149,4 +157,560 @@ theorem dependent_case_tripartite : getCaseOf "lower" (assignCases .tripartite nps) = some .acc := by decide +end VoiceCase + +/-! ### Agree-conditioned pronoun spellout -/ + +section AgreeSpellout + +open Minimalist Mam +open Agreement + +-- ============================================================================ +-- § 0: Minimalism-Specific Vocabulary (Set A / Set B as VI entries) +-- ============================================================================ + +/-! These Vocabulary Insertion entries encode the Fragment's theory-neutral + marker tables as Minimalism feature bundles, enabling the Agree → Spellout + pipeline. The Fragment (`Agreement.lean`) stores the markers as simple + person × number → string tables; here they are parameterized by + `FeatureBundle` and `Cat` for use with `spellout`. -/ + +/-- PhiFeature list per Mam person-number cell. -/ +def mamToPhiFeatures (c : Agreement.Cell) : List PhiFeature := + [.person c.toPersonLevel, .number (if c.isPlural then .Plur else .Sing)] + +/-- Set A (ERG) vocabulary entries: φ-features on Voice (.v) + yield the morphological exponent ([scott-2023] Table 2.8). + All six cells have specific entries. -/ +def setAVocab : Vocabulary := + makePersonVocab Agreement.Cell.pnCells mamToPhiFeatures + (fun c => (setAExponent.realize c).getD "") (some .v) + +/-- Set B (ABS) vocabulary entries: φ-features on Infl (.T) + yield the morphological exponent ([scott-2023] Table 3.5). + Per Scott's DM analysis, only 1SG/1PL/2PL/3PL have specific + entries; 2SG and 3SG fall through to the Elsewhere entry + (no features, tz'=) which surfaces when no specific entry + matches — also catching the blocked-Infl-probe case in transitives. -/ +def setBVocab : Vocabulary := + makePersonVocab setBSpecificCells mamToPhiFeatures + (fun c => (setBExponent.realize c).getD "") (some .T) ++ + [{ features := [], exponent := defaultSetB, context := some .T }] + +/-- Which Minimalist head φ-Agrees with each argument position. + Ditransitive R/T default to none (not modeled). -/ +def agreeProbe : ArgPosition → Option Cat + | .A => some .v -- Voice probes, A in Spec,VoiceP + | .P => none -- Infl probe blocked by Voice_TR + | .S => some .T -- Infl probes, S in its domain + | .R | .T => none + +-- ============================================================================ +-- § 1: Probe Feature Bundles +-- ============================================================================ + +/-- Voice's probe features: [uPerson, uNumber]. + Placeholder values (.third, .Sing) are irrelevant — `sameType` matching + ensures any Person/Number goal is found regardless. -/ +def voiceProbe : FeatureBundle := + [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] + +/-- Infl's probe features: [uPerson, uNumber]. + In intransitives, these are valued by S. In transitives, the probe + is blocked by Voice_TR before reaching any DP. -/ +def inflProbe : FeatureBundle := + [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] + +-- ============================================================================ +-- § 2: Goal Feature Bundles (3SG test case) +-- ============================================================================ + +/-- A 3SG DP's features: [Person:3, Number:sg]. -/ +def dp3sg : FeatureBundle := + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] + +-- ============================================================================ +-- § 3: Agree Valuation — Voice agrees with agent +-- ============================================================================ + +/-- Voice's [uPerson] is valued as [Person:3] from a 3SG agent. -/ +theorem voice_agrees_person : + applyAgree voiceProbe dp3sg (.phi (.person .third)) = + some [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] := by + native_decide + +/-- After person agreement, Voice's [uNumber] is valued as [Number:sg]. + This is the second step of φ-Agree: person first, then number. -/ +theorem voice_agrees_number : + let afterPerson := [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] + applyAgree afterPerson dp3sg (.phi (.number .Sing)) = + some [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by + native_decide + +/-- Full φ-valuation of Voice by a 3SG agent: both person and number valued. -/ +def voiceFullyAgreed : FeatureBundle := + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] + +/-- The two-step Agree pipeline produces a fully valued bundle. -/ +theorem voice_agree_pipeline : + (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind + (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = + some voiceFullyAgreed := by + native_decide + +-- ============================================================================ +-- § 4: Set A Spellout — Voice → agreement morphology +-- ============================================================================ + +/-- Set A spellout: Voice's valued [Person:3, Number:sg] yields "t-" (A2/3SG). -/ +theorem setA_spellout_3sg : + spellout setAVocab voiceFullyAgreed (some .v) = some "t-" := by + native_decide + +/-- Set A spellout for 1SG: Voice with [Person:1, Number:sg] yields A1SG marker. -/ +theorem setA_spellout_1sg : + let v1sg : FeatureBundle := + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + spellout setAVocab v1sg (some .v) = some "n-/w-" := by + native_decide + +-- ============================================================================ +-- § 5: Set B — Two Paths to "tz'=" +-- ============================================================================ + +/-- **Intransitive path**: Infl Agrees with a 3SG intransitive S, copies + [Person:3, Number:sg]. No Set B entry is specified for these features + (1SG=chin, 1PL=qo, 2/3PL=chi — none match 3SG), so the Elsewhere + entry is selected: "tz'=". -/ +theorem setB_intransitive_3sg : + let inflAgreed : FeatureBundle := + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] + spellout setBVocab inflAgreed (some .T) = some "tz'=" := by + native_decide + +/-- **Transitive path**: Infl's probe is blocked by Voice_TR → no + φ-features are copied → the Infl node has an empty feature bundle. + The Elsewhere entry matches (empty features are a subset of anything) + and "tz'=" is selected. + + This is the DEFAULT Set B — it appears in transitives regardless of + the object's person/number features. -/ +theorem setB_transitive_default : + let inflBlocked : FeatureBundle := [] + spellout setBVocab inflBlocked (some .T) = some "tz'=" := by + native_decide + +/-- The two paths produce the same exponent — the surface form is + identical even though the underlying mechanism differs (real agreement + vs. probe failure). -/ +theorem setB_same_surface : + let inflAgreed3sg : FeatureBundle := + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] + let inflBlocked : FeatureBundle := [] + spellout setBVocab inflAgreed3sg (some .T) = + spellout setBVocab inflBlocked (some .T) := by + native_decide + +/-- Set B spellout for 1SG intransitive: Infl copies [Person:1, Number:sg] + from S, yielding "chin" — NOT the Elsewhere form. This is real + agreement, producing a distinct exponent. -/ +theorem setB_intransitive_1sg : + let t1sg : FeatureBundle := + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + spellout setBVocab t1sg (some .T) = some "chin" := by + native_decide + +/-- In a transitive with a 1SG object, the default "tz'=" still appears — + NOT "chin". This is because Infl's probe was blocked by Voice_TR, + so the object's 1SG features are never copied to Infl. -/ +theorem setB_transitive_ignores_object : + -- Even though the object is 1SG, Infl shows default "tz'=", not "chin" + let inflBlocked : FeatureBundle := [] + spellout setBVocab inflBlocked (some .T) = some "tz'=" ∧ + -- Compare: a 1SG intransitive S would trigger "chin" + let inflAgreed1sg : FeatureBundle := + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + spellout setBVocab inflAgreed1sg (some .T) = some "chin" := by + exact ⟨by native_decide, by native_decide⟩ + +-- ============================================================================ +-- § 6: Probe Restriction — Why objects lack φ-agreement +-- ============================================================================ + +/-- Infl's probe has a disjunctive satisfaction condition [SAT: φ or + Voice_TR]. In transitives, the probe encounters transitive Voice and + stops before reaching any DP. This is modeled by the fact that the + Infl node ends up with an empty feature bundle (no φ-features copied). + + In intransitives, Voice is not transitive → the probe continues → + finds S → copies φ. + + This mechanism replaces the older + "closest-goal intervention" account: it is NOT that the agent + intervenes between Infl and the object, but that the probe is + STOPPED by the VoiceP phase boundary. -/ +theorem probe_restriction_yields_default : + -- Transitive: probe blocked → empty → Elsewhere + spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ + -- Intransitive 1SG: probe succeeds → "chin" (not default) + spellout setBVocab + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (some .T) = some "chin" := by + exact ⟨by native_decide, by native_decide⟩ + +-- ============================================================================ +-- § 7: Intransitive Pipeline — Infl Agrees with S +-- ============================================================================ + +/-- In an intransitive clause, Infl probes for φ and Agrees with S. + This is REAL agreement — the probe copies S's φ-features. + The resulting valued features spell out as Set B. -/ +theorem intransitive_pipeline_1sg : + -- Infl Agrees with 1SG S + (applyAgree inflProbe + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (.phi (.person .third))).bind + (λ fb => applyAgree fb + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (.phi (.number .Sing))) = + some [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] ∧ + -- Spells out as "chin" (not default "tz'=") + spellout setBVocab + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (some .T) = some "chin" := by + exact ⟨by native_decide, by native_decide⟩ + +-- ============================================================================ +-- § 8: Transitive Pipeline — Voice Agrees, Infl Blocked +-- ============================================================================ + +/-- The complete prediction for a 3SG transitive clause: + + 1. Voice Agrees with agent → [Person:3, Number:sg] on Voice + 2. [Person:3, Number:sg] on Voice spells out as Set A "t-" + 3. Infl's probe is blocked by Voice_TR → empty bundle on Infl + 4. Empty Infl spells out as Elsewhere Set B "tz'=" + 5. Patient is not φ-Agreed-with → overt pronoun required -/ +theorem full_pipeline_3sg_transitive : + -- Step 1-2: Voice Agrees and spells out as Set A + (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind + (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = some voiceFullyAgreed ∧ + spellout setAVocab voiceFullyAgreed (some .v) = some "t-" ∧ + -- Step 3-4: Infl probe blocked → default Set B + spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ + -- Step 5: patient is not eligible for reduction → overt pronoun + ¬ ArgPosition.CanBeReduced .P := by + refine ⟨?_, ?_, ?_, ?_⟩ + · native_decide + · native_decide + · native_decide + · decide + +/-- The pipeline generalizes: for every argument position, reduction + eligibility ≡ φ-agreement (definitionally — `CanBeReduced := IsPhiAgreed`). -/ +theorem all_positions_match (pos : ArgPosition) : + pos.CanBeReduced ↔ pos.IsPhiAgreed := + Iff.rfl + +-- ============================================================================ +-- § 9: Cross-Paradigm Spellout +-- ============================================================================ + +/-- Set A and Set B have different contexts: Set A on Voice (.v), Set B + on Infl (.T). The same valued features produce different exponents + depending on which head hosts them. -/ +theorem setA_setB_differ_by_context : + spellout setAVocab voiceFullyAgreed (some .v) ≠ + spellout setBVocab voiceFullyAgreed (some .v) := by + native_decide + +/-- Set A vocabulary does NOT match Infl context. -/ +theorem setA_wrong_context : + spellout setAVocab voiceFullyAgreed (some .T) = none := by + native_decide + +/-- Set B vocabulary does NOT match Voice context (for specified entries). + Only the Elsewhere entry could match (it has no features), but it + requires Infl context. -/ +theorem setB_wrong_context : + spellout setBVocab voiceFullyAgreed (some .v) = none := by + native_decide + +-- ============================================================================ +-- § 10: The Tripartite Agreement Pattern +-- ============================================================================ + +/-- The three argument positions each have distinct agreement marking + patterns, yielding morphological tripartite alignment (Scott p. 113): + + - Agent (ERG): Set A agreement from Voice + - Intransitive S (ABS): Set B agreement from Infl + - Patient (ACC): default Set B (Infl probe blocked) + + These three cases each have distinct underlying syntactic case values, + assigned by different heads (Voice for ERG/ACC, Infl for ABS). -/ +theorem agreement_is_tripartite : + -- Agreed-with positions: A (ERG, by Voice) and S (ABS, by Infl) + ArgPosition.IsPhiAgreed .A ∧ + ArgPosition.case .A = .erg ∧ + ArgPosition.IsPhiAgreed .S ∧ + ArgPosition.case .S = .abs ∧ + -- Not agreed-with: P (ACC, from Voice but no φ-Agree) + ¬ ArgPosition.IsPhiAgreed .P ∧ + ArgPosition.case .P = .acc := + ⟨trivial, rfl, trivial, rfl, by decide, rfl⟩ + +/-- Agreement probes are on different heads: Voice for Set A, Infl for + Set B. The patient's lack of agreement is NOT because both heads + target the agent — it's because Infl's probe is blocked by VoiceP. -/ +theorem different_probe_heads : + agreeProbe .A = some .v ∧ + agreeProbe .S = some .T ∧ + agreeProbe .P = none := ⟨rfl, rfl, rfl⟩ + +-- ============================================================================ +-- § 11: Connecting to Obligatory Operations ([preminger-2014], Ch. 5) +-- ============================================================================ + +/-- The transitive Set B default is an instance of Preminger's probe failure: + Infl's probe searches an empty domain (blocked by Voice_TR) and finds no + DP with matching φ-features. `attemptAgree` maps the `none` result from + `applyAgree` to `ProbeOutcome.unvalued`. -/ +theorem transitive_is_probe_failure : + attemptAgree inflProbe [] (.phi (.person .third)) = .unvalued := by + native_decide + +/-- The intransitive case is real agreement: Infl's probe finds S and copies + its φ-features. `attemptAgree` maps the `some _` result to `.valued`. -/ +theorem intransitive_is_real_agreement : + attemptAgree inflProbe + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + (.phi (.person .third)) = .valued := by + native_decide + +/-- Under Preminger's obligatory-no-crash model, probe failure converges + and produces Elsewhere morphology — exactly the Set B "tz'=" we observe + in Mam transitives. This connects the abstract failure model to the + concrete spellout: `ProbeOutcome.unvalued` → `PFRealization.elsewhere` + → the Elsewhere Vocabulary entry → "tz'=". -/ +theorem probe_failure_converges_with_elsewhere : + derivationConverges .obligatoryNocrash .unvalued = true ∧ + ProbeOutcome.unvalued.pfRealization = .elsewhere := ⟨rfl, rfl⟩ + +-- ============================================================================ +-- § 12: Deriving Probe Blocking from SatisfactionCond ([deal-2024]) +-- ============================================================================ + +/-! The Fragment file (`Agreement.lean`) stipulates `isPhiAgreed := false` for + patients. Here we DERIVE that result from the `SatisfactionCond` machinery + in `Agree.lean`: Infl's disjunctive probe [SAT: φ or Voice_TR] encounters + transitive Voice and stops without copying features. + + This closes the gap between stipulation and derivation: the patient's + lack of φ-agreement is not an axiom but a consequence of probe + satisfaction theory. -/ + +/-- In a transitive clause, `mamInflSatisfaction` is satisfied by Voice_TR + (head encounter .v) and copies no features — matching the Fragment's + `¬ IsPhiAgreed .P`. -/ +theorem satisfaction_derives_patient_no_agree : + mamInflSatisfaction.isSatisfied [] (some .v) = true ∧ + mamInflSatisfaction.copiedFeatures [] (some .v) = false ∧ + ¬ ArgPosition.IsPhiAgreed .P := + ⟨by native_decide, by native_decide, by decide⟩ + +/-- In an intransitive clause, `mamInflSatisfaction` is satisfied by + φ-features and DOES copy them — matching `IsPhiAgreed .S`. -/ +theorem satisfaction_derives_intranS_agree : + let dp1sg := [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + mamInflSatisfaction.isSatisfied dp1sg none = true ∧ + mamInflSatisfaction.copiedFeatures dp1sg none = true ∧ + ArgPosition.IsPhiAgreed .S := + ⟨by native_decide, by native_decide, trivial⟩ + +/-- The satisfaction condition's `copiedFeatures` Bool aligns with + the Fragment's `IsPhiAgreed` Prop for both Infl-probed positions: + - patient (transitive): copiedFeatures = false ↔ ¬ IsPhiAgreed .P + - intranS (intransitive): copiedFeatures = true ↔ IsPhiAgreed .S -/ +theorem satisfaction_matches_fragment : + (mamInflSatisfaction.copiedFeatures [] (some .v) = true ↔ + ArgPosition.IsPhiAgreed .P) ∧ + (mamInflSatisfaction.copiedFeatures + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] + none = true ↔ + ArgPosition.IsPhiAgreed .S) := by + refine ⟨?_, ?_⟩ + · constructor <;> intro h <;> first | (native_decide) | trivial + · exact ⟨fun _ => trivial, fun _ => by native_decide⟩ + +-- The former §13 (Unified Agree — bridging Scott 2023's φ-Agree pipeline +-- with Elkins-Torrence-Brown 2026's oblique-Agree pipeline) violated the +-- chronological dependency rule (a 2023 study cross-referencing a 2026 +-- study). It moved to `Studies/ElkinsTorrenceBrown2026.lean` +-- (the later paper, which can correctly back-reference Scott 2023's +-- φ-probe + Set A vocabulary defs). + +-- ============================================================================ +-- § 14: Impoverishment — Connecting to DM ([scott-2023], §4.4.3) +-- ============================================================================ + +/-! Scott's impoverishment rule (ex. 84/94): + + `[+/−singular] → ∅ / [+author]^F` + + Deletes [±singular] from first person pronouns that have been + agreed with (marked by the F diacritic). This bleeds insertion of + the pronominal base morphemes *qin* ([+author,+singular]) and *qo* + ([+author,−singular]), yielding reduced pronouns. + + We model this using `Morphology.DM.Impoverishment.ImpoverishmentRule`. + The condition checks for [+author] (= first person in our feature + system), and the target is [±singular] (= number). -/ + +/-- The Mam first-person impoverishment rule: delete [±singular] + (number) when the bundle contains [+author] (first person) features + that have been agreed with. + + Built via the `paradigmatic` smart constructor — the F-diacritic + condition only inspects the focus bundle (the agreed-with pronoun's + own features), so the rule is paradigmatic by construction. -/ +def mamImpoverishmentRule : Morphology.DM.Impoverishment.ImpoverishmentRule := + Morphology.DM.Impoverishment.paradigmatic + -- Check for [+author] (= valued first person): the F diacritic + -- condition is modeled by this rule only being applied in + -- agreed-with contexts (subj/poss position, not objects). + (λ fb => fb.any (λ f => match f with + | .valued (.phi (.person .first)) => true + | _ => false)) + (.phi (.number .Sing)) + +/-- Mam's rule is paradigmatic — discharged by the smart constructor. -/ +theorem mamImpoverishment_paradigmatic : + Morphology.DM.Impoverishment.Paradigmatic mamImpoverishmentRule := + Morphology.DM.Impoverishment.paradigmatic_isParadigmatic _ _ + +/-- The impoverishment rule fires for 1st person bundles. -/ +theorem impoverishment_fires_1sg : + mamImpoverishmentRule.condition + (Morphology.DM.Impoverishment.Neighborhood.ofBundle + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))]) := by + decide + +/-- The impoverishment rule does NOT fire for 3rd person bundles. -/ +theorem impoverishment_blocked_3sg : + ¬ mamImpoverishmentRule.condition + (Morphology.DM.Impoverishment.Neighborhood.ofBundle + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))]) := by + decide + +/-- After impoverishment, the number feature is deleted from 1st + person bundles, bleeding insertion of the base morpheme *qin*. -/ +theorem impoverishment_deletes_number : + mamImpoverishmentRule.applyToBundle + [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] = + [.valued (.phi (.person .first))] := by + decide + +/-- Without impoverishment (3rd person), the number feature survives. -/ +theorem no_impoverishment_preserves : + mamImpoverishmentRule.applyToBundle + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] = + [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by + decide + +end AgreeSpellout + +/-! ### Super-extended ergativity -/ + +section SuperExtendedErgativity + +open Mayan (MarkerSet) + +-- ============================================================================ +-- § 1: Clause-Type-Conditioned Alignment +-- ============================================================================ + +/-- The Mam alignment in a given clause type. -/ +structure MamAlignment where + /-- Marker set for S (intransitive subject) -/ + sMarker : MarkerSet + /-- Marker set for A (transitive agent) -/ + aMarker : MarkerSet + /-- Marker set for O (transitive patient) -/ + oMarker : MarkerSet + deriving DecidableEq, Repr + +/-- Matrix clause alignment: tripartite. + S = Set B (ABS), A = Set A (ERG), O = default Set B (no agreement). -/ +def matrixAlignment : MamAlignment := + { sMarker := .setB, aMarker := .setA, oMarker := .setB } + +/-- Super-extended ergative alignment: neutral (all Set A). -/ +def seeAlignment : MamAlignment := + { sMarker := .setA, aMarker := .setA, oMarker := .setA } + +-- ============================================================================ +-- § 2: Verification +-- ============================================================================ + +/-- Matrix alignment is tripartite: S, A, O each have distinct marking + patterns (S ≠ A by marker set; S ≡ O by marker set but S has real + agreement while O has default — the tripartite distinction is + agreement-based, not marker-set-based). -/ +theorem matrix_s_ne_a : matrixAlignment.sMarker ≠ matrixAlignment.aMarker := by + decide + +/-- SEE alignment is neutral: all arguments get the same marker set. -/ +theorem see_is_neutral : + seeAlignment.sMarker = seeAlignment.aMarker ∧ + seeAlignment.aMarker = seeAlignment.oMarker := ⟨rfl, rfl⟩ + +/-- The split: matrix and SEE differ in S marking and O marking. -/ +theorem split_ergativity : + matrixAlignment.sMarker ≠ seeAlignment.sMarker ∧ + matrixAlignment.oMarker ≠ seeAlignment.oMarker ∧ + matrixAlignment.aMarker = seeAlignment.aMarker := by + exact ⟨by decide, by decide, rfl⟩ + +/-- A is invariant across the split: Set A in both matrix and SEE. -/ +theorem a_invariant : + matrixAlignment.aMarker = seeAlignment.aMarker := rfl + +-- ============================================================================ +-- § 3: Subordinators That Trigger SEE +-- ============================================================================ + +/-- Subordinators that trigger super-extended ergativity in SJA Mam. -/ +inductive SEETrigger where + | tun -- *tu'n*: purpose/reason clauses + | taj -- *taj*: 'when' (past) + | aj -- *aj*: 'when' (future) + | chix -- *ch'ix*: 'almost' + | nim -- *ni'm*: 'right now' + | nanx -- *na'nx*: 'not yet' + deriving DecidableEq, Repr + +/-- All SEE triggers yield the same neutral alignment. -/ +def seeTriggerAlignment (_ : SEETrigger) : MamAlignment := seeAlignment + +-- ============================================================================ +-- § 4: Object Agreement Restriction in SEE +-- ============================================================================ + +/-- In SEE clauses, object Set A markers are restricted to the default + 2/3SG form (t-). Agreeing Set A markers for the object are + ungrammatical. This parallels the default Set B (tz'=) pattern for + objects in matrix clauses. -/ +def objectSetAIsDefault : Bool := true + +/-- The parallel: in BOTH matrix and SEE, the object slot shows default + (non-agreeing) morphology. The default marker just changes: + - Matrix: default Set B (tz'=) + - SEE: default Set A (t-) -/ +theorem object_default_parallel : + objectSetAIsDefault = true := rfl + +end SuperExtendedErgativity + end Scott2023 diff --git a/Linglib/Studies/Scott2023Agreement.lean b/Linglib/Studies/Scott2023Agreement.lean deleted file mode 100644 index a4baa39d9..000000000 --- a/Linglib/Studies/Scott2023Agreement.lean +++ /dev/null @@ -1,515 +0,0 @@ -import Linglib.Fragments.Mayan.Mam.Agreement -import Linglib.Syntax.Minimalist.Agree -import Linglib.Morphology.DM.VocabSimple -import Linglib.Syntax.Minimalist.ObligatoryOperations -import Linglib.Morphology.DM.Impoverishment - -/-! -# Minimalism Agree-Conditioned Pronoun Spellout in Mam - -[scott-2023] [chomsky-2000] [deal-2024] [elkins-torrence-brown-2026] [preminger-2014] - -Connects the Agree operation (feature valuation) and probe restriction to the empirical distribution of overt vs. -reduced pronouns in SJA Mam. - -## The Derivation - -In a Mam transitive clause with a 3SG agent and 3SG patient: - -1. **Voice probes for φ**: Voice has [uPerson, uNumber]. It Agrees with - the agent in Spec,VoiceP, valuing [Person:3, Number:sg]. Voice also - assigns inherent ERG case to the agent. The valued φ-features spell - out as Set A "t-" on Voice. - -2. **Infl probes for φ**: Infl has a φ-probe with a disjunctive - satisfaction condition [SAT: φ or Voice_TR]. - In a transitive clause, the probe encounters transitive Voice and - **stops** — no φ-features are copied to Infl. The Set B slot is - filled by the Elsewhere form "tz'=" (default 2/3SG). - -3. **Object is case-licensed by Voice**: The patient receives structural - ACC from Voice (low-abs syntax; [scott-2023], §3.4). Infl's probe - never reaches the object because it was satisfied by Voice_TR. - -4. **Pronoun realization follows**: Agreed-with arguments (agent, S) - undergo pronoun reduction — agreement morphology redundantly - expresses their φ-features, triggering deletion of the pronominal - base ([scott-2023], ch. 4). The patient, lacking φ-agreement, must - be a full overt pronoun. - -## Two Paths to Set B "tz'=" - -A key insight of Scott's analysis is that the same Set B form "tz'=" arises -via two distinct mechanisms: - -- **Intransitive**: Infl's probe succeeds, copies S's φ-features - (e.g., [3SG]) → no more specific Set B entry matches → Elsewhere - "tz'=" is selected. -- **Transitive**: Infl's probe is blocked by Voice_TR → no φ-features - on Infl → Elsewhere "tz'=" is selected. - -Both yield "tz'=", but the intransitive case involves real agreement while -the transitive case involves probe failure. This bridge demonstrates -both paths. - --/ - -namespace Scott2023 - -open Minimalist Mam -open Agreement - --- ============================================================================ --- § 0: Minimalism-Specific Vocabulary (Set A / Set B as VI entries) --- ============================================================================ - -/-! These Vocabulary Insertion entries encode the Fragment's theory-neutral - marker tables as Minimalism feature bundles, enabling the Agree → Spellout - pipeline. The Fragment (`Agreement.lean`) stores the markers as simple - person × number → string tables; here they are parameterized by - `FeatureBundle` and `Cat` for use with `spellout`. -/ - -/-- PhiFeature list per Mam person-number cell. -/ -def mamToPhiFeatures (c : Agreement.Cell) : List PhiFeature := - [.person c.toPersonLevel, .number (if c.isPlural then .Plur else .Sing)] - -/-- Set A (ERG) vocabulary entries: φ-features on Voice (.v) - yield the morphological exponent ([scott-2023] Table 2.8). - All six cells have specific entries. -/ -def setAVocab : Vocabulary := - makePersonVocab Agreement.Cell.pnCells mamToPhiFeatures - (fun c => (setAExponent.realize c).getD "") (some .v) - -/-- Set B (ABS) vocabulary entries: φ-features on Infl (.T) - yield the morphological exponent ([scott-2023] Table 3.5). - Per Scott's DM analysis, only 1SG/1PL/2PL/3PL have specific - entries; 2SG and 3SG fall through to the Elsewhere entry - (no features, tz'=) which surfaces when no specific entry - matches — also catching the blocked-Infl-probe case in transitives. -/ -def setBVocab : Vocabulary := - makePersonVocab setBSpecificCells mamToPhiFeatures - (fun c => (setBExponent.realize c).getD "") (some .T) ++ - [{ features := [], exponent := defaultSetB, context := some .T }] - -/-- Which Minimalist head φ-Agrees with each argument position. - Ditransitive R/T default to none (not modeled). -/ -def agreeProbe : ArgPosition → Option Cat - | .A => some .v -- Voice probes, A in Spec,VoiceP - | .P => none -- Infl probe blocked by Voice_TR - | .S => some .T -- Infl probes, S in its domain - | .R | .T => none - --- ============================================================================ --- § 1: Probe Feature Bundles --- ============================================================================ - -/-- Voice's probe features: [uPerson, uNumber]. - Placeholder values (.third, .Sing) are irrelevant — `sameType` matching - ensures any Person/Number goal is found regardless. -/ -def voiceProbe : FeatureBundle := - [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] - -/-- Infl's probe features: [uPerson, uNumber]. - In intransitives, these are valued by S. In transitives, the probe - is blocked by Voice_TR before reaching any DP. -/ -def inflProbe : FeatureBundle := - [.unvalued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] - --- ============================================================================ --- § 2: Goal Feature Bundles (3SG test case) --- ============================================================================ - -/-- A 3SG DP's features: [Person:3, Number:sg]. -/ -def dp3sg : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] - --- ============================================================================ --- § 3: Agree Valuation — Voice agrees with agent --- ============================================================================ - -/-- Voice's [uPerson] is valued as [Person:3] from a 3SG agent. -/ -theorem voice_agrees_person : - applyAgree voiceProbe dp3sg (.phi (.person .third)) = - some [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] := by - native_decide - -/-- After person agreement, Voice's [uNumber] is valued as [Number:sg]. - This is the second step of φ-Agree: person first, then number. -/ -theorem voice_agrees_number : - let afterPerson := [.valued (.phi (.person .third)), .unvalued (.phi (.number .Sing))] - applyAgree afterPerson dp3sg (.phi (.number .Sing)) = - some [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by - native_decide - -/-- Full φ-valuation of Voice by a 3SG agent: both person and number valued. -/ -def voiceFullyAgreed : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] - -/-- The two-step Agree pipeline produces a fully valued bundle. -/ -theorem voice_agree_pipeline : - (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind - (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = - some voiceFullyAgreed := by - native_decide - --- ============================================================================ --- § 4: Set A Spellout — Voice → agreement morphology --- ============================================================================ - -/-- Set A spellout: Voice's valued [Person:3, Number:sg] yields "t-" (A2/3SG). -/ -theorem setA_spellout_3sg : - spellout setAVocab voiceFullyAgreed (some .v) = some "t-" := by - native_decide - -/-- Set A spellout for 1SG: Voice with [Person:1, Number:sg] yields A1SG marker. -/ -theorem setA_spellout_1sg : - let v1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - spellout setAVocab v1sg (some .v) = some "n-/w-" := by - native_decide - --- ============================================================================ --- § 5: Set B — Two Paths to "tz'=" --- ============================================================================ - -/-- **Intransitive path**: Infl Agrees with a 3SG intransitive S, copies - [Person:3, Number:sg]. No Set B entry is specified for these features - (1SG=chin, 1PL=qo, 2/3PL=chi — none match 3SG), so the Elsewhere - entry is selected: "tz'=". -/ -theorem setB_intransitive_3sg : - let inflAgreed : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] - spellout setBVocab inflAgreed (some .T) = some "tz'=" := by - native_decide - -/-- **Transitive path**: Infl's probe is blocked by Voice_TR → no - φ-features are copied → the Infl node has an empty feature bundle. - The Elsewhere entry matches (empty features are a subset of anything) - and "tz'=" is selected. - - This is the DEFAULT Set B — it appears in transitives regardless of - the object's person/number features. -/ -theorem setB_transitive_default : - let inflBlocked : FeatureBundle := [] - spellout setBVocab inflBlocked (some .T) = some "tz'=" := by - native_decide - -/-- The two paths produce the same exponent — the surface form is - identical even though the underlying mechanism differs (real agreement - vs. probe failure). -/ -theorem setB_same_surface : - let inflAgreed3sg : FeatureBundle := - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] - let inflBlocked : FeatureBundle := [] - spellout setBVocab inflAgreed3sg (some .T) = - spellout setBVocab inflBlocked (some .T) := by - native_decide - -/-- Set B spellout for 1SG intransitive: Infl copies [Person:1, Number:sg] - from S, yielding "chin" — NOT the Elsewhere form. This is real - agreement, producing a distinct exponent. -/ -theorem setB_intransitive_1sg : - let t1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - spellout setBVocab t1sg (some .T) = some "chin" := by - native_decide - -/-- In a transitive with a 1SG object, the default "tz'=" still appears — - NOT "chin". This is because Infl's probe was blocked by Voice_TR, - so the object's 1SG features are never copied to Infl. -/ -theorem setB_transitive_ignores_object : - -- Even though the object is 1SG, Infl shows default "tz'=", not "chin" - let inflBlocked : FeatureBundle := [] - spellout setBVocab inflBlocked (some .T) = some "tz'=" ∧ - -- Compare: a 1SG intransitive S would trigger "chin" - let inflAgreed1sg : FeatureBundle := - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - spellout setBVocab inflAgreed1sg (some .T) = some "chin" := by - exact ⟨by native_decide, by native_decide⟩ - --- ============================================================================ --- § 6: Probe Restriction — Why objects lack φ-agreement --- ============================================================================ - -/-- Infl's probe has a disjunctive satisfaction condition [SAT: φ or - Voice_TR]. In transitives, the probe encounters transitive Voice and - stops before reaching any DP. This is modeled by the fact that the - Infl node ends up with an empty feature bundle (no φ-features copied). - - In intransitives, Voice is not transitive → the probe continues → - finds S → copies φ. - - This mechanism replaces the older - "closest-goal intervention" account: it is NOT that the agent - intervenes between Infl and the object, but that the probe is - STOPPED by the VoiceP phase boundary. -/ -theorem probe_restriction_yields_default : - -- Transitive: probe blocked → empty → Elsewhere - spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ - -- Intransitive 1SG: probe succeeds → "chin" (not default) - spellout setBVocab - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - (some .T) = some "chin" := by - exact ⟨by native_decide, by native_decide⟩ - --- ============================================================================ --- § 7: Intransitive Pipeline — Infl Agrees with S --- ============================================================================ - -/-- In an intransitive clause, Infl probes for φ and Agrees with S. - This is REAL agreement — the probe copies S's φ-features. - The resulting valued features spell out as Set B. -/ -theorem intransitive_pipeline_1sg : - -- Infl Agrees with 1SG S - (applyAgree inflProbe - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - (.phi (.person .third))).bind - (λ fb => applyAgree fb - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - (.phi (.number .Sing))) = - some [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] ∧ - -- Spells out as "chin" (not default "tz'=") - spellout setBVocab - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - (some .T) = some "chin" := by - exact ⟨by native_decide, by native_decide⟩ - --- ============================================================================ --- § 8: Transitive Pipeline — Voice Agrees, Infl Blocked --- ============================================================================ - -/-- The complete prediction for a 3SG transitive clause: - - 1. Voice Agrees with agent → [Person:3, Number:sg] on Voice - 2. [Person:3, Number:sg] on Voice spells out as Set A "t-" - 3. Infl's probe is blocked by Voice_TR → empty bundle on Infl - 4. Empty Infl spells out as Elsewhere Set B "tz'=" - 5. Patient is not φ-Agreed-with → overt pronoun required -/ -theorem full_pipeline_3sg_transitive : - -- Step 1-2: Voice Agrees and spells out as Set A - (applyAgree voiceProbe dp3sg (.phi (.person .third))).bind - (λ fb => applyAgree fb dp3sg (.phi (.number .Sing))) = some voiceFullyAgreed ∧ - spellout setAVocab voiceFullyAgreed (some .v) = some "t-" ∧ - -- Step 3-4: Infl probe blocked → default Set B - spellout setBVocab ([] : FeatureBundle) (some .T) = some "tz'=" ∧ - -- Step 5: patient is not eligible for reduction → overt pronoun - ¬ ArgPosition.CanBeReduced .P := by - refine ⟨?_, ?_, ?_, ?_⟩ - · native_decide - · native_decide - · native_decide - · decide - -/-- The pipeline generalizes: for every argument position, reduction - eligibility ≡ φ-agreement (definitionally — `CanBeReduced := IsPhiAgreed`). -/ -theorem all_positions_match (pos : ArgPosition) : - pos.CanBeReduced ↔ pos.IsPhiAgreed := - Iff.rfl - --- ============================================================================ --- § 9: Cross-Paradigm Spellout --- ============================================================================ - -/-- Set A and Set B have different contexts: Set A on Voice (.v), Set B - on Infl (.T). The same valued features produce different exponents - depending on which head hosts them. -/ -theorem setA_setB_differ_by_context : - spellout setAVocab voiceFullyAgreed (some .v) ≠ - spellout setBVocab voiceFullyAgreed (some .v) := by - native_decide - -/-- Set A vocabulary does NOT match Infl context. -/ -theorem setA_wrong_context : - spellout setAVocab voiceFullyAgreed (some .T) = none := by - native_decide - -/-- Set B vocabulary does NOT match Voice context (for specified entries). - Only the Elsewhere entry could match (it has no features), but it - requires Infl context. -/ -theorem setB_wrong_context : - spellout setBVocab voiceFullyAgreed (some .v) = none := by - native_decide - --- ============================================================================ --- § 10: The Tripartite Agreement Pattern --- ============================================================================ - -/-- The three argument positions each have distinct agreement marking - patterns, yielding morphological tripartite alignment (Scott p. 113): - - - Agent (ERG): Set A agreement from Voice - - Intransitive S (ABS): Set B agreement from Infl - - Patient (ACC): default Set B (Infl probe blocked) - - These three cases each have distinct underlying syntactic case values, - assigned by different heads (Voice for ERG/ACC, Infl for ABS). -/ -theorem agreement_is_tripartite : - -- Agreed-with positions: A (ERG, by Voice) and S (ABS, by Infl) - ArgPosition.IsPhiAgreed .A ∧ - ArgPosition.case .A = .erg ∧ - ArgPosition.IsPhiAgreed .S ∧ - ArgPosition.case .S = .abs ∧ - -- Not agreed-with: P (ACC, from Voice but no φ-Agree) - ¬ ArgPosition.IsPhiAgreed .P ∧ - ArgPosition.case .P = .acc := - ⟨trivial, rfl, trivial, rfl, by decide, rfl⟩ - -/-- Agreement probes are on different heads: Voice for Set A, Infl for - Set B. The patient's lack of agreement is NOT because both heads - target the agent — it's because Infl's probe is blocked by VoiceP. -/ -theorem different_probe_heads : - agreeProbe .A = some .v ∧ - agreeProbe .S = some .T ∧ - agreeProbe .P = none := ⟨rfl, rfl, rfl⟩ - --- ============================================================================ --- § 11: Connecting to Obligatory Operations ([preminger-2014], Ch. 5) --- ============================================================================ - -/-- The transitive Set B default is an instance of Preminger's probe failure: - Infl's probe searches an empty domain (blocked by Voice_TR) and finds no - DP with matching φ-features. `attemptAgree` maps the `none` result from - `applyAgree` to `ProbeOutcome.unvalued`. -/ -theorem transitive_is_probe_failure : - attemptAgree inflProbe [] (.phi (.person .third)) = .unvalued := by - native_decide - -/-- The intransitive case is real agreement: Infl's probe finds S and copies - its φ-features. `attemptAgree` maps the `some _` result to `.valued`. -/ -theorem intransitive_is_real_agreement : - attemptAgree inflProbe - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - (.phi (.person .third)) = .valued := by - native_decide - -/-- Under Preminger's obligatory-no-crash model, probe failure converges - and produces Elsewhere morphology — exactly the Set B "tz'=" we observe - in Mam transitives. This connects the abstract failure model to the - concrete spellout: `ProbeOutcome.unvalued` → `PFRealization.elsewhere` - → the Elsewhere Vocabulary entry → "tz'=". -/ -theorem probe_failure_converges_with_elsewhere : - derivationConverges .obligatoryNocrash .unvalued = true ∧ - ProbeOutcome.unvalued.pfRealization = .elsewhere := ⟨rfl, rfl⟩ - --- ============================================================================ --- § 12: Deriving Probe Blocking from SatisfactionCond ([deal-2024]) --- ============================================================================ - -/-! The Fragment file (`Agreement.lean`) stipulates `isPhiAgreed := false` for - patients. Here we DERIVE that result from the `SatisfactionCond` machinery - in `Agree.lean`: Infl's disjunctive probe [SAT: φ or Voice_TR] encounters - transitive Voice and stops without copying features. - - This closes the gap between stipulation and derivation: the patient's - lack of φ-agreement is not an axiom but a consequence of probe - satisfaction theory. -/ - -/-- In a transitive clause, `mamInflSatisfaction` is satisfied by Voice_TR - (head encounter .v) and copies no features — matching the Fragment's - `¬ IsPhiAgreed .P`. -/ -theorem satisfaction_derives_patient_no_agree : - mamInflSatisfaction.isSatisfied [] (some .v) = true ∧ - mamInflSatisfaction.copiedFeatures [] (some .v) = false ∧ - ¬ ArgPosition.IsPhiAgreed .P := - ⟨by native_decide, by native_decide, by decide⟩ - -/-- In an intransitive clause, `mamInflSatisfaction` is satisfied by - φ-features and DOES copy them — matching `IsPhiAgreed .S`. -/ -theorem satisfaction_derives_intranS_agree : - let dp1sg := [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - mamInflSatisfaction.isSatisfied dp1sg none = true ∧ - mamInflSatisfaction.copiedFeatures dp1sg none = true ∧ - ArgPosition.IsPhiAgreed .S := - ⟨by native_decide, by native_decide, trivial⟩ - -/-- The satisfaction condition's `copiedFeatures` Bool aligns with - the Fragment's `IsPhiAgreed` Prop for both Infl-probed positions: - - patient (transitive): copiedFeatures = false ↔ ¬ IsPhiAgreed .P - - intranS (intransitive): copiedFeatures = true ↔ IsPhiAgreed .S -/ -theorem satisfaction_matches_fragment : - (mamInflSatisfaction.copiedFeatures [] (some .v) = true ↔ - ArgPosition.IsPhiAgreed .P) ∧ - (mamInflSatisfaction.copiedFeatures - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] - none = true ↔ - ArgPosition.IsPhiAgreed .S) := by - refine ⟨?_, ?_⟩ - · constructor <;> intro h <;> first | (native_decide) | trivial - · exact ⟨fun _ => trivial, fun _ => by native_decide⟩ - --- The former §13 (Unified Agree — bridging Scott 2023's φ-Agree pipeline --- with Elkins-Torrence-Brown 2026's oblique-Agree pipeline) violated the --- chronological dependency rule (a 2023 study cross-referencing a 2026 --- study). It moved to `Studies/ElkinsTorrenceBrown2026.lean` --- (the later paper, which can correctly back-reference Scott 2023's --- φ-probe + Set A vocabulary defs). - --- ============================================================================ --- § 14: Impoverishment — Connecting to DM ([scott-2023], §4.4.3) --- ============================================================================ - -/-! Scott's impoverishment rule (ex. 84/94): - - `[+/−singular] → ∅ / [+author]^F` - - Deletes [±singular] from first person pronouns that have been - agreed with (marked by the F diacritic). This bleeds insertion of - the pronominal base morphemes *qin* ([+author,+singular]) and *qo* - ([+author,−singular]), yielding reduced pronouns. - - We model this using `Morphology.DM.Impoverishment.ImpoverishmentRule`. - The condition checks for [+author] (= first person in our feature - system), and the target is [±singular] (= number). -/ - -/-- The Mam first-person impoverishment rule: delete [±singular] - (number) when the bundle contains [+author] (first person) features - that have been agreed with. - - Built via the `paradigmatic` smart constructor — the F-diacritic - condition only inspects the focus bundle (the agreed-with pronoun's - own features), so the rule is paradigmatic by construction. -/ -def mamImpoverishmentRule : Morphology.DM.Impoverishment.ImpoverishmentRule := - Morphology.DM.Impoverishment.paradigmatic - -- Check for [+author] (= valued first person): the F diacritic - -- condition is modeled by this rule only being applied in - -- agreed-with contexts (subj/poss position, not objects). - (λ fb => fb.any (λ f => match f with - | .valued (.phi (.person .first)) => true - | _ => false)) - (.phi (.number .Sing)) - -/-- Mam's rule is paradigmatic — discharged by the smart constructor. -/ -theorem mamImpoverishment_paradigmatic : - Morphology.DM.Impoverishment.Paradigmatic mamImpoverishmentRule := - Morphology.DM.Impoverishment.paradigmatic_isParadigmatic _ _ - -/-- The impoverishment rule fires for 1st person bundles. -/ -theorem impoverishment_fires_1sg : - mamImpoverishmentRule.condition - (Morphology.DM.Impoverishment.Neighborhood.ofBundle - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))]) := by - decide - -/-- The impoverishment rule does NOT fire for 3rd person bundles. -/ -theorem impoverishment_blocked_3sg : - ¬ mamImpoverishmentRule.condition - (Morphology.DM.Impoverishment.Neighborhood.ofBundle - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))]) := by - decide - -/-- After impoverishment, the number feature is deleted from 1st - person bundles, bleeding insertion of the base morpheme *qin*. -/ -theorem impoverishment_deletes_number : - mamImpoverishmentRule.applyToBundle - [.valued (.phi (.person .first)), .valued (.phi (.number .Sing))] = - [.valued (.phi (.person .first))] := by - decide - -/-- Without impoverishment (3rd person), the number feature survives. -/ -theorem no_impoverishment_preserves : - mamImpoverishmentRule.applyToBundle - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] = - [.valued (.phi (.person .third)), .valued (.phi (.number .Sing))] := by - decide - -end Scott2023 diff --git a/Linglib/Studies/Scott2023Ergativity.lean b/Linglib/Studies/Scott2023Ergativity.lean deleted file mode 100644 index a8cd8b9e2..000000000 --- a/Linglib/Studies/Scott2023Ergativity.lean +++ /dev/null @@ -1,140 +0,0 @@ -import Linglib.Fragments.Mayan.Mam.Agreement -import Linglib.Fragments.Mayan.Params - -/-! -# Super-Extended Ergativity in SJA Mam -[scott-2023] [england-2017] - -Theory-neutral data on split ergativity in San Juan Atitán (SJA) Mam. - -## The Phenomenon - -In matrix clauses, Mam shows a tripartite agreement pattern: -- A (transitive agent): Set A (ERG) -- S (intransitive subject): Set B (ABS) -- P (transitive patient): default Set B (no agreement) - -In certain dependent clauses — purpose clauses headed by *tu'n*, reason -clauses, *taj* 'when' clauses — the alignment shifts to what -[england-2017] calls **super-extended ergativity**: Set A marking -extends to ALL arguments (S, A, and O). The system becomes "neutral" -with all arguments receiving the same marker set. - -## The Split - -The trigger is clause type, not aspect or person features: -- **Matrix clauses**: tripartite (ERG Set A / ABS Set B / default Set B) -- **Super-extended ergative (SEE) clauses**: neutral (all Set A) - -## Key Data Points - -1. Intransitive S in SEE clauses: Set A (not Set B as in matrix) -2. Transitive A in SEE clauses: Set A (same as matrix) -3. Transitive O in SEE clauses: Set A on directional (not default Set B/ - independent pronoun as in matrix). Only default 2/3SG Set A (t-) is - allowed — agreeing Set A markers for the object are ungrammatical - ([scott-2023], §2.6.3, ex. 196). - -## Why Not `SplitErgativity`? - -`Syntax.Case.SplitErgativity` models a binary toggle between ergative and -accusative alignment conditioned by some factor (e.g., aspect in Hindi). -Mam's SEE split is not binary — it goes from tripartite (three distinct -marking patterns) to neutral (one pattern for all). The custom -`MamAlignment` struct captures this richer contrast directly. - -## See Also - -`Scott2023` for the Agree-based derivation -of the matrix tripartite pattern (probe blocking by Voice_TR). --/ - -namespace Scott2023 - -open Mayan (MarkerSet) - --- ============================================================================ --- § 1: Clause-Type-Conditioned Alignment --- ============================================================================ - -/-- The Mam alignment in a given clause type. -/ -structure MamAlignment where - /-- Marker set for S (intransitive subject) -/ - sMarker : MarkerSet - /-- Marker set for A (transitive agent) -/ - aMarker : MarkerSet - /-- Marker set for O (transitive patient) -/ - oMarker : MarkerSet - deriving DecidableEq, Repr - -/-- Matrix clause alignment: tripartite. - S = Set B (ABS), A = Set A (ERG), O = default Set B (no agreement). -/ -def matrixAlignment : MamAlignment := - { sMarker := .setB, aMarker := .setA, oMarker := .setB } - -/-- Super-extended ergative alignment: neutral (all Set A). -/ -def seeAlignment : MamAlignment := - { sMarker := .setA, aMarker := .setA, oMarker := .setA } - --- ============================================================================ --- § 2: Verification --- ============================================================================ - -/-- Matrix alignment is tripartite: S, A, O each have distinct marking - patterns (S ≠ A by marker set; S ≡ O by marker set but S has real - agreement while O has default — the tripartite distinction is - agreement-based, not marker-set-based). -/ -theorem matrix_s_ne_a : matrixAlignment.sMarker ≠ matrixAlignment.aMarker := by - decide - -/-- SEE alignment is neutral: all arguments get the same marker set. -/ -theorem see_is_neutral : - seeAlignment.sMarker = seeAlignment.aMarker ∧ - seeAlignment.aMarker = seeAlignment.oMarker := ⟨rfl, rfl⟩ - -/-- The split: matrix and SEE differ in S marking and O marking. -/ -theorem split_ergativity : - matrixAlignment.sMarker ≠ seeAlignment.sMarker ∧ - matrixAlignment.oMarker ≠ seeAlignment.oMarker ∧ - matrixAlignment.aMarker = seeAlignment.aMarker := by - exact ⟨by decide, by decide, rfl⟩ - -/-- A is invariant across the split: Set A in both matrix and SEE. -/ -theorem a_invariant : - matrixAlignment.aMarker = seeAlignment.aMarker := rfl - --- ============================================================================ --- § 3: Subordinators That Trigger SEE --- ============================================================================ - -/-- Subordinators that trigger super-extended ergativity in SJA Mam. -/ -inductive SEETrigger where - | tun -- *tu'n*: purpose/reason clauses - | taj -- *taj*: 'when' (past) - | aj -- *aj*: 'when' (future) - | chix -- *ch'ix*: 'almost' - | nim -- *ni'm*: 'right now' - | nanx -- *na'nx*: 'not yet' - deriving DecidableEq, Repr - -/-- All SEE triggers yield the same neutral alignment. -/ -def seeTriggerAlignment (_ : SEETrigger) : MamAlignment := seeAlignment - --- ============================================================================ --- § 4: Object Agreement Restriction in SEE --- ============================================================================ - -/-- In SEE clauses, object Set A markers are restricted to the default - 2/3SG form (t-). Agreeing Set A markers for the object are - ungrammatical. This parallels the default Set B (tz'=) pattern for - objects in matrix clauses. -/ -def objectSetAIsDefault : Bool := true - -/-- The parallel: in BOTH matrix and SEE, the object slot shows default - (non-agreeing) morphology. The default marker just changes: - - Matrix: default Set B (tz'=) - - SEE: default Set A (t-) -/ -theorem object_default_parallel : - objectSetAIsDefault = true := rfl - -end Scott2023