Obligatory Operations @cite{preminger-2014}

@cite{chomsky-2001}

@cite{preminger-2014} argues that φ-agreement is an obligatory operation that can fail without crashing the derivation. This contrasts with the standard Minimalist view where unvalued features at the interfaces cause the derivation to crash.

The Standard Model

Probes carry uninterpretable/unvalued features ([uφ]). If [uφ] reaches the interfaces (PF/LF) without being valued by Agree, the derivation crashes. This makes agreement effectively obligatory AND success- mandatory: any probe must find a matching goal, or the structure is ungrammatical.

Preminger's Alternative

Agreement is obligatory — the grammar MUST attempt it — but failure does NOT crash the derivation:

• At PF: unvalued features receive the Elsewhere exponent (3SG ∅)
• At LF: unvalued features make no semantic contribution (vacuous)
• The derivation converges either way

The key distinction: obligatoriness (the probe must search) vs. crash-on-failure (failure to find a goal is fatal). Standard Minimalism conflates these; Preminger separates them.

The Derivational Time-Bomb Argument (Ch. 5)

Derivational time-bombs (uninterpretable features that cause crash at the interface) cannot model obligatory-but-failable agreement because:

1. A time-bomb ([uF]) detonates at the interface if unvalued
2. The system cannot distinguish "probe attempted and failed" from "probe was never present"
3. But obligatoriness requires this distinction: a probe that tried and failed should produce default morphology, while a probe that was never there should produce no morphology

Empirical Evidence

• Kichean AF: omnivorous agreement targets whichever argument bears the sought feature. If neither does, the default (3SG ∅) surfaces — the probe failed without crashing.
• Dative intervention: a dative DP blocks the probe but cannot be a valid goal (wrong case). The probe fails → default agreement.
• Icelandic quirky subjects: dative subject intervenes between T and the nominative object → T's probe fails → default 3SG.

All three are instances of the same mechanism: obligatory probing + failure without crash → default morphology.

inductive Minimalism.AgreementModel : Type

Two models of what happens when a probe fails to find a matching goal.

• crashOnFailure: the standard Minimalist model. Unvalued features at the interfaces cause the derivation to crash. Agreement is both obligatory and success-mandatory.
• obligatoryNocrash: Preminger's model. Agreement is obligatory (the probe must attempt to Agree), but failure to find a goal does NOT crash — default morphology surfaces instead.

• crashOnFailure : AgreementModel

  Standard: unvalued features at interface → crash.

• obligatoryNocrash : AgreementModel

  Preminger: obligatory but failure → default, no crash.

instance Minimalism.instDecidableEqAgreementModel : DecidableEq AgreementModel

Equations

• Minimalism.instDecidableEqAgreementModel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instBEqAgreementModel : BEq AgreementModel

Equations

• Minimalism.instBEqAgreementModel = { beq := Minimalism.instBEqAgreementModel.beq }

def Minimalism.instBEqAgreementModel.beq : AgreementModel → AgreementModel → Bool

Equations

• Minimalism.instBEqAgreementModel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instReprAgreementModel : Repr AgreementModel

Equations

• Minimalism.instReprAgreementModel = { reprPrec := Minimalism.instReprAgreementModel.repr }

def Minimalism.instReprAgreementModel.repr : AgreementModel → ℕ → Std.Format

Equations

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

inductive Minimalism.ProbeOutcome : Type

The outcome of an obligatory probing operation.

• valued: the probe found a goal and was valued by its φ-features.
• unvalued: the probe attempted but found no suitable goal. In the crash model, this crashes. In the obligatory-no-crash model, the derivation continues with default morphology.

• valued : ProbeOutcome

  Probe successfully agreed with a goal.

• unvalued : ProbeOutcome

  Probe attempted but found no suitable goal.

instance Minimalism.instDecidableEqProbeOutcome : DecidableEq ProbeOutcome

Equations

• Minimalism.instDecidableEqProbeOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instBEqProbeOutcome : BEq ProbeOutcome

Equations

• Minimalism.instBEqProbeOutcome = { beq := Minimalism.instBEqProbeOutcome.beq }

def Minimalism.instBEqProbeOutcome.beq : ProbeOutcome → ProbeOutcome → Bool

Equations

• Minimalism.instBEqProbeOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instReprProbeOutcome : Repr ProbeOutcome

Equations

• Minimalism.instReprProbeOutcome = { reprPrec := Minimalism.instReprProbeOutcome.repr }

def Minimalism.instReprProbeOutcome.repr : ProbeOutcome → ℕ → Std.Format

Equations

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

def Minimalism.derivationConverges (model : AgreementModel) (outcome : ProbeOutcome) : Bool

Does the derivation converge given a probe outcome? In the crash model: only if the probe was valued. In the obligatory-no-crash model: always.

Equations

• Minimalism.derivationConverges Minimalism.AgreementModel.crashOnFailure Minimalism.ProbeOutcome.unvalued = false
• Minimalism.derivationConverges model outcome = true

def Minimalism.ProbeOutcome.yieldsDefault : ProbeOutcome → Bool

Does this outcome yield default morphology? Only unvalued probes produce the default (Elsewhere entry).

Equations

• Minimalism.ProbeOutcome.valued.yieldsDefault = false
• Minimalism.ProbeOutcome.unvalued.yieldsDefault = true

inductive Minimalism.PFRealization : Type

What surfaces at PF for a given probe outcome.

• Valued probe: agreement morphology reflecting the goal's features.
• Unvalued probe: the Elsewhere entry (3SG ∅ in Kaqchikel).

In the crash model, the unvalued case never reaches PF (the derivation crashes first). In Preminger's model, it does, and the Elsewhere entry surfaces.

• agreement : PFRealization

  Agreement morphology reflecting the valued features.

• elsewhere : PFRealization

  Default/Elsewhere morphology (3SG ∅ in Kichean).

instance Minimalism.instDecidableEqPFRealization : DecidableEq PFRealization

Equations

• Minimalism.instDecidableEqPFRealization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instBEqPFRealization.beq : PFRealization → PFRealization → Bool

Equations

• Minimalism.instBEqPFRealization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqPFRealization : BEq PFRealization

Equations

• Minimalism.instBEqPFRealization = { beq := Minimalism.instBEqPFRealization.beq }

def Minimalism.instReprPFRealization.repr : PFRealization → ℕ → Std.Format

Equations

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

instance Minimalism.instReprPFRealization : Repr PFRealization

Equations

• Minimalism.instReprPFRealization = { reprPrec := Minimalism.instReprPFRealization.repr }

def Minimalism.ProbeOutcome.pfRealization : ProbeOutcome → PFRealization

Map a probe outcome to its PF realization.

Equations

• Minimalism.ProbeOutcome.valued.pfRealization = Minimalism.PFRealization.agreement
• Minimalism.ProbeOutcome.unvalued.pfRealization = Minimalism.PFRealization.elsewhere

theorem Minimalism.models_agree_on_success : derivationConverges AgreementModel.crashOnFailure ProbeOutcome.valued = true ∧ derivationConverges AgreementModel.obligatoryNocrash ProbeOutcome.valued = true

The two models agree when the probe succeeds: both converge.

theorem Minimalism.models_diverge_on_failure : derivationConverges AgreementModel.crashOnFailure ProbeOutcome.unvalued = false ∧ derivationConverges AgreementModel.obligatoryNocrash ProbeOutcome.unvalued = true

The two models diverge when the probe fails: the crash model does not converge, but the obligatory-no-crash model does.

theorem Minimalism.crash_requires_success (outcome : ProbeOutcome) : derivationConverges AgreementModel.crashOnFailure outcome = true ↔ outcome = ProbeOutcome.valued

The crash model requires success for convergence.

theorem Minimalism.obligatory_always_converges (outcome : ProbeOutcome) : derivationConverges AgreementModel.obligatoryNocrash outcome = true

The obligatory-no-crash model always converges.

theorem Minimalism.failed_yields_default : ProbeOutcome.unvalued.yieldsDefault = true

Failed probes yield default morphology (the Elsewhere entry).

theorem Minimalism.success_no_default : ProbeOutcome.valued.yieldsDefault = false

Successful probes do NOT yield default morphology.

theorem Minimalism.failure_produces_elsewhere : derivationConverges AgreementModel.obligatoryNocrash ProbeOutcome.unvalued = true ∧ ProbeOutcome.unvalued.pfRealization = PFRealization.elsewhere

In the obligatory-no-crash model, failed agreement produces the Elsewhere PF realization — not a crash. This is Preminger's central empirical prediction (Ch. 5).

inductive Minimalism.ProbePresence : Type

Whether a probe was present in the derivation. Obligatoriness means: if the functional head is projected, its probe MUST be present. The question is what happens when the probe fails — not whether it can be absent.

• present : ProbeOutcome → ProbePresence

  Probe is present (functional head projected).

• absent : ProbePresence

  No probe (functional head not projected).

def Minimalism.instDecidableEqProbePresence.decEq (x✝ x✝¹ : ProbePresence) : Decidable (x✝ = x✝¹)

Equations

• Minimalism.instDecidableEqProbePresence.decEq (Minimalism.ProbePresence.present a) (Minimalism.ProbePresence.present b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqProbePresence.decEq (Minimalism.ProbePresence.present a) Minimalism.ProbePresence.absent = isFalse ⋯
• Minimalism.instDecidableEqProbePresence.decEq Minimalism.ProbePresence.absent (Minimalism.ProbePresence.present a) = isFalse ⋯
• Minimalism.instDecidableEqProbePresence.decEq Minimalism.ProbePresence.absent Minimalism.ProbePresence.absent = isTrue ⋯

instance Minimalism.instDecidableEqProbePresence : DecidableEq ProbePresence

Equations

• Minimalism.instDecidableEqProbePresence = Minimalism.instDecidableEqProbePresence.decEq

def Minimalism.instBEqProbePresence.beq : ProbePresence → ProbePresence → Bool

Equations

• Minimalism.instBEqProbePresence.beq (Minimalism.ProbePresence.present a) (Minimalism.ProbePresence.present b) = (a == b)
• Minimalism.instBEqProbePresence.beq Minimalism.ProbePresence.absent Minimalism.ProbePresence.absent = true
• Minimalism.instBEqProbePresence.beq x✝¹ x✝ = false

instance Minimalism.instBEqProbePresence : BEq ProbePresence

Equations

• Minimalism.instBEqProbePresence = { beq := Minimalism.instBEqProbePresence.beq }

instance Minimalism.instReprProbePresence : Repr ProbePresence

Equations

• Minimalism.instReprProbePresence = { reprPrec := Minimalism.instReprProbePresence.repr }

def Minimalism.instReprProbePresence.repr : ProbePresence → ℕ → Std.Format

Equations

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

def Minimalism.ProbePresence.realization : ProbePresence → Option PFRealization

The three-way distinction that Preminger argues for:

1. Probe present + valued → agreement morphology
2. Probe present + unvalued → default morphology (NOT crash)
3. Probe absent → no agreement morphology at all

The crash model collapses (2) into ungrammaticality, losing the distinction between (2) and (3).

Equations

• (Minimalism.ProbePresence.present a).realization = some a.pfRealization
• Minimalism.ProbePresence.absent.realization = none

theorem Minimalism.present_unvalued_vs_absent : (ProbePresence.present ProbeOutcome.unvalued).realization ≠ ProbePresence.absent.realization

Present+unvalued and absent are observationally distinct: the former produces default morphology, the latter produces no morphology. The crash model cannot capture this.

def Minimalism.attemptAgree (probeFeats goalFeats : FeatureBundle) (ftype : FeatureVal) : ProbeOutcome

Run an Agree attempt and return the outcome.

This bridges the Agree mechanism (applyAgree) with the failure model (ProbeOutcome): if valuation succeeds, the probe was valued; otherwise it attempted but failed. This is the missing link between the Agree operation (which returns Option FeatureBundle) and Preminger's obligatory-but-failable model (which distinguishes valued from unvalued).

The key insight: the Agree mechanism itself doesn't decide what happens on failure — that's the job of the AgreementModel. This function extracts the binary outcome so the model can decide convergence.

Equations

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

def Minimalism.agreeWithModel (model : AgreementModel) (probeFeats goalFeats : FeatureBundle) (ftype : FeatureVal) : Bool × PFRealization

Run Agree under a given model and return convergence + PF realization.

Equations

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

theorem Minimalism.attemptAgree_valued {pf gf : FeatureBundle} {ft : FeatureVal} {result : FeatureBundle} (h : applyAgree pf gf ft = some result) : attemptAgree pf gf ft = ProbeOutcome.valued

Successful Agree yields a valued probe outcome.

theorem Minimalism.attemptAgree_unvalued {pf gf : FeatureBundle} {ft : FeatureVal} (h : applyAgree pf gf ft = none) : attemptAgree pf gf ft = ProbeOutcome.unvalued

Failed Agree yields an unvalued probe outcome.

theorem Minimalism.agreeWithModel_obligatory_converges (pf gf : FeatureBundle) (ft : FeatureVal) : (agreeWithModel AgreementModel.obligatoryNocrash pf gf ft).fst = true

Under the obligatory-no-crash model, Agree always converges regardless of whether the probe found a goal.