Preminger 2014 — Agreement and Its Failures [Pre14]

[BR03] [HM93] [HR02] [Nev11] [Sti06] [Hal12]

[Pre14], Agreement and Its Failures (MIT Press, LI Monographs 68), applies [BR03]'s split-probe system and Person Licensing Condition — with relativized probing, Preminger's own addition (§4.2) — to the Kichean Agent Focus construction (Ch. 4) and uses the resulting failure cases to argue for an "obligatory operations" model of φ-Agree (Ch. 5). The fragment in Fragments/Mayan/Kaqchikel/Agreement.lean carries the theory-neutral data; this file adds the analytical apparatus. Section and example numbers below were verified against the monograph manuscript; page numbers are omitted (draft and published pagination differ).

Attribution discipline

Per Preminger's own framing:

• The feature geometry [φ] → [PERSON] → [participant] → [author] traces to [HR02]; [Pre14] adopts a simplified version.
• The split π/# probes (person probing first) and the Person Licensing Condition (PLC) are [BR03]'s (§4.1, §4.4). Relativized probing is Preminger's own addition (§4.2, recalling [Riz90]) — B&R's π-probe is explicitly NOT relativized (see Studies/BejarRezac2003.lean and ch4_relativization_contrast). The separate-heads implementation (π⁰ merged below #⁰, probing first; B&R put both probes on one head) is also Preminger's; what surfaces is decided by a single morphological slot in which a clitic beats out the exponence of π⁰/#⁰.
• Omnivorous agreement as the name for the surface pattern is [Nev11]'s term, which Preminger adopts.
• DM Vocabulary insertion for setAVocab/setBVocab follows [HM93]. The Elsewhere ∅ entry is this formalization's DM rendering: Preminger's own statement is that the absolutive paradigm has no overt 3rd-person-singular exponence, so failed probing leaves the slot empty.
• What is distinctively Preminger 2014: relativizing π⁰ to [participant] and #⁰ to [plural] for Kichean AF (Ch. 4); the "obligatory operations" model of φ-Agree (Ch. 5) — φ-Agree is obligatory but failure-tolerant, with failed Agree surfacing as default morphology rather than crashing the derivation; and the Ch. 7 case against salience-hierarchy primitives (the Mayanist hierarchy tradition: Dayley, Smith-Stark, Norman & Campbell, Mondloch; and constraint-based recastings such as [Sti06]).

Two-probe relativized probing

§4.4 derives the Kichean AF agreement target from two independently relativized probes:

• π⁰ seeks [participant]: targets 1st/2nd person DPs, skips 3rd.
• #⁰ seeks [plural]: targets plural DPs, skips singulars.

The single AF marker reflects π⁰'s output if it succeeds (clitic doubling of the [participant]-bearing argument); otherwise #⁰'s output (the 3PL marker e- by direct exponence); otherwise the slot is empty (∅). This slot competition is Probe.cascade over the two probes, definitionally: afAgreementTarget IS the cascade, the ∅ row is failed Agree realized by the DM Elsewhere entry, and the rank comparison is the derived form (afAgreementTarget_eq_rank). There is no salience scale, and personRestrictionOk_iff_plc derives the person restriction from the PLC via Probe/Phi.lean's search-licensing substrate.

Why not a hierarchy

A surface-equivalent hierarchy [+participant] > [+plural] > default would predict the same outputs on the table-(22) cells, but Ch. 7 gives five arguments against hierarchy accounts:

1. Restrictedness (§7.1): "salience" effects surface nowhere else in the language (prose only — needs regular-transitive data).
2. K'ichee' formal addressee la: a 2nd-person pronoun that is morphosyntactically 3rd person under AF, contrary to 2 ≫ 3 (prose only — needs a K'ichee' fragment).
3. Co-occurrence asymmetry: a hierarchy is silent on co-occurrence — nothing about it explains why two 1st/2nd-person arguments cannot co-occur while two 3rd-plurals can. The two-probe + PLC account derives both the agreement pattern and the restriction; the hierarchy derives only the former (ch7_arg3_participant_vs_plural_asymmetry).
4. Morphophonology of the markers ("perhaps strongest" per §7.1; the morphophonology is detailed in §3.4): 1st/2nd ABS markers stand in the relation <agreement marker> = <strong pronoun> − <initial approximant> (149) — a clitic-doubling signature that 3rd-person markers lack (smoke check only — the fragment lacks strong-pronoun forms).
5. Zulu parallel (§7.2): [Hal12]'s analysis of Zulu augmentless nominals uses the same machinery over augmented/augmentless — categories with no plausible "salience" reading (ch7_arg5_zulu_parallel, via Studies/Halpert2012.lean).

Cross-references

• Syntax/Minimalist/Phi/Geometry.lean — decomposePerson, probeVisible, probeResolutionRank.
• Syntax/Minimalist/Probe/Basic.lean — Probe, Probe.Licensed, Probe.outcome/Probe.Outcome (the Ch. 5 valued/unvalued result of an obligatory probe); Probe/Phi.lean — PLC: the search-and-licensing layer the derivations below consume. Failed Agree = an unvalued probe outcome that is tolerated (no crash) and spells out as the Elsewhere entry.
• Morphology/DM/VocabSimple.lean — Vocabulary, Agreement.Cell.toPhiFeatures, makePersonVocab, spellout.
• Studies/Scott2023.lean — the same DM/Agree machinery applied to Mam (where Infl's φ-probe is blocked in transitives).
• Studies/CoonMateoPedroPreminger2014.lean — Voice/case-flavor side of the same author cluster's Mayan work.

Feature decomposition (grounded in Phi/Geometry.lean)

def Preminger2014.IsParticipant (c : Agreement.Cell) : Prop

Bears [+participant]? Visibility to π⁰ under relativized probing ([BR03] via Agreement.Cell.visibleTo); derives from [HR02]'s feature geometry through decomposePerson.

Equations

• Preminger2014.IsParticipant c = (c.visibleTo Minimalist.Probe.Target.participant = true)

@[implicit_reducible]

instance Preminger2014.instDecidablePredCellIsParticipant : DecidablePred IsParticipant

Equations

• Preminger2014.instDecidablePredCellIsParticipant c = Preminger2014.instDecidablePredCellIsParticipant._aux_1 c

def Preminger2014.IsAuthor (c : Agreement.Cell) : Prop

Bears [+author]?

Equations

• Preminger2014.IsAuthor c = ((Minimalist.decomposePerson c.toPerson).hasAuthor = true)

@[implicit_reducible]

instance Preminger2014.instDecidablePredCellIsAuthor : DecidablePred IsAuthor

Equations

• Preminger2014.instDecidablePredCellIsAuthor c = Preminger2014.instDecidablePredCellIsAuthor._aux_1 c

theorem Preminger2014.isParticipant_of_isAuthor (c : Agreement.Cell) : IsAuthor c → IsParticipant c

[author] entails [participant]: the [HR02] geometric containment, inherited from decomposePerson.

DM Vocabulary insertion ([HM93])

def Preminger2014.setAVocab : Minimalist.Vocabulary

Set A as DM Vocabulary entries, contextualized to Voice/v. All six cells have overt exponents.

Equations

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

def Preminger2014.setBVocab : Minimalist.Vocabulary

Set B as DM Vocabulary entries, contextualized to Infl/T: specific entries for the five overt cells, plus the Elsewhere ∅ entry realizing 3SG and failed agreement (see the module docstring on this DM rendering vs. Preminger's own formulation).

Equations

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

theorem Preminger2014.spellout_matches_paradigm (c : Agreement.Cell) : c ∈ Agreement.Cell.pnCells → Minimalist.spellout setAVocab (Preminger2014.cellBundle✝ c) (some Minimalist.Cat.v) = Agreement.Paradigm.realize Kaqchikel.setAExponent c ∧ Minimalist.spellout setBVocab (Preminger2014.cellBundle✝ c) (some Minimalist.Cat.T) = Agreement.Paradigm.realize Kaqchikel.setBExponent c

Vocabulary insertion recovers the fragment's paradigms: spelling out each cell's valued bundle yields the fragment's exponent — for Set B, the 3SG cell via the Elsewhere entry, the rest via their specific entries.

Two-probe relativized probing ([BR03], applied per §4.4)

def Preminger2014.afRank (c : Agreement.Cell) : ℕ

Probe-resolution rank for a Kaqchikel person-number cell under the two-probe (π⁰ before #⁰) system. Computed via probeResolutionRank on the cell's person + number features. NOT a salience scale — afAgreementTarget_eq_rank derives the rank comparison from the probe cascade.

Equations

• Preminger2014.afRank c = Minimalist.probeResolutionRank c.toPerson c.isPlural

def Preminger2014.PersonRestrictionOk (subj obj : Agreement.Cell) : Prop

Person restriction ([Pre14] (25)): at most one core argument can bear [+participant]. The empirical generalization; it DERIVES from the Person Licensing Condition — see personRestrictionOk_iff_plc. This is the syntactic licensing story, not the morphological clitic-slot competition.

Equations

• Preminger2014.PersonRestrictionOk subj obj = ¬(Preminger2014.IsParticipant subj ∧ Preminger2014.IsParticipant obj)

@[implicit_reducible]

instance Preminger2014.instDecidableRelCellPersonRestrictionOk : DecidableRel PersonRestrictionOk

Equations

• Preminger2014.instDecidableRelCellPersonRestrictionOk subj obj = Preminger2014.instDecidableRelCellPersonRestrictionOk._aux_1 subj obj

theorem Preminger2014.personRestrictionOk_iff_plc (s o : Agreement.Cell) : PersonRestrictionOk s o ↔ Minimalist.PLC Prod.snd [(Features.Prominence.ArgumentRole.A, s), (Features.Prominence.ArgumentRole.P, o)]

The person restriction derives from the PLC ([BR03]; [Pre14] §4.4 (75)): with the AF clause's agent and patient as π⁰'s goal tokens, the PLC holds iff at most one bears [+participant]. A [+participant] argument requires an Agree relation with π⁰ to be licensed; π⁰'s single search licenses at most one token (Probe.allLicensed_iff), so two [+participant] arguments cannot both be licensed and the derivation crashes.

theorem Preminger2014.ch4_relativization_contrast : ¬BejarRezac2003.PLCOk [[{ person := Person.third, fLicensed := true }, { person := Person.first, fLicensed := false }]] [{ person := Person.third, fLicensed := true }, { person := Person.first, fLicensed := false }] ∧ Minimalist.PLC Prod.snd [(Features.Prominence.ArgumentRole.A, Agreement.Cell.pn UD.Person.third UD.Number.Sing), (Features.Prominence.ArgumentRole.P, Agreement.Cell.pn UD.Person.first UD.Number.Sing)]

[Pre14] Ch. 4's move (§4.2), made formal: [BR03]'s ⊤-visible π-probe is absorbed by an F-licensed 3rd-person dative, stranding a participant below it — the PCC. The Kichean π⁰, relativized to [participant], skips the same 3rd-person goal and licenses the lower participant. Relativization to exactly the licensing-needy class is what converts absorption into omnivorous licensing.

def Preminger2014.piProbe : Minimalist.Probe Agreement.Cell

π⁰: the person probe — the denotation of the substrate's Probe.Target.participant specification.

Equations

• Preminger2014.piProbe = Minimalist.Probe.Target.participant.toProbe

def Preminger2014.numProbe : Minimalist.Probe Agreement.Cell

#⁰: the number probe — the denotation of Probe.Target.plural.

Equations

• Preminger2014.numProbe = Minimalist.Probe.Target.plural.toProbe

def Preminger2014.afProbes : List (Minimalist.Probe Agreement.Cell)

The two AF probes in slot order: π⁰'s clitic output beats #⁰'s direct exponence in the single morphological slot ([Pre14] §4.4).

Equations

• Preminger2014.afProbes = [Preminger2014.piProbe, Preminger2014.numProbe]

def Preminger2014.afAgreementTarget (subj obj : Agreement.Cell) : Option Agreement.Cell

The AF agreement target, by probe cascade: π⁰'s goal if it finds one, else #⁰'s, else none — both probes failed (3SG × 3SG) and the slot stays empty. Pure Agree: grammaticality (the PLC) is checked at afMarker. When both arguments are visible to the winning probe it takes the closer one (the subject) — immaterial for the marker (afMarker_comm).

Equations

• Preminger2014.afAgreementTarget subj obj = Minimalist.Probe.cascade Preminger2014.afProbes [subj, obj]

def Preminger2014.afMarker (subj obj : Agreement.Cell) : Option String

The AF agreement marker: the Set B exponent of the cascade's target; the Elsewhere ∅ via DM insertion from the unvalued bundle when both probes failed; none (ungrammatical) when the PLC fails on the clause's goal tokens (equivalently, when the surface person restriction is violated: personRestrictionOk_iff_plc).

Equations

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

theorem Preminger2014.afAgreementTarget_eq_rank (s : Agreement.Cell) : s ∈ Agreement.Cell.pnCells → ∀ o ∈ Agreement.Cell.pnCells, afAgreementTarget s o = if afRank s = 0 ∧ afRank o = 0 then none else if afRank s ≥ afRank o then some s else some o

The rank encoding (probeResolutionRank, [BR03] convenience form) is derived from the cascade: on the φ-cell inventory the cascade's target is the higher-ranked argument — except that double rank-0 (both probes fail) is an honest none rather than a default target.

Verification: grounding in Phi.Geometry

theorem Preminger2014.feature_decomposition_cells : IsParticipant (Agreement.Cell.pn UD.Person.first UD.Number.Sing) ∧ IsParticipant (Agreement.Cell.pn UD.Person.second UD.Number.Sing) ∧ ¬IsParticipant (Agreement.Cell.pn UD.Person.third UD.Number.Sing) ∧ ¬IsParticipant (Agreement.Cell.pn UD.Person.third UD.Number.Plur) ∧ afRank (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = 2 ∧ afRank (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = 2 ∧ afRank (Agreement.Cell.pn UD.Person.third UD.Number.Plur) = 1 ∧ afRank (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = 0

Smoke check: feature decomposition and probe ranks on the key cells match the [HR02] + [BR03] expectations — [+participant] → rank 2, [+plural, −participant] → rank 1, 3SG → rank 0.

Verification: AF paradigm ([Pre14] table (22))

theorem Preminger2014.af_paradigm_correct (d : Kaqchikel.AFAgreementDatum) : d ∈ Kaqchikel.afParadigm → afMarker d.subject d.object = d.marker

The full AF paradigm (table (22)) is correctly predicted: each empirical datum in the fragment's afParadigm matches afMarker.

theorem Preminger2014.afMarker_comm (s : Agreement.Cell) : s ∈ Agreement.Cell.pnCells → ∀ o ∈ Agreement.Cell.pnCells, afMarker s o = afMarker o s

AF agreement is commutative: swapping subject and object yields the same marker (empirical statement: §3.2, table (22), which pools subject/object φ as unordered sets; derived as a prediction of the clitic-doubling account in §4.4, representative pair (67a–b)). Of the 36 ordered pairs, the 11 unordered cells of table (22) are empirical; pairs of two participants are unattestable for independent binding-theoretic reasons and are vacuously symmetric (both orders yield none).

theorem Preminger2014.participant_over_plural : afMarker (Agreement.Cell.pn UD.Person.first UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Plur) = some "in-" ∧ afMarker (Agreement.Cell.pn UD.Person.third UD.Number.Plur) (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = some "at-"

π⁰ output suppresses #⁰ when both have a target: when one argument is 1st/2nd and the other is 3PL, the marker reflects the participant (clitic-doubling output of π⁰), not the plural.

theorem Preminger2014.restriction_and_default : afMarker (Agreement.Cell.pn UD.Person.first UD.Number.Sing) (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = none ∧ afMarker (Agreement.Cell.pn UD.Person.second UD.Number.Sing) (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = none ∧ afMarker (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some "∅"

PLC violation: two [+participant] arguments are blocked, in either order. Both arguments 3SG: both probes fail to find a target (afAgreementTarget is none) and ∅ surfaces from the Elsewhere entry (see failed_agree_tolerated for the Ch. 5 reading).

theorem Preminger2014.personRestrictionOk_comm (s o : Agreement.Cell) : PersonRestrictionOk s o ↔ PersonRestrictionOk o s

The person restriction is symmetric.

Obligatory operations ([Pre14] Ch. 5)

def Preminger2014.piOutcome (subj obj : Agreement.Cell) : Minimalist.Probe.Outcome

π⁰'s outcome on the AF clause's goal pair: each probe is independently obligatory ([Pre14] Ch. 5).

Equations

• Preminger2014.piOutcome subj obj = Preminger2014.piProbe.outcome [subj, obj]

def Preminger2014.numOutcome (subj obj : Agreement.Cell) : Minimalist.Probe.Outcome

#⁰'s outcome on the AF clause's goal pair.

Equations

• Preminger2014.numOutcome subj obj = Preminger2014.numProbe.outcome [subj, obj]

def Preminger2014.afProbe.Outcome (subj obj : Agreement.Cell) : Minimalist.Probe.Outcome

Joint outcome of the AF probes: unvalued only when both probes fail (i.e., both arguments are 3SG).

Equations

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

theorem Preminger2014.afAgreementTarget_eq_none_iff (subj obj : Agreement.Cell) : afAgreementTarget subj obj = none ↔ afProbe.Outcome subj obj = Minimalist.Probe.Outcome.unvalued

The cascade comes back empty exactly when the joint probe outcome is unvalued — Agree-level failure and outcome-level failure are the same fact, for arbitrary φ-cells.

theorem Preminger2014.failed_agree_tolerated : afAgreementTarget (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = none ∧ piOutcome (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = Minimalist.Probe.Outcome.unvalued ∧ numOutcome (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = Minimalist.Probe.Outcome.unvalued ∧ afProbe.Outcome (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = Minimalist.Probe.Outcome.unvalued ∧ Minimalist.spellout setBVocab ⊥ (some Minimalist.Cat.T) = some "∅" ∧ afMarker (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some "∅"

Failed Agree is tolerated, not crashing ([Pre14] Ch. 5): when both probes find no goal (3SG × 3SG), each probe ends unvalued, the derivation converges under the obligatory-operations model, PF realizes the Elsewhere entry, and the observed marker is ∅ — recovered by Vocabulary insertion from the unvalued (empty) bundle. Contrast the PLC case in restriction_and_default: failed licensing crashes (none); failed Agree does not.

Verification: Ch. 7 anti-hierarchy arguments (3 of 5)

theorem Preminger2014.ch7_arg3_participant_vs_plural_asymmetry : afMarker (Agreement.Cell.pn UD.Person.first UD.Number.Sing) (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = none ∧ afMarker (Agreement.Cell.pn UD.Person.third UD.Number.Plur) (Agreement.Cell.pn UD.Person.third UD.Number.Plur) = some "e-"

[Pre14] Ch. 7 arg 3: a salience hierarchy [+participant] > [+plural] > default is silent on co-occurrence — nothing about it explains why two 1st/2nd-person arguments cannot co-occur while two 3rd plurals can. The two-probe + PLC analysis derives both: π⁰ targets [participant] under the PLC (single Agree relation → restriction); #⁰ targets [plural] with no parallel licensing condition (no competition for 3PL + 3PL).

theorem Preminger2014.ch7_arg4_form_distinctness (c : Agreement.Cell) : c ∈ [Agreement.Cell.pn UD.Person.first UD.Number.Sing, Agreement.Cell.pn UD.Person.second UD.Number.Sing, Agreement.Cell.pn UD.Person.first UD.Number.Plur, Agreement.Cell.pn UD.Person.second UD.Number.Plur] → Agreement.Paradigm.realize Kaqchikel.setBExponent c ≠ Agreement.Paradigm.realize Kaqchikel.setBExponent (Agreement.Cell.pn UD.Person.third UD.Number.Plur) ∧ Agreement.Paradigm.realize Kaqchikel.setBExponent c ≠ Agreement.Paradigm.realize Kaqchikel.setBExponent (Agreement.Cell.pn UD.Person.third UD.Number.Sing)

[Pre14] Ch. 7 arg 4 smoke check (§3.4, table (148), relation (149)): 1st/2nd ABS markers stand in the relation <agreement marker> = <strong pronoun> − <initial approximant> (e.g., 1sg i(n)- from yïn, 1pl oj- from röj; the observation traces to Kaufman 1977). 3rd-person markers lack this property — pointing to clitic doubling for 1st/2nd vs. direct exponence for 3rd.

UNVERIFIED: this theorem only checks that 1st/2nd ABS markers are distinct in form from the 3rd-person ones, which is necessary but not sufficient for arg 4. The genuine relation (149) requires strong-pronoun forms (yïn, rat, röj, rïx, rja', rje') which the fragment does not currently carry. A faithful arg-4 theorem awaits extending the fragment with strong pronouns and a suffix-stripping bridge function.

theorem Preminger2014.ch7_arg5_zulu_parallel : Minimalist.PLC Prod.snd [(Features.Prominence.ArgumentRole.A, Agreement.Cell.pn UD.Person.third UD.Number.Sing), (Features.Prominence.ArgumentRole.P, Agreement.Cell.pn UD.Person.first UD.Number.Sing)] ∧ ¬Halpert2012.LicensingOk [{ nounClass := 1, augmented := true }, { nounClass := 5, augmented := false }] ∧ afMarker (Agreement.Cell.pn UD.Person.third UD.Number.Sing) (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some "∅" ∧ Halpert2012.lSpellout [] = "ya-"

[Pre14] Ch. 7 arg 5 (§7.2, via Ch. 6): [Hal12]'s Zulu runs the same search-and-licensing substrate over a salience-irrelevant contrast. Kichean is the diagonal instance (diagonal Probe.AllLicensed: π⁰ relativized to exactly the licensing-needy [participant] cells), so a needy argument is licensed even from object position — the probe skips non-bearers. Zulu's L⁰ is the off-diagonal instance (Probe.indiscriminate: indiscriminate probe, augmentless = needy), so an augmented subject intervenes and a lower augmentless nominal goes unlicensed. Same machinery, opposite skippability — and there is little plausible salience grounding for augmented/augmentless, a contrast sensitive to purely structural relations such as c-command, undermining the cognitive-salience grounding of hierarchy accounts. Both systems realize failed probing as default morphology (Kichean covert ∅, Zulu overt ya-).