Defective Goal

@cite{roberts-2010} @cite{storment-2025} @cite{storment-2026}

Roberts's notion of a defective goal: a goal whose formal features are a proper subset of those of its probe. Defective goals trigger default agreement (the probe's unvalued features cannot all be checked) and underlie a range of empirical patterns: PCC effects, Setswana SM17 default subject marking in QI, Bantu locative inversion agreement.

Used by:

• DefectiveCircumvention.lean — Storment's probing operation that conditionally re-probes past a defective goal.
• Phenomena/ArgumentStructure/Studies/Storment2026.lean — derives Setswana QI agreement default from defective theme.

def Minimalist.Probing.DefectiveGoal (probe goal : FeatureBundle) : Prop

A goal G is defective with respect to a probe P iff G's formal features are a proper subset of P's. The probe needs more features than the goal has to offer, so checking is incomplete. @cite{roberts-2010}, ch. 2; cited as eq. (49) in @cite{storment-2026}.

Equations

• Minimalist.Probing.DefectiveGoal probe goal = (goal ⊆ probe ∧ ∃ f ∈ probe, f ∉ goal)

@[implicit_reducible]

instance Minimalist.Probing.instDecidableDefectiveGoal (probe goal : FeatureBundle) : Decidable (DefectiveGoal probe goal)

Equations

• Minimalist.Probing.instDecidableDefectiveGoal probe goal = id inferInstance

theorem Minimalist.Probing.DefectiveGoal.empty_of_nonempty (probe : FeatureBundle) (h : probe ≠ []) : DefectiveGoal probe []

The empty goal is defective with respect to any nonempty probe.

theorem Minimalist.Probing.DefectiveGoal.exists_missing {probe goal : FeatureBundle} (h : DefectiveGoal probe goal) : ∃ f ∈ probe, f ∉ goal

A defective goal is necessarily missing some feature the probe has.

theorem Minimalist.Probing.DefectiveGoal.subset {probe goal : FeatureBundle} (h : DefectiveGoal probe goal) : goal ⊆ probe

A defective goal's features are all in the probe (proper subset).

theorem Minimalist.Probing.DefectiveGoal.irrefl (fb : FeatureBundle) : ¬DefectiveGoal fb fb

No goal is defective with respect to itself.