Binding at a stage of the derivation

Movement reorders c-command, and binding may be evaluated before or after it: reconstruction. CCommandsAt d n x y says that x c-commands y in the object the replay of d reaches after n steps, which by faithfulness is d.stageAt n itself, so the predicate decides a fact about the unordered syntactic object; a stage whose replay fails c-commands nothing. BindsAtSurface evaluates binding at the last stage and BindsAtSomeStage at any, the derivational binding condition under which a sentence is well formed as soon as some stage satisfies it ([cole-hermon-2008], fn. 28), reconstruction to any position the mover passed through. Binding at some stage is monotone under extending the derivation; binding at the surface is not.

Main definitions

• Minimalist.SyntacticObject.Derivation.CCommandsAt, BindsAtSurface, BindsAtSomeStage

Main results

• Minimalist.SyntacticObject.Derivation.CCommandsAt.cCommandsIn_stageAt: the predicate speaks of the derivation's own stage.
• Minimalist.SyntacticObject.Derivation.cCommandsAt_append_of_le, BindsAtSomeStage.append.

References

• [cole-hermon-2008]

def Minimalist.SyntacticObject.Derivation.CCommandsAt (d : Derivation) (n : ℕ) (x y : SyntacticObject) : Prop

x c-commands y at stage n of d: in the ordered object the replay reaches after n steps.

Equations

• d.CCommandsAt n x y = ∃ p ∈ (d.take n).externalize?, (↑p).cCommandsIn x y

@[instance_reducible]

instance Minimalist.SyntacticObject.Derivation.instDecidableCCommandsAt (d : Derivation) (n : ℕ) (x y : SyntacticObject) : Decidable (d.CCommandsAt n x y)

Equations

• d.instDecidableCCommandsAt n x y = id inferInstance

theorem Minimalist.SyntacticObject.Derivation.CCommandsAt.cCommandsIn_stageAt {d : Derivation} {n : ℕ} {x y : SyntacticObject} (h : d.CCommandsAt n x y) : (d.stageAt n).cCommandsIn x y

The stage the predicate looks at is the derivation's own.

theorem Minimalist.SyntacticObject.Derivation.cCommandsAt_append_of_le {d : Derivation} {steps : List Step} {n : ℕ} {x y : SyntacticObject} (h : n ≤ d.length) : (d.append steps).CCommandsAt n x y ↔ d.CCommandsAt n x y

The early stages of an extended derivation are the original's.

@[reducible, inline]

abbrev Minimalist.SyntacticObject.Derivation.BindsAtSurface (d : Derivation) (x y : SyntacticObject) : Prop

Surface binding: c-command at the last stage.

Equations

• d.BindsAtSurface x y = d.CCommandsAt d.length x y

def Minimalist.SyntacticObject.Derivation.BindsAtSomeStage (d : Derivation) (x y : SyntacticObject) : Prop

Derivational binding: c-command at some stage.

Equations

• d.BindsAtSomeStage x y = ∃ n ≤ d.length, d.CCommandsAt n x y

@[instance_reducible]

instance Minimalist.SyntacticObject.Derivation.instDecidableBindsAtSomeStage (d : Derivation) (x y : SyntacticObject) : Decidable (d.BindsAtSomeStage x y)

Equations

• d.instDecidableBindsAtSomeStage x y = id inferInstance

theorem Minimalist.SyntacticObject.Derivation.BindsAtSurface.bindsAtSomeStage {d : Derivation} {x y : SyntacticObject} (h : d.BindsAtSurface x y) : d.BindsAtSomeStage x y

Binding at the surface is binding at some stage.

theorem Minimalist.SyntacticObject.Derivation.BindsAtSomeStage.append {d : Derivation} {steps : List Step} {x y : SyntacticObject} (h : d.BindsAtSomeStage x y) : (d.append steps).BindsAtSomeStage x y

Binding at some stage is monotone under extension.