What excactly is the matalanguage of mathematics?
I mean, the predicate calculus admits the formal language of mathematics, right? Then we add set axioms to it et voilá: mathematics.
But what does it mean when talking about metalanguage? In particular, when writing down a proof, what language is used? Then, usually, you write down english sentences and sometimes paragraphed predicate formulas. So, is this metalanguage?
Do you have some references or explainations? I'm very interested in this topic.
EDIT: Or is it, that the formal language of mathematics has no "sense" (Frege), just "reference" (truth or false). And the meta-language (like english+symbols?) gives these things "sense" (e.g. "what is a vector space")?