How are metalogic proofs valid?

Solution 1:

Short answer: yes, it is essentially a chicken-and-egg problem, or perhaps a hermeneutical circle or a spiral. The common interpretation of the incompleteness theorems is that this circularity cannot be avoided.

You can use normal mathematical reasoning for the metatheory - which is not formalized in the first place - or you can choose some formal theory. In the latter case, you can choose a stronger metatheory, like ZFC, or a weaker one, like PRA.

In principle, you would then be able to choose a meta-metatheory, a meta-meta-metatheory, etc., but in practice essentially all the interesting issues arrive at the theory/metatheory level, and the higher levels just repeat these issues rather than giving new issues.

Solution 2:

This is actually not a disagreement with Carl Mummert's answer, but another way of thinking about it. No, it isn't circular. But you don't prove what you might imagine you prove.

All actual proofs in mathematics are in what we call "mathematical English" -- we believe this is all completely rock solid, but essentially it is in the form of sentences and paragraphs and so on. Sometimes (rarely) you even diagram those sentences and break them down into something that looks more like formulas, and follow rigid rules (see Russell's "game on paper" interpretation of math), but ultimately the idea is to be "completely convinced" that a statement is true.

The informality of the above is completely necessary and unavoidable!

When we "prove theorems about theorems" or any other meta-mathematical idea, what we really do is design (in our informal mathematical English) a model where we represent statements as numbers, and so on, so that we can say "this number represents a sentence" and "this number represents a proof of this statement from this set of statements" and so on, we're actually making a statement about numbers.

You convince yourself that this statement about the natural numbers is really the same as the metamathematical statement you care about. This can't be formalized either, but should be seen as "obvious" once explained properly. Then you can prove this statement about numbers in the normal mathematical sense.

Solution 3:

I think Richard Rast's answer is basically right, but I want to add a little to it.

Ordinary logic, as practiced by mathematicians, studies a formalized copy of mathematics. It studies that copy using the same tools, and the same level of rigor, as any other field of mathematics. People get confused about this because the object being studied and the tools being used to study it look so similar.

For instance, the soundness theorem specifies a relationship between certain combinatorial objects (proofs) and certain algebraic objects (models). In mathematical logic, the fact that these objects remind us mathematical proofs has no bearing on what constitutes a proof: the standard of validity is the same as for any other combinatorial proof.

Using logic as a philosophical foundation for mathematics is a more delicate task, and is fundamentally a philosophical project, not a mathematical one, though it obviously has to be heavily informed by mathematical ideas. There, as in any other attempt at a foundation for mathematics, the question of what can be taken as basic and what gets built on top of what is very difficult. In particular, materials on mathematical logic don't generally concern themselves with these issues.