Satisfaction conditions: the Deal/Keine probe specification

[Dea24] [Kei19]

Standard Agree assumes a probe is satisfied only by finding a matching valued feature. [Dea24] argues for richer conditions — a probe can interact (halt) with more than satisfies it:

• Feature match: the standard case.
• Head encounter: probe halts on encountering a head of a category (e.g. Mam's Infl probe stopped by transitive Voice), copying no features → Elsewhere/default exponent.
• Disjunctive: halt on ANY of several conditions.

A SatisfactionCond is a probe specification in the sense of Probe/Basic.lean: it denotes a Probe α via SatisfactionCond.toProbe, with visibility = halting ([Dea24] interaction) and activity = feature copying ([Dea24] satisfaction). The interaction/satisfaction split is exactly the Probe.vis/Probe.act split — this file is where the substrate makes that identification (the previously study-local bridge in Studies/Scott2023.lean).

Main declarations

• SatisfactionCond — featureMatch / headEncounter / disjunctive.
• SatisfactionCond.isSatisfied, .copiedFeatures — halting and copying.
• SatisfactionCond.toProbe — the canonical specification-to-Probe map, generic over how a goal exposes its features and host category.

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). [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** ([scott-2023], via [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 [Dea24]'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.

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

@[implicit_reducible]

instance Minimalist.instReprSatisfactionCond : Repr SatisfactionCond

Equations

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

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.SatisfactionCond.toProbe {α : Type u_1} (cond : SatisfactionCond) (feats : α → FeatureBundle) (cat : α → Option Cat) : Probe α

The Probe a SatisfactionCond denotes, given how a goal exposes its features (feats) and host category (cat): visibility = halting (interaction), activity = feature copying (satisfaction).

Equations

• cond.toProbe feats cat = { vis := fun (a : α) => cond.isSatisfied (feats a) (cat a), act := fun (a : α) => cond.copiedFeatures (feats a) (cat a) }

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 (FeatureBundle.ofGramFeatures [GramFeature.valued (FeatureVal.phi (PhiFeature.person Person.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.singular))]) 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 (FeatureBundle.ofGramFeatures [GramFeature.valued (FeatureVal.phi (PhiFeature.person Person.first)), GramFeature.valued (FeatureVal.phi (PhiFeature.number Number.singular))]) none = true

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

theorem Minimalist.mamInflSatisfaction_isSatisfied (fb : FeatureBundle) (ctx : Option Cat) : mamInflSatisfaction.isSatisfied fb ctx = (hasValuedFeature fb (FeatureVal.phi (PhiFeature.person Person.third)) || ctx == some Cat.v)

Infl's satisfaction condition, unfolded: φ-match or Voice_TR encounter.

theorem Minimalist.mamInflSatisfaction_copiedFeatures (fb : FeatureBundle) (ctx : Option Cat) : mamInflSatisfaction.copiedFeatures fb ctx = hasValuedFeature fb (FeatureVal.phi (PhiFeature.person Person.third))

Head-encounter satisfaction never copies: Infl copies features iff they are there to copy, whatever the context.