Names should be automatically generated. Alpha-equivalence should be trivial. English shouldn't be required, but you're not going to get away from requiring something of equivalent expressiveness at some level.
Ruby allowing utf-8 identifiers is successfully used with Japanese. Using symbols instead of a few english keywords would completely solve the problem, maybe using configurable automatic string replacement to get the symbols, comparable to IDEs like coq.