Binding at a reading

This file proves that binding at the copy object is binding at one reading: a token c-commands another in the copy object just when it does in the reading in which the chains holding the second are read low. So the choice of copies the semantic interface reads loses no binding relation, and the reading that shows a given relation is found from the bound token alone. When nothing moves from itself a reading also creates no binding, so binding at the copy object is binding at some reading.

Implementation notes

• The theorem names one reading as well as some reading because the reading is found locally, and the step-by-step induction needs that: the test that a copy holds y is independent of the stage.
• Without DistinctDaughters a reading may bind where the copy object does not: an object that moves from itself, read low, comes to c-command the sister of its movement node.
• Two chains sharing a mark could have mark reach copies with different terms, which MarksName excludes. Reading each chain high or low is enough because the theorem concerns one pair of tokens at a time.

References

• Chomsky 1995, The Minimalist Program formalized
• Collins 2005, A Smuggling Approach to the Passive in English formalized
• Collins 2026, Reconstruction and the New Minimalism formalized