Barendregt's Variable Convention: what does it mean?

Question

Barendregt's Variable Convention: If $M_1,...,M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

This convention appears a lot in papers and I always wonder what does it mean. I want to know exactly what it is saying. I have two ideas about it

when you working on the theory

1. always keep a bound variable's name different from the names of variables at a particular time (Note:two bound variables may have same names)

2. always keep a bound variable name different from name of other bound variables name and all free variable names (every name is distinct)

Variable convention does not mention about if we can have two bound variables with same names, but I feel variable convention also implies such distinctiveness of bound variables.

So anyone clarify it to me?

Thanks in advance!

• Andrej Bauer: It's a device to pretend that one is taking syntax seriously. After you've implemented type theory and/or a programming language several times, you stop believing that variable capture can be done by humans in textbooks.
• alim: @AndrejBauer I don't understand what you mean.
• chi: @alim The point is: avoiding variable capture is trivially doable in theory, exploiting alpha-conversion, but painful and boring to do explicitly every time in proofs and definitions. Worse, despite it being trivial, it's very easy to get it wrong at first, e.g. by forgetting to alpha-convert, or by alpha-converting to a non completely fresh name. When you try to write an interpreter (or several ones) of a language, this often has to be done, no matter how tedious or error-prone it is. After one tries, and sees how easy it is to get it wrong, one starts to understand the pain.
• chi: @alim In papers, which are meant for humans instead of computers, carefully handling alpha-conversions is boring, error-prone and detrimental to presentation. The Barendregt convention basically says "we know one should handle renaming more precisely, but we won't -- we instead pretend that closed terms are considered up-to alpha, but still dissect them structurally when needed, without really checking that what we do does not depend on the choice of the bound names, since it is so boring".
• Andrej Bauer: The real pain actually starts not when you implement bound variables (no renaming is necessary there) but when you want to prove meta-theorems about syntax, or God forbid, that your programs work correctly.