+1 interesting, relevant question. But it's a [soft-question] isn't it, and should be CW?

How about "For every x∈A, f(x) is prime"? I agree with "avoid", not with "[u]nder no circumstances": the issues are that (i) there's usually poor phrasing going on, and (ii) the typography is tricky.

@Pete: I think you are right. But a couple of caveats: Barendregt was speaking informally in a Q&A, and he was talking of systems with tactics, which Mizar doesn't have. And what baseline informal proof of the JCT should we be considering for our comparison? It's easy not to compare like with like here.

@Tom: only because ivy is generally used in mass noun constructions. "An ivy vine" is perfectly idiomatic English; "an ivy graph" would be fine in maths.

@castal: I've looked this up. Medieval west-European scholars of between C6th-12th did not have access to the whole of the Elements until Adelard of Bath translated it from Arabic to Latin, but they did have access to books 1-4 and 11-13; they were important texts. Islamic and Byzantine scholars had access to the whole text without interruption.

There's a lot of material in the published book that are not in the online lecture notes.

Now on SO: stackoverflow.com/questions/2701841/…