Agree (Minimalist Feature Checking)

Formalization of Agree following @cite{chomsky-2000} and @cite{adger-2003}.

The Agree Operation

Agree is the mechanism by which features are checked/valued:

1. A probe (head with unvalued feature) searches its c-command domain
2. It finds the closest goal (element with matching valued feature)
3. The probe's feature is valued by copying from the goal
4. Both features are then checked (and may delete at PF/LF)

Architecture

This file contains the Agree operation and its structural conditions (locality, activity, phase-boundedness, defective intervention). For the feature types (PhiFeature, FeatureVal, etc.), see Features.lean. For the failure model (what happens when Agree fails), see ObligatoryOperations.lean. For the Case Filter, see CaseFilter.lean.

Satisfaction Conditions

Standard Agree assumes a probe is satisfied by finding a matching valued feature. @cite{deal-2024} and @cite{keine-2019} argue for richer conditions:

• Feature match: the standard case
• Head encounter: probe is satisfied by encountering a head of a particular category (e.g., Infl's probe stopped by transitive Voice)
• Disjunctive: probe is satisfied by ANY of several conditions

This captures e.g. Mam's Infl probe, which has satisfaction condition [SAT: φ or Voice_TR] — it stops when it finds either matching φ-features OR transitive Voice, whichever comes first.

structure Minimalist.ExtendedLI : Type

Extended LI with grammatical features

This extends Harizanov's LI with Agree-relevant features. The original ⟨CAT, SEL⟩ handles selection; this adds φ, Case, etc.

• base : LexicalItem
• features : FeatureBundle

@[implicit_reducible]

instance Minimalist.instReprExtendedLI : Repr ExtendedLI

Equations

• Minimalist.instReprExtendedLI = { reprPrec := Minimalist.instReprExtendedLI.repr }

def Minimalist.instReprExtendedLI.repr : ExtendedLI → ℕ → Std.Format

Equations

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

def Minimalist.ExtendedLI.fromSimple (cat : Cat) (sel : SelStack) (feats : FeatureBundle) : ExtendedLI

Create an extended LI from a simple LI

Equations

• Minimalist.ExtendedLI.fromSimple cat sel feats = { base := Minimalist.LexicalItem.simple cat sel, features := feats }

def Minimalist.ExtendedLI.isProbe (li : ExtendedLI) : Bool

Is this LI a probe (has unvalued features)?

Equations

• li.isProbe = List.any li.features Minimalist.GramFeature.isUnvalued

def Minimalist.ExtendedLI.isGoalFor (li : ExtendedLI) (ftype : FeatureVal) : Bool

Is this LI a potential goal for a given feature type?

Equations

• li.isGoalFor ftype = Minimalist.hasValuedFeature li.features ftype

structure Minimalist.AgreeRelation : Type

A probe-goal pair for Agree

• probe : SyntacticObject
• goal : SyntacticObject
• feature : FeatureVal
• probeFeatures : FeatureBundle
• goalFeatures : FeatureBundle

def Minimalist.AgreeRelation.probeCommands (a : AgreeRelation) (root : SyntacticObject) : Prop

The probe c-commands the goal within a given tree

Equations

• a.probeCommands root = Minimalist.cCommandsIn root a.probe a.goal

def Minimalist.AgreeRelation.goalHasFeature (a : AgreeRelation) : Bool

The goal has the relevant valued feature

Equations

• a.goalHasFeature = Minimalist.hasValuedFeature a.goalFeatures a.feature

def Minimalist.AgreeRelation.probeNeedsFeature (a : AgreeRelation) : Bool

The probe has the relevant unvalued feature

Equations

• a.probeNeedsFeature = Minimalist.hasUnvaluedFeature a.probeFeatures a.feature

def Minimalist.validAgree (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree: probe c-commands goal (in tree), probe has unvalued, goal has valued

Equations

• Minimalist.validAgree a root = (a.probeCommands root ∧ a.probeNeedsFeature = true ∧ a.goalHasFeature = true)

def Minimalist.intervenes (root probe x goal : SyntacticObject) (xFeatures : FeatureBundle) (ftype : FeatureVal) : Prop

X intervenes between probe and goal (within tree root) iff:

• probe c-commands X
• X c-commands goal
• X has a matching valued feature

Equations

• Minimalist.intervenes root probe x goal xFeatures ftype = (Minimalist.cCommandsIn root probe x ∧ Minimalist.cCommandsIn root x goal ∧ Minimalist.hasValuedFeature xFeatures ftype = true)

def Minimalist.closestGoal (a : AgreeRelation) (root : SyntacticObject) : Prop

Goal is the closest matching goal for probe.

Caveat: this definition existentially quantifies over feature bundles (∃ xFeats), meaning ANY structurally intervening node blocks regardless of its actual features. This is strictly stronger than necessary — a V° with no phi-features would block a phi-probe. For derivations that need to distinguish nodes by their actual features, use closestGoalWith (propositional, with feature assignment) or closestGoalB (boolean, with matching predicate).

Equations

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

@[reducible, inline]

abbrev Minimalist.FeatureAssignment : Type

A feature assignment maps each syntactic object in a tree to its actual feature bundle.

Equations

• Minimalist.FeatureAssignment = (Minimalist.SyntacticObject → Minimalist.FeatureBundle)

def Minimalist.closestGoalWith (a : AgreeRelation) (root : SyntacticObject) (fa : FeatureAssignment) : Prop

Goal is the closest matching goal for probe, given a feature assignment that determines each node's actual features.

Compared to closestGoal: the existential ∃ xFeats is replaced by fa x, so only nodes whose ACTUAL features match can intervene. This correctly models Agree: a V° (no phi-features) should not block T°'s phi-probe even if V° is structurally between T° and the subject DP. closestGoal is strictly stronger (see closestGoal_implies_closestGoalWith).

Equations

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

theorem Minimalist.closestGoal_implies_closestGoalWith (a : AgreeRelation) (root : SyntacticObject) (fa : FeatureAssignment) (h : closestGoal a root) : closestGoalWith a root fa

closestGoal (existential over features) implies closestGoalWith (fixed feature assignment): if no node with ANY features intervenes, then no node with its ACTUAL features intervenes.

def Minimalist.closestGoalB (root probe goal : SyntacticObject) (pred : SyntacticObject → Bool) : Bool

Boolean closest-goal check: is goal the closest node matching pred in probe's c-command domain within root?

This is the computational counterpart of closestGoalWith, using decidable cCommandsIn and a matching predicate. pred determines which nodes are potential goals/interveners — typically a category check (e.g., "is this node D-bearing?").

1. probe c-commands goal
2. goal matches the predicate
3. No other matching node is both c-commanded by probe AND c-commands goal (= no intervener)

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidableIsHorizonLeafFor (horizonCat : Cat) (n : SyntacticObject) : Decidable (Minimalist.isHorizonLeafFor✝ horizonCat n)

Equations

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

def Minimalist.behindHorizonB (root probe target : SyntacticObject) (horizonCat : Cat) : Bool

Is target behind a horizon of category horizonCat relative to probe in tree root?

A leaf head n of category horizonCat creates a horizon: its c-command domain is opaque to the probe. target is behind the horizon iff there exists a leaf n with category horizonCat such that:

1. probe c-commands n (n is in probe's search domain)
2. n c-commands target (target is in n's opaque domain)

This captures @cite{keine-2019}'s horizon mechanism: the probe cannot see past a head of the horizon category. Elements that are c-commanded by the horizon head are invisible to the probe.

Example: N° is a horizon for wh-probes (@cite{aissen-polian-2025}). In [DP D° [PossP Psr N°]], N° c-commands Psr (they are sisters), so wh-probes on C° cannot reach Psr. But D° is a sister of PossP, NOT c-commanded by N°, so the whole DP remains visible for pied-piping.

Equations

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

def Minimalist.valueFeature (unvalued valued : GramFeature) : Option GramFeature

Value an unvalued feature by copying from a valued one

Equations

• Minimalist.valueFeature (Minimalist.GramFeature.unvalued a) (Minimalist.GramFeature.valued v) = some (Minimalist.GramFeature.valued v)
• Minimalist.valueFeature unvalued valued = none

def Minimalist.applyAgree (probeFeats goalFeats : FeatureBundle) (ftype : FeatureVal) : Option FeatureBundle

Apply Agree: value the probe's feature from the goal. Uses sameType for matching, so a probe with [uPerson:_] will be valued by a goal with [Person:3rd] — the placeholder value is irrelevant, only the feature type matters.

Equations

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

structure Minimalist.TAgree : Type

T-Agree: T probes for φ-features on subject DP

T has [uφ], subject DP has [φ] → T gets valued φ. The .third value on person probes is a conventional placeholder — sameType ignores the specific PersonLevel value, matching any .person _ against any .person _.

• tHead : SyntacticObject
• subject : SyntacticObject
• tFeatures : FeatureBundle
• subjFeatures : FeatureBundle
• t_has_uphi : hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.person Features.Prominence.PersonLevel.third)) = true ∨ hasUnvaluedFeature self.tFeatures (FeatureVal.phi (PhiFeature.number Number.sg)) = true
• subj_has_phi : hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.person Features.Prominence.PersonLevel.third)) = true ∨ hasValuedFeature self.subjFeatures (FeatureVal.phi (PhiFeature.number Number.sg)) = true

structure Minimalist.CAgree : Type

C-Agree: C probes for [Q] feature

C has [uQ], interrogative element has [+Q] → question is licensed

• cHead : SyntacticObject
• qElement : SyntacticObject
• cFeatures : FeatureBundle
• qFeatures : FeatureBundle
• c_has_uq : hasUnvaluedFeature self.cFeatures (FeatureVal.q false) = true
• q_has_q : hasValuedFeature self.qFeatures (FeatureVal.q true) = true

def Minimalist.hasEPP (fb : FeatureBundle) : Bool

EPP triggers movement to specifier

When a head has [EPP], Agree is not enough - the goal must MOVE to the specifier position of the agreeing head.

Equations

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

def Minimalist.tToCTriggered (cFeats : FeatureBundle) : Bool

T-to-C movement is triggered by [uQ] + [EPP] on C

In matrix questions:

• C has [uQ, EPP]
• T has [+Q] (in some analyses) or movement satisfies EPP
• T moves to C (head movement)

Equations

• Minimalist.tToCTriggered cFeats = (Minimalist.hasUnvaluedFeature cFeats (Minimalist.FeatureVal.q false) && Minimalist.hasEPP cFeats)

def Minimalist.matrixCFeatures : FeatureBundle

Matrix C features: [uQ, EPP]

Equations

• Minimalist.matrixCFeatures = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.q false), Minimalist.GramFeature.valued (Minimalist.FeatureVal.epp true)]

def Minimalist.embeddedCFeatures : FeatureBundle

Embedded C features: [uQ] only (satisfied by wh-movement)

Equations

• Minimalist.embeddedCFeatures = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.q false)]

theorem Minimalist.matrix_triggers_t_to_c : tToCTriggered matrixCFeatures = true

Matrix C triggers T-to-C

theorem Minimalist.embedded_no_t_to_c : tToCTriggered embeddedCFeatures = false

Embedded C does not trigger T-to-C

def Minimalist.isActive (fb : FeatureBundle) : Bool

Is a feature bundle active? (has at least one unvalued feature)

An element is active iff it has at least one unvalued feature. Typically, DPs are active when they have unvalued Case.

Equations

• Minimalist.isActive fb = List.any fb Minimalist.GramFeature.isUnvalued

def Minimalist.needsCase (fb : FeatureBundle) : Bool

An element needs Case (has unvalued Case feature)

Equations

• Minimalist.needsCase fb = List.any fb fun (f : Minimalist.GramFeature) => f.isUnvalued && match f.featureType with | Minimalist.FeatureVal.case a => true | x => false

def Minimalist.hasCase (fb : FeatureBundle) : Bool

An element has valued Case

Equations

• Minimalist.hasCase fb = List.any fb fun (f : Minimalist.GramFeature) => f.isValued && match f.featureType with | Minimalist.FeatureVal.case a => true | x => false

theorem Minimalist.activity_via_case (fb : FeatureBundle) (h : (List.all fb fun (f : GramFeature) => match f.featureType with | FeatureVal.case a => true | x => false) = true) : isActive fb = true ↔ needsCase fb = true

Activity is typically determined by Case: A DP is active iff it lacks Case

When a feature bundle contains only Case features, the bundle is active (has unvalued features) iff it needs Case (has unvalued Case).

structure Minimalist.ActiveGoal : Type

A goal that satisfies the Activity Condition

• goal : SyntacticObject
• goalFeatures : FeatureBundle
• isActive : Minimalist.isActive self.goalFeatures = true

@[implicit_reducible]

instance Minimalist.instReprActiveGoal : Repr ActiveGoal

Equations

• Minimalist.instReprActiveGoal = { reprPrec := Minimalist.instReprActiveGoal.repr }

def Minimalist.instReprActiveGoal.repr : ActiveGoal → ℕ → Std.Format

Equations

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

def Minimalist.mkActiveGoal (goal : SyntacticObject) (feats : FeatureBundle) : Option ActiveGoal

Create an ActiveGoal if the features are indeed active

Equations

• Minimalist.mkActiveGoal goal feats = if h : Minimalist.isActive feats = true then some { goal := goal, goalFeatures := feats, isActive := h } else none

def Minimalist.validAgreeWithActivity (a : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Activity Condition

Agree requires:

1. Probe c-commands goal (within tree)
2. Probe has unvalued feature
3. Goal has matching valued feature
4. Goal is ACTIVE (has some unvalued feature)

Equations

• Minimalist.validAgreeWithActivity a root = (Minimalist.validAgree a root ∧ Minimalist.isActive a.goalFeatures = true)

structure Minimalist.MultipleAgree : Type

Multiple Agree: a probe agreeing with a list of goals

• probe : SyntacticObject
• probeFeatures : FeatureBundle
• goals : List (SyntacticObject × FeatureBundle)
• feature : FeatureVal
• goalsHaveFeature : (self.goals.all fun (x : SyntacticObject × FeatureBundle) => match x with | (fst, gf) => hasValuedFeature gf self.feature) = true

def Minimalist.instReprMultipleAgree.repr : MultipleAgree → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprMultipleAgree : Repr MultipleAgree

Equations

• Minimalist.instReprMultipleAgree = { reprPrec := Minimalist.instReprMultipleAgree.repr }

def Minimalist.MultipleAgree.isValid (ma : MultipleAgree) (root : SyntacticObject) : Prop

Is Multiple Agree valid? Each goal must be c-commanded by probe (within tree)

Equations

• ma.isValid root = (Minimalist.hasUnvaluedFeature ma.probeFeatures ma.feature = true ∧ ∀ g ∈ ma.goals, Minimalist.cCommandsIn root ma.probe g.1)

def Minimalist.applyMultipleAgree (ma : MultipleAgree) : Option FeatureBundle

Apply Multiple Agree: value probe's feature, mark all goals

Equations

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

structure Minimalist.DefectiveElement : Type

A defective element: has some matching features but incomplete set

• so : SyntacticObject
• features : FeatureBundle
• hasPartialPhi : (List.any self.features fun (f : GramFeature) => match f.featureType with | FeatureVal.phi a => true | x => false) = true
• isDeficient : Bool

def Minimalist.instReprDefectiveElement.repr : DefectiveElement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprDefectiveElement : Repr DefectiveElement

Equations

• Minimalist.instReprDefectiveElement = { reprPrec := Minimalist.instReprDefectiveElement.repr }

def Minimalist.defectivelyIntervenes (root probe x goal : SyntacticObject) (xDef : DefectiveElement) (ftype : FeatureVal) : Prop

Does X defectively intervene between probe and goal (within tree root)?

X defectively intervenes if:

• X is between probe and goal (c-command wise)
• X has matching features
• X is defective (can't be a full goal)

Equations

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

def Minimalist.validAgreeWithPIC (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

Valid Agree with Phase Impenetrability Condition.

Agree is blocked if the goal is inside a phase complement (and thus inaccessible under PIC). The strength parameter selects the PIC variant (PIC₁ vs PIC₂); see PICStrength. It is not yet consumed by phaseImpenetrable itself but is retained on the Agree-level interface so that derivational variants can wire it in without breaking call sites.

Equations

• Minimalist.validAgreeWithPIC strength phases rel root = (Minimalist.validAgree rel root ∧ ¬∃ ph ∈ phases, Minimalist.phaseImpenetrable ph.head rel.goal)

def Minimalist.fullAgree (strength : PICStrength) (phases : List Phase) (rel : AgreeRelation) (root : SyntacticObject) : Prop

PIC-bounded Agree with Activity Condition.

The full Agree constraint: probe c-commands goal, feature matching holds, goal is active, AND no intervening phase boundary blocks the relation. See validAgreeWithPIC for the role of strength.

Equations

• Minimalist.fullAgree strength phases rel root = (Minimalist.validAgreeWithActivity rel root ∧ ¬∃ ph ∈ phases, Minimalist.phaseImpenetrable ph.head rel.goal)

def Minimalist.finAgreeFeatures (isFinite : Bool) : FeatureBundle

Fin-Agree: Fin probes for [±finite] on its complement (TP).

Equations

• Minimalist.finAgreeFeatures isFinite = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.finite isFinite)]

def Minimalist.forceFinAgreeFeatures (isFactive : Bool) : FeatureBundle

Force-Fin-Agree: Force/C probes for clause-type features on Fin.

Equations

• Minimalist.forceFinAgreeFeatures isFactive = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.factive isFactive)]

def Minimalist.negAgreeFeatures : FeatureBundle

Neg-Agree: Neg probes for [±neg], licensing sentential negation.

Equations

• Minimalist.negAgreeFeatures = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.neg true)]

def Minimalist.relAgreeFeatures : FeatureBundle

Rel-Agree: Rel probes for [±rel], licensing relative clause formation.

Equations

• Minimalist.relAgreeFeatures = [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.rel true)]

theorem Minimalist.finite_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.finite true)) (GramFeature.valued (FeatureVal.finite true)) = true

Clause-typing features match correctly.

theorem Minimalist.factive_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.factive true)) (GramFeature.valued (FeatureVal.factive false)) = true

theorem Minimalist.neg_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.neg true)) (GramFeature.valued (FeatureVal.neg true)) = true

theorem Minimalist.rel_features_match : featuresMatch (GramFeature.unvalued (FeatureVal.rel true)) (GramFeature.valued (FeatureVal.rel false)) = true

inductive Minimalist.SatisfactionCond : Type

How a probe's search can be terminated.

Standard Agree assumes a probe is satisfied only by finding a matching
valued feature (simple feature match). @cite{deal-2024} argues for richer
conditions to capture e.g. Mam's Infl probe, which is satisfied by
EITHER matching φ-features OR encountering transitive Voice:

**Mam example** (@cite{scott-2023}, via @cite{deal-2024}):
- Infl carries [uφ] with satisfaction [SAT: φ or Voice_TR]
- Intransitive: probe passes through (no Voice_TR) → finds S → real φ-agreement
- Transitive: probe encounters Voice_TR → satisfied without copying φ → default "∅"

This turns the Mam bridge's prose account into a computable derivation:
```
def mamInflSatisfaction : SatisfactionCond :=

.disjunctive [.featureMatch (.phi (.person.third)),.headEncounter.v] ```

• featureMatch : FeatureVal → SatisfactionCond

  Standard: probe is satisfied by finding a matching valued feature.

• disjunctive : List SatisfactionCond → SatisfactionCond

  Disjunctive: probe is satisfied by ANY of these conditions. Models @cite{deal-2024}'s interaction-based probes.

• headEncounter : Cat → SatisfactionCond

  Head encounter: probe is satisfied by encountering a head of this category, even without feature matching. The probe stops but copies no features — yielding the Elsewhere (default) exponent at PF.

@[implicit_reducible]

instance Minimalist.instReprSatisfactionCond : Repr SatisfactionCond

Equations

• Minimalist.instReprSatisfactionCond = { reprPrec := Minimalist.instReprSatisfactionCond.repr }

partial def Minimalist.instReprSatisfactionCond.repr : SatisfactionCond → ℕ → Std.Format

def Minimalist.SatisfactionCond.isSatisfied (cond : SatisfactionCond) (fb : FeatureBundle) (ctx : Option Cat) : Bool

Check whether a satisfaction condition is met.

fb is the feature bundle of the element the probe encounters. ctx is the syntactic category of that element (if it's a head). Returns true if the probe should stop searching.

Equations

• (Minimalist.SatisfactionCond.featureMatch a).isSatisfied fb ctx = Minimalist.hasValuedFeature fb a
• (Minimalist.SatisfactionCond.disjunctive a).isSatisfied fb ctx = a.any fun (x : Minimalist.SatisfactionCond) => Minimalist.atomicSatisfied✝ x fb ctx
• (Minimalist.SatisfactionCond.headEncounter a).isSatisfied fb ctx = (ctx == some a)

def Minimalist.SatisfactionCond.copiedFeatures (cond : SatisfactionCond) (fb : FeatureBundle) (ctx : Option Cat) : Bool

Did the probe copy features, or just stop?

When satisfied by feature match, the probe copies features (→ real agreement). When satisfied by head encounter, no features are copied (→ default/Elsewhere). For disjunctive conditions, feature copying occurs iff the first satisfied condition is a feature match.

Equations

• One or more equations did not get rendered due to their size.
• (Minimalist.SatisfactionCond.featureMatch a).copiedFeatures fb ctx = Minimalist.hasValuedFeature fb a
• (Minimalist.SatisfactionCond.headEncounter a).copiedFeatures fb ctx = false

def Minimalist.mamInflSatisfaction : SatisfactionCond

Mam's Infl probe satisfaction condition: satisfied by EITHER matching φ-features OR encountering transitive Voice.

Equations

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

theorem Minimalist.mam_intransitive_satisfied : mamInflSatisfaction.isSatisfied [GramFeature.valued (FeatureVal.phi (PhiFeature.person Features.Prominence.PersonLevel.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.sg))] none = true

Intransitive environment: the probe encounters a DP with φ-features (no Voice_TR in the way). Feature match is satisfied → real agreement.

theorem Minimalist.mam_transitive_satisfied : mamInflSatisfaction.isSatisfied [] (some Cat.v) = true

Transitive environment: the probe encounters Voice_TR (category.v). Head encounter is satisfied → probe stops without copying features.

theorem Minimalist.mam_transitive_no_copy : mamInflSatisfaction.copiedFeatures [] (some Cat.v) = false

In the transitive case, no features are copied — yielding default.

theorem Minimalist.mam_intransitive_copies : mamInflSatisfaction.copiedFeatures [GramFeature.valued (FeatureVal.phi (PhiFeature.person Features.Prominence.PersonLevel.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.sg))] none = true

In the intransitive case, features ARE copied — yielding real agreement.