Documentation

Linglib.Studies.Scott2023

[Sco23] — Pronouns and Agreement in San Juan Atitán Mam #

[Sco23] [Woo97] [Mar91] [Bak15] [Cho00] [Dea24] [ETB26] [Pre14] [england-2017]

Single study file for [Sco23] (UC Berkeley dissertation), in three sections.

Voice-based case #

Scott treats case as assigned directly by functional heads keyed to argument position, building on [Woo97]'s claim that ergative is lexical/inherent Case assigned with θ-role rather than configurationally derived. Each case has a dedicated assigner:

This produces a tripartite underlying system (ERG ≠ ACC ≠ ABS) visible through the Mam agreement patterns. The Mam data discriminate between three theories of case assignment: Agree-based ([Cho00], [Cho01]: ACC requires a phase head), dependent case ([Mar91], [Bak15]: 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.

Agree-conditioned pronoun spellout #

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.

Super-extended ergativity #

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 ([Sco23], §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.

Voice-based case #

Scott 2023's central case-theoretic claim: Voice (and Infl) assign case directly based on argument position. A → ERG, P → ACC, S → ABS — three distinct cases from three different heads, with the assignment fixed by θ-position rather than by Agree or by NP configuration.

The three argument positions receive three distinct cases — a tripartite underlying system (ERG ≠ ACC ≠ ABS) at the case-assignment layer, prior to any morphological syncretism. Inherits from Alignment.tripartite_distinguishes_all via the substrate connection.

Agree-based case ties ACC to a phase head (v*). Voice flavors that are not phase heads (anticausative, passive) cannot assign ACC under this view, predicting a gap for unaccusative patients. Scott 2023's Voice-based assignment makes no such phase-head requirement.

Under Agree, anticausative Voice is not a phase head, so it cannot serve as an ACC assigner.

Under Agree, agentive Voice (v*) is a phase head and can assign ACC.

Dependent case is Voice-blind — the algorithm sees only NP configuration (higher vs. lower) and lexical case, not θ-role or Voice flavor. Two caseless NPs in a domain produce ACC on the lower one regardless of whether the higher NP is an agent or a derived subject. Scott's Voice-based assignment, by contrast, would only assign ACC under transitive Voice with an agent.

theorem Scott2023.dependent_case_ignores_voice :
have transitive := [{ label := "agent", lexicalCase := none }, { label := "theme", lexicalCase := none }]; have unaccusative := [{ label := "experiencer", lexicalCase := none }, { label := "theme", lexicalCase := none }]; Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative transitive) = Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative unaccusative)

Dependent case yields ACC for the lower of two caseless NPs whether or not the higher NP carries an agent θ-role. The algorithm never inspects Voice flavor.

theorem Scott2023.dependent_case_tripartite :
have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; Syntax.Case.getCaseOf "higher" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.tripartite nps) = some Case.erg Syntax.Case.getCaseOf "lower" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.tripartite nps) = some Case.acc

Dependent case in tripartite mode produces a parallel ERG/ACC split from the same configuration — but assigns it on positional grounds (higher NP gets ERG, lower NP gets ACC), not on θ-role grounds. Voice-based case derives the same surface pattern via a different mechanism, with the assigners keyed to θ-role rather than to NP configuration.

Agree-conditioned pronoun spellout #

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.

Set A (ERG) vocabulary entries: φ-features on Voice (.v) yield the morphological exponent ([Sco23] Table 2.8). All six cells have specific entries.

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

    Set B (ABS) vocabulary entries: φ-features on Infl (.T) yield the morphological exponent ([Sco23] 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.

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

      Voice's probe features: [uPerson, uNumber]. Placeholder values (.third, .Sing) are irrelevant — sameType matching ensures any Person/Number goal is found regardless.

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

        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.

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

          A 3SG DP's features: [Person:3, Number:sg].

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

            Full φ-valuation of Voice by a 3SG agent: both person and number valued.

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

              Set A spellout: Voice's valued [Person:3, Number:sg] yields "t-" (A2/3SG).

              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 Scott2023.setB_transitive_default :
              have inflBlocked := ; Minimalist.spellout setBVocab inflBlocked (some Minimalist.Cat.T) = some "tz'="

              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.

              The two paths produce the same exponent — the surface form is identical even though the underlying mechanism differs (real agreement vs. probe failure).

              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.

              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.

              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 halted by head-encounter satisfaction at transitive Voice ([Dea24]-style [SAT: φ or Voice_TR]; see the derived probe table below for the search-level statement).

              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.

              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

              The pipeline generalizes: for every argument position, reduction eligibility ≡ φ-agreement (definitionally — CanBeReduced := IsPhiAgreed).

              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.

              Set A vocabulary does NOT match Infl context.

              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.

              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).

              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.

              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, so its outcome is unvalued ([Pre14] Ch. 5). Under the obligatory-operations model this does not crash; the unvalued (empty) bundle spells out as the Elsewhere entry — the Set B "tz'=" observed in Mam transitives.

              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.

              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

              Deriving the probe table from relativized search (Probe/Basic.lean) #

              The agreeProbe table stipulates which head agrees with which position. Here it is DERIVED: each probe runs Probe.search over the goal sequence of its clause, relativized to its satisfaction condition. .P => none falls out of Voice_TR halting Infl's search before any DP (infl_truncated_at_voiceTR) plus Voice's own search stopping at the closer agent (voice_finds_A). The stipulation moves from the conclusion (the table) to independently motivated premises: mamInflSatisfaction (Agree.lean) and the clause spine's encounter order (Infl > Voice_TR > A > P). The goal lists are stipulated linearizations per clause type, not computed from a SyntacticObject — the tree-geometric derivation exists in Agree.lean but is native_decide-bound; this level matches Probing.lean's altitude.

              An element a probe encounters while walking its search domain: the argument position it realizes (none for non-DP heads like Voice_TR), its feature bundle, and its head category (none for DP goals). The (FeatureBundle, Option Cat) pair is exactly the argument signature of SatisfactionCond.isSatisfied.

              Instances For

                The probe a SatisfactionCond denotes over Encounters: the substrate's generic SatisfactionCond.toProbe (Probe/Satisfaction.lean) instantiated at the Encounter projections — visibility = halting ([Dea24] interaction), activity = feature copying (satisfaction).

                Equations
                Instances For

                  The argument position a probe φ-agrees with: (satProbe cond).agree — the probe agrees with the found element only if satisfaction copied features (feature match, not head encounter).

                  Equations
                  Instances For

                    Transitive Voice as an encounter: a head of category .v, no φ-features visible to the probe.

                    Equations
                    Instances For

                      A DP goal realizing position p with φ-bundle φ.

                      Equations
                      Instances For

                        A probe over an empty search space agrees with nothing.

                        Infl's goal sequence in the clause containing position p. In a transitive clause Infl c-commands VoiceP, so the FIRST element its downward search encounters is the Voice_TR head, before either DP. In an intransitive there is no transitive Voice; the search reaches S directly.

                        Equations
                        Instances For

                          The key derivation: Infl's search over ANY transitive goal sequence (Voice_TR first) yields no agreement target — by rfl, for arbitrary material below Voice. The search halts at Voice_TR (head encounter satisfies), no features are copied, so no DP is agreed with.

                          DERIVED probe table: which head φ-agrees with position p, computed by running each probe's Probe.search over the goal sequence of the clause containing p.

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

                            The stipulated table coincides with the derivation, for any clause whose A and S bear person features.

                            Concrete instantiation (3SG transitive + 3SG intransitive), kernel-checked end to end.

                            φ-valuation outcome of a probe with a satisfaction condition: valued iff the search found a goal AND satisfaction copied features. NOTE: this is NOT (satProbe cond).outcome — a head-encounter halt satisfies the search but leaves the probe φ-unvalued.

                            Equations
                            Instances For

                              Transitive Infl: search halts at Voice_TR, probe stays unvalued, and converges with Elsewhere morphology — the §11 facts, now derived from the goal sequence rather than from a stipulated empty bundle.

                              Contrast: Probe.outcome relativized to the satisfaction condition reports .valued in the transitive — the search DID find a halting element. The valuation/satisfaction distinction is exactly [Dea24]'s interaction-vs-satisfaction split.

                              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.

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

                                Mam's rule is paradigmatic — discharged by the smart constructor.

                                Super-extended ergativity #

                                The Mam alignment in a given clause type.

                                Instances For
                                  def Scott2023.instDecidableEqMamAlignment.decEq (x✝ x✝¹ : MamAlignment) :
                                  Decidable (x✝ = x✝¹)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Matrix clause alignment: tripartite. S = Set B (ABS), A = Set A (ERG), O = default Set B (no agreement).

                                      Equations
                                      Instances For

                                        Super-extended ergative alignment: neutral (all Set A).

                                        Equations
                                        Instances For

                                          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).

                                          SEE alignment is neutral: all arguments get the same marker set.

                                          A is invariant across the split: Set A in both matrix and SEE.

                                          Subordinators that trigger super-extended ergativity in SJA Mam.

                                          Instances For
                                            @[implicit_reducible]
                                            Equations
                                            def Scott2023.instReprSEETrigger.repr :
                                            SEETriggerStd.Format
                                            Equations
                                            Instances For

                                              All SEE triggers yield the same neutral alignment.

                                              Equations
                                              Instances For

                                                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.

                                                Equations
                                                Instances For

                                                  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-)