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:
We define what it means for a formal theory to have proof, formula, theorem, deduction and so on.
We define axioms of some formal theory, say, PA.
We somehow argue that metamathematical definitions are interpreted in PA (no idea how to formalize this).
Then by proving something in PA we interpret it as being true for metamathematical definitions (because of the interpretation).
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.