What does it mean for metatheory to be some formal system

Question

In logic I have encountered statements like PA cannot prove itself, PA cannot prove its consistency using PA as a metatheory, ZFC cannot prove its consistency using ZFC as a metatheory and so on.

I have trouble understanding what does it mean for PA to be a metatheory or ZFC to be a metatheory.

I have learned metamathematics and logic using the book by Kleene "Introduction to Metamathematics".

There, the idea, if I understand correctly, is that many things in mathematics are not intuitive for humans, for example, infinite sets and operations on infinite sets. Thus, instead of abandoning such mathematics, we should formulate them using something that humans can understand. Then, there is an idea that theory and all our ideas about non intuitive things could be recasted as finite sequences which we give certain interpretation. But then, in order to make sure we do not have wrong intuition about it, we should make proofs and theorems purely syntactical, i.e. finite sequences of strings/symbols which can be checked for being a proof or theorem algorithmically without any appeal to what those objects are or what these objects represent.

Then, metatheory is a specification of what is a formula, proof, deduction and so forth. These definitions are given in terms of finite symbols and finite strings, so that they are accessible by our intuition. I was thinking that it means that metatheory cannot be formalized because for something to be formalized it means that we understand what the definition of formula, proof and so forth means. But metatheory is exactly such specification of these definitions. If it would use its own definitions it would become circular [?].

So, what does it mean for metatheory be PA? Is there some multi-layered path? For example:

1. We define what it means for a formal theory to have proof, formula, theorem, deduction and so on.

2. We define axioms of some formal theory, say, PA.

3. We somehow argue that metamathematical definitions are interpreted in PA (no idea how to formalize this).

4. Then by proving something in PA we interpret it as being true for metamathematical definitions (because of the interpretation).

5. We add another theory. (How can we do that? For example, how to formally analyze PA using PA? How can we add another theories?)

I hope that my question makes sense. Please feel free to give any suggestions, references and comments. I would appreciate that!

Also maybe you can recommend me some reference textbooks on this question. Something of the level of rigor like Kleene's "Introduction to Metamathematics" would be very appropriate.

Answer 1

Formalization of a metatheory in PA is essentially the same thing as arithmetization of syntax (I assume you're familiar with this since you've asked several questions about GIT). You can code expressions and lists of expressions by Godel numbers. Then, for instance, you can translate your rules for whether an expression is a well-formed to a arithmetic predicate that takes the Godel number of an expression and holds iff it is a well-formed formula. You can also take the rules for forming a proof (say in some Hilbert system) and write down an arithmetic predicate $P(m,n)$ that holds if and only $m$ is the code for a proof of the sentence coded by $n.$ This is just the proof predicate that figures prominently in the incompleteness theorem (when the theory in question PA itself).

Hopefully this also makes it clear that the purpose of formalizing the metatheory isn't necessarily to justify it in the way Hilbert wanted to justify set theoretical mathematics. Really, we just want to study our reasoning systems mathematically: our agenda can really be anything. In this case, doing so leads to neat results about formal systems in general, like the incompleteness theorem... so our agenda can be just that.

More generally, the view you describe is a rather limited way of looking at what logic and formalization are 'for', although it is certainly one important facet. Part of the issue might be that you're reading a textbook that, though very good by most accounts, was written in the 1950s. There are certainly more modern accounts of the incompleteness theorems available (see for instance Smullyan's book, Boolos/Jeffrey, or if you want more philosophical content, Smith).

Hopefully this also puts the circularity you describe into perspective. It is true that if you keep trying to justify/clarify your reasoning system by formalizing it in terms of lower-level concepts, you will eventually wind up in a vicious circle. Could your meta-meta-meta-meta theory possibly be any more intuitive and obviously sound than your meta-meta-meta-theory? At a certain point we need to stop and take the $\mbox{meta}^n$-theory on faith. But again, reducing your reasoning to more intuitive and obviously sound principles isn't always the point of formalization (even if it can be a compelling reason sometimes).

Answer 2

In ordinary mathematics, we don't really need a metatheory - we are interested in proving theorems, and if we worry about the axioms we use then those axioms make a formal theory that we use to prove things.

In logic, we sometimes want to study formal theories themselves, using methods of mathematics. To do so, we could worry about which axioms we want to use to prove things about formal theories. These new axioms are then called the metatheory, and the theory we are studying is called the object theory.

In practice, we can use almost any foundational mathematical theory as a metatheory, although the choice of a particular metatheory can restrict what we can express and prove about the object theory.

• If we use a theory of arithmetic as a metatheory (e.g. Peano Arithmetic), we can prove things about the syntax of the object theory, but it is difficult to even express statements about models of the object theory. There are also consistency issues - for example PA does not prove that ZFC is consistent. However, we can prove the incompleteness theorem and some syntactic results such as the deduction theorem in Peano Arithmetic.

• If we use a stronger theory such as ZFC for the metatheory, we can also study models of the object theory. This allows us to prove theorems such as the completeness and compactness theorems, which are of course fundamental tools in logic. In some cases, we can get by with theories weaker than ZFC, such as second-order arithmetic. In other cases, we may want to add additional axioms to ZFC, particularly large cardinal axioms.

In the early 20th century, there were reasons that logicians were interested in finitistic metatheories, but that is no longer the main focus. In contemporary logic, we often move between different metatheories depending on what we want to achieve at each moment.

It is also true that we could look at a metametatheory to study the metatheory. However, most of the interesting issues already arise at the metatheory / object theory level, and so there is not often much interest in having three or more levels of metaness.