# 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")?

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.