Metalanguage of mathematics 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")?
 A: Let's clear up a misconception: mathematics as a whole doesn't have one metalanguage. One theory $T$ in a language $L$ has a metatheory $T^\prime$ in metalanguage $L^\prime$. Tarski showed languages are free of paradox iff they can't ascribe truth values as a predicate to its own statements, so we take $L^\prime\ne L$. But presumably, you want both theories to be part of "mathematics", as well as an infinite hierarchy of metatheories above $T^\prime$ too.
Meanwhile, what we can write in practice can be formal, semiformal or informal, which allows us to think of English with extra symbols as the language of every theory we study. This makes sense as long as you accept each such extension gives a "different" language. For example, English with $L^\prime$ add-ons isn't the same as English with $L$ add-ons.
In Objective Knowledge , Popper discussed the use of one natural language to statements in another, which is another way you can get your head around the principles of metalanguages. Popper used this to explain Tarski's technical insights into metalanguage behaviour. Here's an example: "The German sentence Der Mond ist aus grünem Käse gemacht is true iff the moon is made of green cheese."
