Metalanguage of mathematics

Question

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

The language of meta-math is the same language of math : natural language (e.g English) + symbols. — Mauro ALLEGRANZA, Feb 10 '19 at 12:49
What is relevant is the meta-theory of a formalized theory; in this case, the meta-theory must be some set theory. At least the theory of Hereditarily finite set : it must be capable of speaking of finite strings of symbols : expressions, formulas, and sequances of formulas : proofs. — Mauro ALLEGRANZA, Feb 10 '19 at 12:52
That's somehow disturbing. You use set theory to describe the meta-language of set theory? :-/ — YoungMath, Feb 10 '19 at 12:53
Examples : S.C.Kleene, Introduction to metamathematics (1952), Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic (1998), Stephen Simpson, Subsystems of Second Order Arithmetic (2009). — Mauro ALLEGRANZA, Feb 10 '19 at 12:55
Exactly........ What language do you use to describe the grammar of English language ? — Mauro ALLEGRANZA, Feb 10 '19 at 12:55
See also the post Separation of mathematics and metamathematics — Mauro ALLEGRANZA, Feb 10 '19 at 12:57
Well, that's more philosophical, but you use the language that everyone understands and the language you use to teach babies their native language: Gestures and mimics. — YoungMath, Feb 10 '19 at 12:58
See also what-does-it-mean-for-metatheory-to-be-some-formal-system? — Mauro ALLEGRANZA, Feb 10 '19 at 12:59

score 2 · Answer 1 · answered Feb 10 '19 at 13:22

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."

Metalanguage of mathematics

1 Answers1