# How can you formalize the metamathematics conventionally used to state Godel’s theorem?

Gödel’s incompleteness theorem states that for any sufficiently strong formal system $T$ there exists a statement $G$ such that if $T$ is consistent, then $G$ is true but not provable in $T$. But I’m interested in how to formally state Gödel‘s theorem in symbolic language.

What is often said in this context is that systems of arithmetic as weak as PRA can prove $Con(T)\rightarrow\neg Pr_T(G)$, or in words “If there exists no natural number $m$ which is the Gödel number of a proof of $0=1$ in $T$, then there exists no natural number $n$ which is the Gödel number of a proof of $G$ in T.” But the thing is, Gödel’s theorem isn’t usually stated as a theorem of arithmetic, but as a theorem of metamathematics. So my question is, is there any way to formalize the metamathematics conventionally used to state Gödel’s theorem? That is, using a formal language that talks explicitly about formal systems, statements, and proofs.

Am I right that proof theory is the relevant field to look in? Is provability logic relevant?

• Why? To me that’s like asking for a theory that was originally written in some specific language like Japanese. Jul 29, 2018 at 9:13
• There are many formal languages that capture it. Jul 29, 2018 at 9:19
• Probably what you are looking for is something like the HOL in proof assistants like Isabelle or Coq. See this paper: A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets These are very general purpose languages, but they are designed so that proofs can be stated in the correct level of generality. Jul 29, 2018 at 9:50
• What does it mean to "talk explicitly" about proofs? PA and ZFC can "explicitly talk" about formalized proofs, which are simply natural numbers that satisfy special properties about their factorization. If you are looking for a system where a proof means "a proof as in real life", that is, a string of symbols of the logic you work inside, then how are you planning to refer to these proofs with the variable symbols of the logic they belong to without doing some kind of coding? How are you planning to quantify over proofs? Jul 29, 2018 at 10:24
• @KeshavSrinivasan: I know what provability logic is but I don't understand how it answers your question (or, at least, the question which I think you are asking). In provability logic, the box operator means "it is provable that...". So what? You wrote that you want a system that "explicitly talks" about proofs, statements etc. How does the box operator help in this case? Provability logic simply sweeps the dirty work in Gödel's proof under the rug by taking the provability predicate which you construct in PA as a black-box (with some special properties known as Hilbert-Bernays conditions.) Jul 29, 2018 at 22:57

I may not be understanding your question, but here goes:

In most cases (aside from some metamathematics of set theory itself) the metalanguage is implicitly understood to be ZFC. So Gödel's first incompleteness theorem while a metatheorem of arithmetic is a theorem proper of ZFC.

The idea behind Gödel's second incompleteness theorem (as an improvement in his first incompleteness theorem) is that arithmetic itself can be used as the metalanguage. Gödel coding allows you to represent formulas in any recursive language as natural numbers. This can be extended to code proofs as natural numbers. Many of the properties proofs you might want to talk about in your metatheory can be expressed as arithmetic (in fact, primitive recursive) properties of their corresponding Gödel codes. So for example, one can define a formula $\phi(x)$ in the language of arithmetic such that $\phi(n)$ is true if and only if $n$ is a Godel code of a valid proof in a given recursively-axiomatizable proof system. One can also prove (as theorems of some weak fragments of arithmetic) basic proof theoretic facts like:

"If $T \vdash \phi$ and $T \vdash \psi$, then $T \vdash \phi \wedge \psi$"

The choice of proof system doesn't so much matter, as proof systems tend to be entirely syntactic, and any recursive syntax can be interpreted in the natural numbers, with all syntactic operations and relations interpretable as arithmetically-definable functions and relations on natural numbers. One important observation is that our metatheory does not need to refer to or have access to the standard model $\mathbb{N}$ of arithmetic, because if $P(x)$ is a primitive recursive predicate, then the truth of $P(n)$ for any standard natural number will be the same in any model of arithmetic. This is the reason we can go as far down as PRA for Godel's incompleteness theorem.

It's also possible to compare two theories, entirely using arithmetic as your metalanguage, so long as those theories are recursively-axiomatizable. The idea is you represent a recursively-axiomatizable theory as a natural number which codes a primitive recursive function whose range is the set of Gödel codes of axioms of that theory.

Gödel's first incompleteness theorem requires more metatheory than the second incompleteness theorem, because the "punch" of the theorem (that this unprovable sentence G is true in the standard model of arithemtic) requires a metatheory which can recognize that G is in fact true. But the second incompleteness theorem does not require this, so arithemtic itself can be the metalanguage.

• To be clear, as I said in my question I want to express Godel's theorem in a formal language that explicitly talks about proofs and statements and formal systems and the like, as opposed to talking in terms of Gödel numbers. Jul 29, 2018 at 8:23
• The language of arithmetic is a formal language that explicitly talks about proofs and statements and formal systems. Gödel numbering can be seen as specific example of the general principle that any kind of finite object (including proofs, recursively-axiomatized theories, images, etc.) can be represented as a finite binary string. The only difference between arithmetic and any other metalanguage you might want to use to express Gödel's theorem will be only a superficial syntactic difference. It is only our human bias which makes it seem $n$ refers to a number and not a proof. Jul 29, 2018 at 8:43
• It doesn’t explicitly talk about proofs, it explicitly talks about numbers. Regardless of human bias or what, I want a statement of Godel’s theorem that doesn’t mention Gödel numbering. Jul 29, 2018 at 8:55
• Just to be clear, the first incompleteness theorem says nothing about truth, just about provability, which does not require any fancy meta-theory.
– cody
Jul 29, 2018 at 15:07

I think this question is clearly asking for provability logic. This is the basic modal logic K with the additional axiom

$$\square(\square A \to A) \to \square A.$$

"$\square A$" is interpreted as "$A$ is provable" (with reference to some fixed target formal system).

Edit: the specific question of being able to prove the second incompleteness theorem in provability logic (the answer is yes) has been discussed on philosophy.stackexchange and math.stackexchange.

Just to be clear, the above refers to provability within a specific formal system. The general semantic notion of provability, in the sense of "demonstrable with rational certainty", outside of any fixed formal system has been axiomatized in this book. That is a much more subtle notion, but it can be consistently axiomatized.

• Is it possible to state and prove Godel's theorem in some system of provability logic? I think you would need quantified provability logic since you need the notions of "for all proofs" and "there exists a proof". Jul 29, 2018 at 16:37
• I think so, yes. There is such a thing as predicate provability logic but I don't think you need it since Godel's theorem is proven by producing a specific sentence $G$ which is neither provable nor unprovable, assuming the target system is consistent. (Consistency of the target system can be expressed by the propositional formula $\neg \square \perp$.) This G can be constructed using a fixed point theorem, which one does have in provability logic. Jul 29, 2018 at 16:50

The formal mechanisms for describing the first incompleteness theorem are well understood: indeed, part of the achievements of the body of work of the Russel, Frege and Hilbert school of formalism is carving out precise mathematical definitions of provability and consistency!

More precisely, the statement relies on 4 essential syntactic categories:

1. A language $\cal L$ which will outline the set of symbols which can be used to construct objects of the theory. These are typically $0, S, +, \times$ etc. Typically you can restrict yourself to finite such $\cal L$.

2. A set of terms $\cal T$ built from the language $\cal L$. These should be represented as trees, whose nodes are symbols in $\cal L$, and whose leaves are either symbols or variables in some infinite set $x,y,z, x',\ldots$ Note that we don't need to consider the infinite set of terms, just be able to express sentences like "for every term $t\in {\cal T},...$"

3. A set of sentences $\cal S$ which express statements about terms. Again these are trees with at their leaves atomic statements like $t_1=t_2$, and as nodes the logical constructors like $\vee, \wedge,\Rightarrow$ or quantifiers like $\forall x, \exists x$. There is a subtle point here, where one might need to talk about free vs bound variables, but this isn't usually a problem about meta-theoretical expressiveness, so I won't go into it.

4. A set of deductions $\cal D$ which express which statements are provable in the formal system under consideration (e.g. $\mathrm{PA}$). These are yet again trees, with logical axioms at the leaves (e.g. $x=x$) and as nodes an intermediate statement along with a deduction rule taken from some (finite) set of acceptable deductions. We often write $\vdash \phi$ instead of $\phi$ to denote that $\phi$ is the root of some deduction and not just some arbitrary sentence.

Now it is clear that to express the first incompleteness theorem, you only really need a theory about trees over some finite set of possible node types, and consistency is some statement like

There is no deduction with conclusion $\vdash 0 = S(0)$

This can be done using a vast variety of theories, including ZFC, but also the theory of finite sets (ZF + $\neg$Axiom of infinity) and, using Gödel encodings, the theory of arithmetic.

Modern computer interactive proof systems tend to have the notion of tree as a built-in, since they are so similar to the datatypes one encounters constantly in computer science. This makes expressing the first incompletness theorem particularly easy (but not proving it!), as is outlined in Coq here by Russel O'Connor.

I would add that the pain of using Gödel encodings is such that it makes the statements proofs of both incompleteness theorems unnecessarily convoluted, and is really just a historical accident due to excessive attention being given to natural numbers rather than the more natural (no pun intended) tree structure. Paulson carries out the full (formal) proof in the context of finite sets rather than $\mathrm{PA}$, as he describes in A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS.

I believe that what you're looking for is a development of Gödel's theorem in what we might call "the language of syntax" rather than "the language of arithmetic." The closest thing I'm aware of to what you want is Chapter 7 of Quine's book Mathematical Logic, in which he develops something he calls protosyntax. See also David Auerbach's article How to say things with formalisms, specifically the discussion starting on page 82 about the language of Syntax. Auerbach makes it clear that once you grasp the idea of how to go back and forth between arithmetic and syntax, there isn't really a need to write out in full a separate "syntactical development"; the standard arithmetic development already contains all the details, as long as you read it through the correct lens.