**Quote-plus**

jeremyw is correct, of course. Simply saying "permission to quote is granted" or something similar is almost as concise, and far clearer to most people.

**Metamath**

The second big problem with Metamath is the fact that it nails down specific constructions. It's important to note, however, that this is a characteristic of the set.mm database, not the Metamath framework itself.

The solution to this problem, I think, is to use "theory
interpretation." Instead of saying, for example, "0 is the empty set,
and x + 1 is x U {x}", you say, "for all sets N and functions +, -, *,
/, whatever satisfying the usual axioms for arithmetic." Then, if you
ever need to show the *existence* of such a thing, for example to
use arithmetic as a temporary while proving something else, you can
use the standard construction, or any construction for that matter.

The question is how much more awkward this will make proofs. Metamath's choice of a definite construction is good for overall simplicity. I guess there's really only one way to find out.