Proofs and Metalanguage

Question

I've read that proofs take place in a metalanguage. My question: is there a proof that a proof must take place in a metalanguage, or is this taken to be obvious? Sorry if my question might be too similar to 'Why are ⊢ and ⊨ symbols from metalanguage?' or other posts.

Answer 1

"Proofs take place in the metalanguage" is a fair, but suboptimal description, in my opinion. A (formal) proof of a sentence $S$ in the formal theory is a sequence of formulae, each of which are either axioms or follow from earlier statements from rules of inference, whose last line $S$. (Or something similar to this, depending on the nature of the deductive system you are using.)

What occurs in the metatheory are the following:

1. Verification that in fact, what you have written down is a list of strings of characters in the formal language.
2. Verification that each of strings of symbols in the list is in fact a well-formed formula of the language.
3. Verification that the list of sentences follows the rules described above to constitute a proof of the sentence.

(Actually, $2$ could all be rolled into $3,$ but I wanted to emphasize that all the 'low-level' stuff is the meta-theory at work.)

When we have carried this out (in the meta-theory) then we consider ourselves to have proven (that is, proven in the metatheory) that "$\vdash S"$ (which is a meta-statement). This is not 'the proof' of $S$ but is a verification of the fact that some sequence of sentences constitutes a valid proof of $S.$

Notice the proof itself isn't significantly less "formal" a thing than sentences and formulae. It is just another structure of a similar sort. The metatheory is where we verify that in fact it is a proof (and for that matter that sentences are sentences, formulae are formulae, etc.)

So it doesn't really make sense to consider whether a proof must take place in the metalanguage. All of our talking about our formal system - what is a symbol, what is a sentence, what is a proof - takes place in the metalanguage.

addendum

(which may or may not be helpful, depending on your background)

To clear up another potential point of confusion, one strange thing is that if you open a book on axiomatic set theory, which purports that its theorems are consequences of ZFC, ZF, ZF$^-,$ or what-have-you, you will not see long annotated lists of symbols, but rather arguments given in natural language for the truth of the theorems. These shouldn't be confused with arguments 'in the metatheory.' These proofs should really be viewed as natural language translations of the long lists of symbols (which would be much more difficult to follow). After all, the formal system is meant to model our assumptions and reasoning. Occasional peppered in reminders of where the proof uses replacement or foundation can serve as reminders that we're really working the formal system here.

So a proof of a theorem of ZFC in one of these books is really implicitly instructions for how to write down a formal proof in the formal language, and also implicitly verifies it, thus establishing $ZFC\vdash S.$ So it really is a meta-result (as all our results about formal systems are), but the lion's share of reasoning expressed in the proof the stuff that got translated into the formal proof. To add to the confusion, often these results are expressed alongside results that don't have the simple form $ZFC\vdash S,$ but rather have a more intricate role for the metatheory than simply verifying the proof. These include theorem schema and what are often called "meta-theorems." Theorem schema are results that have a form like "for any formula $\phi$ (meeting certain conditions), there is a sentence $S(\phi)$ such that $ZFC\vdash S(\phi)$," and "meta-theorems" are things with more complicated forms than that. An example is the relative consistency statement $Con(ZF)\to Con(ZFC)$ which can be phrased more clearly like: "if there is a proof in ZFC of a contradiction, then there is a proof in ZF of one."

Answer 2

Mathematics is made of proofs. Every theorem has a proof.

In mathematical logic we formalize the object of study as a formal system with syntax and semantics.

Usually we define a calculus, i.e. a set of axioms and rules of inference.

Withe them we define the key concept of derivation, i.e. the formalized counterpart of proof.

But the formal system is itself a mathematical object and we study it in order to discover its properties: soundness, completeness, consistency.

Thus, the mathematical theory of formal systems produces proofs about the formal systems, like the Deduction theorem for propositional calculus or Gödel's completeness theorem for first-order logic.

These are mathematical theorems about logical calculus and, being math theorems, they have a proof. But they are not theorem in the calculus and their proof is not a derivation in the calculus.

Thus, we say that they are meta-logic theorems, in order to avoid the confusion with the formulas derived in the calculus, that are logic theorems.

---

The symbol that expresses the derivability relation between formulas: $\vdash$, as well as that expressing the relation of logical consequence between formulas: $\vDash$, are symbols in the meta-language; they are not part of the formal language of the calculus.

The connectives: $\to, \lnot$ and the quantifiers are part of the formal language and we need them in order to write the expressions of the formal language.

The symbol $\vdash$ is used e.g. to express the fact that a formula is derivable in the propositional calculus :

$\vdash P \to (Q \to P)$.