Docs / Syntax / Minimalist / Probe / SyntacticObject

Minimal search over syntactic objects

import Linglib.Syntax.Minimalist.Probe.SyntacticObject · namespace Minimalist.LinearizedSyntacticObject

This file instantiates probe search at the tree: a probe on the head at a position of a linearized object searches the positions the head c-commands in some order, a key on positions. Closest by the branching positions above them, it finds a goal that no other satisfier asymmetrically c-commands: the Minimal Link Condition, with mutually c-commanding candidates equidistant. Procedural search orders are in Probe/Search.lean. Positions closed to the search, by the PIC or by a horizon, cut its domain. Agree and labeling are both this search; what Agree then does to the features of the probe and the goal is Minimalist.FeatureState.value.

Main definitions

Minimalist.LinearizedSyntacticObject.goalsBy, goals, goalsUnder: the terms a probe on a head finds under a search order, under closeness, and with some positions closed to it.
Minimalist.LinearizedSyntacticObject.leafProbe, phraseProbe: the probes satisfied by the leaves of a category, and by the phrases its heads form.

Main results

Minimalist.LinearizedSyntacticObject.not_finds_of_cCommands: a satisfier that asymmetrically c-commands a position blocks the goal there.
Minimalist.LinearizedSyntacticObject.finds_above_branching_iff: among satisfiers none of which dominates another, a probe finds those that no satisfier asymmetrically c-commands.
Minimalist.LinearizedSyntacticObject.mem_goals_leafProbe_map_iff: a probe for the leaves of a category finds the same goals under an injective relabelling that keeps categories.

References

Chomsky 2000, Minimalist Inquiries: The Framework

Closest goals

A probe on the head at a position searches the positions the head c-commands, keyed by the branching positions above each (LinearizedSyntacticObject.above), and finds a goal minimal under the key, the Minimal Link Condition of Chomsky 1995.

A satisfier that asymmetrically c-commands a position blocks the goal there, whatever else the probe's domain holds.

theorem not_finds_of_cCommands L55–59

{t : LinearizedSyntacticObject} {p : Probe (↑t).Positions} {s : Set (↑t).Positions} {q g : (↑t).Positions} (hq : q ∈ s) (hsq : p.sat q) (hqg : (↑t).CCommands ↑q ↑g) (hgq : ¬(↑t).CCommands ↑g ↑q) :

¬p.Finds s (t.above t.branching) g

Among satisfiers none of which dominates another, a probe finds those that no satisfier asymmetrically c-commands: mutually c-commanding candidates are equidistant.

theorem finds_above_branching_iff L61–67

{t : LinearizedSyntacticObject} {p : Probe (↑t).Positions} {s : Set (↑t).Positions} {g : (↑t).Positions} (hs : IsAntichain (fun (x1 x2 : (↑t).Positions) => x1 ≤ x2) {q : (↑t).Positions | q ∈ s ∧ p.sat q}) :

p.Finds s (t.above t.branching) g ↔ (g ∈ s ∧ p.sat g) ∧ ∀ ⦃q : (↑t).Positions⦄, q ∈ s → p.sat q → ¬((↑t).CCommands ↑q ↑g ∧ ¬(↑t).CCommands ↑g ↑q)

The terms a probe on the head h finds when its search orders positions by key: those at the first satisfying positions that an occurrence of h c-commands.

def goalsBy L74–79

(t : LinearizedSyntacticObject) {β : Type u_1} [Preorder β] [DecidableRel fun (x1 x2 : β) => x1 < x2] (p : Probe (↑t).Positions) (h : SyntacticObject) (key : (↑t).Positions → β) :

Finset SyntacticObject

t.goalsBy p h key = Finset.image t.termAt {g : (↑t).Positions | ∃ (a : (↑t).Positions), t.termAt a = h ∧ p.Finds {q : (↑t).Positions | (↑t).CCommands ↑a ↑q} key g}

Used by mem_goalsBy, goals

Used in BrananErlewine2026, Storment2026

L81–86

The terms a probe on the head h finds: those at the closest satisfying positions that an occurrence of h c-commands.

def goals L91–94

(t : LinearizedSyntacticObject) (p : Probe (↑t).Positions) (h : SyntacticObject) :

Finset SyntacticObject

t.goals p h = t.goalsBy p h (t.above t.branching)

Built from

Used by mem_goals, goalsUnder_empty, mem_goals_leafProbe_map_iff

Used in AissenPolian2025, Bruening2001, Chomsky2013, Collins2005

L96–99

The terms a probe on the head h finds when, at each occurrence a of h, the positions cut a are closed to its search, by the PIC or by a horizon.

def goalsUnder L102–108

(t : LinearizedSyntacticObject) (p : Probe (↑t).Positions) (h : SyntacticObject) (cut : Core.Order.TreePath → Set Core.Order.TreePath) [(a : Core.Order.TreePath) → DecidablePred fun (x : Core.Order.TreePath) => x ∈ cut a] :

Finset SyntacticObject

The definition is too large to print here; read it in the source.

Used by goalsUnder_empty, mem_goalsUnder_of_finds

Used in AissenPolian2025

L110–112

L114–120

The probe satisfied by the leaves of category c.

def leafProbe L123–125

(t : LinearizedSyntacticObject) (c : Cat) :

Probe (↑t).Positions

t.leafProbe c = Minimalist.Probe.relativized fun (q : (↑t).Positions) => decide (Minimalist.SyntacticObject.isLeafOf c (t.termAt q)) = true

Used by mem_goals_leafProbe_map_iff

Used in AissenPolian2025, BrananErlewine2026, Collins2005, Storment2026

The probe satisfied by the phrases a head of category c forms with its sister, so that a phrase in a specifier is closer than whatever its sister contains.

def phraseProbe L128–133

(t : LinearizedSyntacticObject) (c : Cat) :

Probe (↑t).Positions

The definition is too large to print here; read it in the source.

Used in Chomsky2013

A probe for the leaves of a category finds the relabelled goals in a relabelled object, under an injective relabelling that keeps categories.

theorem mem_goals_leafProbe_map_iff L135–163

{t : LinearizedSyntacticObject} {f : LexicalItem.Token → LexicalItem.Token} (hf : Function.Injective f) (hcat : ∀ (t : LexicalItem.Token), (f t).item.cat = t.item.cat) {c : Cat} {h x : SyntacticObject} :

SyntacticObject.map f x ∈ (map f t).goals ((map f t).leafProbe c) (SyntacticObject.map f h) ↔ x ∈ t.goals (t.leafProbe c) h

Built from ,