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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.