# Is there any current development of a first order formalization of metamathematics?

I hope that this post isn't off topic, but I already asked math.stackexchange about first order formalizations of first order logic. There are provability logics and extensions in modal logic's that seem to attempt to address this question, and model theory implies answering questions about metamathematics. But I'm looking for an explicitly first order theory that can be used to prove things about metamathematics.

Basically, I'm wondering if there are first order formalizations of metamathematics. I'm interested in making proofs in first order logic about proof systems, such as the completeness and incompleteness theorems for first order theories in a fashion that is analogous to making a computer language compiler that can compile itself.

I understand that this probably should be possible, seeing it's generally agreed that you can represent most of mathematics in set theory, and represent set theory in first order logic, and I don't see any reason why encoding definitions about formal statements, provability, satisfiability, and other notions related to metamathematics would be unworkable.

There are formalizations of arithmetic both in the language of first order logic directly and in the language of set theory. Are there formalizations of metamathematical systems that I can use to make first order proofs about first order proofs similar to first order theories about arithmetic and set theory?

• I'm confused: in light of Goedel coding, how isn't first-order arithmetic already a "logic of proofs" (and other things besides)? My understanding was that weaker systems, like modal logics of proofs, are fragments of first-order arithmetic, although I could be wrong (theories axiomatizing notions of truth are really really strong, but these aren't quite theories of provability). – Noah Schweber Aug 7 '14 at 22:35
• The definition of a Gödel numbering is done in the metatheory, along with other definitions for making informal proofs. I'm looking for formal first order definitions, including of Gödel numberings. Arithmetic is embedded in set theory, but without the appropriate definitions its hard to ask questions about arithmetic in raw set theory, and without the appropriate definitions in arithmetic, its hard to ask questions about Gödel numbering of formula in arithmetic. – dezakin Aug 7 '14 at 22:50
• You can do nearly 100% of it in PRA and 97% in much less... See the article by Craig Smorynski in the Handbook of Mathematical Logic for a detailed exposition. – François G. Dorais Aug 7 '14 at 23:02
• Thanks, I'll check it. I was mostly motivated in asking questions about satisfiability, decidability, and provability about questions inside an automated theorem proving system, so I need to be able to formalize all definitions if I want to ask a question about a particular well formed formula like "Is this a decidable statement?" or "Is this a satisfiable statement?" or "Do statements that have this form fall in the set of decidable statements?" – dezakin Aug 7 '14 at 23:22
• You might also find this interesting - r6.ca/Goedel/goedel1.html – François G. Dorais Aug 7 '14 at 23:47