German: translating metasyntactic identifiers etc.

[avekens]

In metamath/metamath-website-seed#21, It was discussed if (and how) metasyntactic identifiers and other technical texts should be translated (into German) or remain in English.
My concern was that Metamath is used in English, and capitalization imight be an issue in this context.

Remark of @digama0:

My thinking is that we should ideally be able to have a full-German experience here, like a properly translated system: the book is in German, the software speaks German, and while set.mm will continue to be in English one can have a German metamath database without issue and then it is possible to not really come in contact with English. At least, this to me seems like the ideal end-state for a proper localization.

[jkingdon]

In general this is a pretty tricky question. For example, when writing in English do you say "detachment" or "modus ponens"? I think there are also examples of mathematical terms borrowed from Russian, German, French, or other languages, although I'm not finding them right now.

As for this book in particular, I suppose I'll defer to those who might benefit from a full-German experience (if/when we hear from them). But I don't think I'd dismiss some level of polyglotness as an ideal end-state. Having a few words here and there from another language (especially words which might be loanwords anyway if "translated") is a pretty different situation than having large blocks of text.