"Metalanguages of formal systems all resolve ultimately to natural language, the 'common parlance' in which mathematicians and logicians converse..."

Question

---

The current article on Metalanguage on Wikipedia states in the section In Natural Language:

Metalanguages of formal systems all resolve ultimately to natural language, the 'common parlance' in which mathematicians and logicians converse to define their terms and operations and 'read out' their formulae.[6]

Where [6] is the reference:

Borel, Félix Édouard Justin Émile (1928). Leçons sur la theorie des fonctions (in French) (3 ed.). Paris: Gauthier-Villars & Cie. p. 160.

I was able to find titles of the notes added in the 3rd edition:

NOTE DE LA TROISIÈME ÉDITION

VII - Pour ou contre la logique empirique.

- Logique formelle et logique empiriste, par Rolin Wavre.
- Sur le principe du tiers exclu et sur les théorèmes non susceptibles de démonstration, par Paul Lévy.
- Sur le principe du tiers exclu, par Rolin Wavre.
- Critique de la logique empirique, par Paul Lévy.
- A propos de la récente discussion entre Rolin Wavre et Paul Lévy, par Émile Borel.
- Sur la logique de Brouwer, par Barzin et A. Errera.
- Logique classique, logique brouwerienne et logique mixte, par Paul Lévy.

but I'm not able to find the document itself.

I guess my question is: where can I find some modern discourse on this notion that all metalanguage must eventually devolve into an informal natural language?

Answer 1

where can I find some modern discourse on this notion that all metalanguage must eventually devolve into an informal natural language?

You can see every mathematical logic textbook : the formal systems that are the "object" of the study are described with "standard" mathematical jargon : natural language plus mathematical symbols used as abbreviations.

See e.g. R.Kaye, The Mathematics of Logic (2007), page 28:

Proposition 3.6 Suppose $Σ ⊆ 2^*$ and $Σ \vdash ⊥$. Then there is a formal derivation of $⊥$ from $Σ$ using only the Given Strings and Shortening Rules. [...]

We have now explored this formal system in some detail. Most of our results have been mathematical theorems and arguments concerning what does or does not have a formal proof. Some people like to call such mathematical theorems and arguments metatheorems and metaproofs since they are theorems and proofs about theorems and proofs. This terminology is sometimes useful and you may use it if you wish, but there is nothing special about such ‘metamathematics’. Metamathematics is just the ordinary mathematics you are already used to.

To take this study further, and in particular to apply it to other areas of mathematics, we have to start thinking about what the formal system actually means. A formal system is really just like a game with symbols. To prove anything in this system you just follow the rules, nothing more. This is in some ways good, because there is no thinking involved and because a machine could check your working for you, but in other ways it is bad, because it does not seem that this system is proving anything particularly useful, or about anything. So the next step is to try to attach meaning or semantics to the symbols we are using, and interpret the strings of symbols of the system.

---

For a subtler discussion, see Yuri Manin, A Course in Mathematical Logic for Mathematicians (Springer, 2010), Ch.I Introduction to Formal Languages.

Answer 2

You may wish to look at "pragmatics". In most of the foundational literature you will find mention of how mathematical ideas are communicated from teachers to students with what are properly called "language acts". An exception to this can be found in de Morgan's paper on double algebra. Seen as an anticipation of model theory, de Morgan describes a scenario wherein an uninitiated individual ascribes meaning to an ideal formal proof.

In the twentieth century, Carnap had attempted to reduce mathematical theories to a purely syntactic exercise. Tarski's work on semantics motivated him to relax his views with respect to syntax. But, when describing syntax and semantics, he still gave no account of meaning with respect to language users. The "third leg" of pragmatics had been acknowledged ( It does not originate with Carnap. But, his invocation of its role motivated its development. )

Tarski is known for a semantic conception of truth. When Carnap pursued semantics, he did so with an analytic conception of truth. It is with this view that formalizations ultimately reduce to natural language interpretation. His book on meaning and necessity is an attempt at using an analytic conception of truth to implement modality. His motivation had been Wittgenstein's "states of affairs". This, however, had been unsuccessful. Kripke would eventually develop a successful interpretation of modal contexts.

Carnap's work led to "meaning postulates". Run searches on that expression in combination with "intensional logic".