47
$\begingroup$

I understand Gödel's Incompleteness Theorems to be statements about effectively generated formal systems, which basically makes them theorems about algorithms. This is cool, because despite being very abstract, they actually constrain my expectations about how computers and human beings can behave. But, being theorems, what formal system are they theorems in? That is, what formal language is used to express them, how do I interpret that language as being about algorithms, what axioms are assumed, and what rules of inference are used to derive the incompleteness theorems?

I ask because I am looking for a better answer than "ZFC", which has been given to me in person a few times now. ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families…), at least not in the same way I believe in concrete things like computers and algorithms. I can see from skimming the proofs that I could probably make up a formal system in which the theorems could be expressed and proven, which did not refer to all the monstrosities of ZFC. I just want to know what standard, "simplest" formal system(s) can be used for this purpose.

$\endgroup$
8
  • 13
    $\begingroup$ PRA, en.wikipedia.org/wiki/Primitive_recursive_arithmetic, suffices. $\endgroup$ Jan 6, 2013 at 6:34
  • 3
    $\begingroup$ Also, note that the theorems apply to Robinson Arithmetic, which is weaker than Peano. $\endgroup$
    – David Roberts
    Jan 6, 2013 at 7:55
  • 2
    $\begingroup$ See also: mathoverflow.net/questions/55311/… $\endgroup$ Jan 6, 2013 at 19:48
  • 3
    $\begingroup$ @Andrew Critch: The article on the incompleteness theorems in the Handbook of Mathematical Logic, by Smorynski, has the details. Look for the term "formalized incompleteness theorem". $\endgroup$ Jan 6, 2013 at 23:21
  • 12
    $\begingroup$ @Andrew: Historically, there's a good reason why PRA suffices. In the background was lurking Hilbert's program to dispel doubts about infinitary set-theoretic reasoning by proving the consistency of set theory by finitary means. Since Goedel was claiming to demonstrate the impossibility of a finitary consistency proof (though not, initially, of set theory), he had good reasons to restrict his own arguments to finitary ones, to forestall criticism of his own proof. Your suspicions about infinitary reasoning are not new! $\endgroup$ Jan 7, 2013 at 4:08

5 Answers 5

47
$\begingroup$

As Andres Caicedo points out in his comment (to the Question), the modest fragment $\sf{PRA}$ (Primitive Recursive Arithmetic) of $\sf{PA}$ (Peano arithmetic) is already able to verify the incompleteness theorems.

Indeed, the proof of the Gödel–Rosser incompleteness proof is entirely syntactic and can be readily implemented in a fragment of $\sf{PRA}$ known as $I\Delta_0 + exp$, where $I\Delta_0$ is the weakening of $PA$ in which the induction scheme is only available for $\Delta_0$-formulas, and $exp$ asserts the totality of the exponential function $2^x$ (it is well-known that $I\Delta_0$ is unable to prove the totality of the exponential function).

It is worth noting that in the above $I\Delta_0 + exp$ can be even reduced to $I\Delta_0 + \Omega_1$, where $\Omega_1$ is the axiom asserting the totality of the function $2^{\left| x\right|^2 }$, where $\left| x\right|$ denotes the length of the binary expansion of $x$. The theory $I\Delta_0 + \Omega_1$ is commonly viewed as the weakest fragment of $\sf{PA}$ in which one can develop a workable "theory of syntax".

PS. As pointed out by Jeřábek, the incompleteness theorems can be implemented in even weaker systems.

$\endgroup$
9
  • 2
    $\begingroup$ Really $2^{|x|}$, not $2^{|x|^2}$? $\endgroup$
    – Goldstern
    Jan 6, 2013 at 12:54
  • 1
    $\begingroup$ Thanks for this! Is that grey box a quotation? If so, where from? Where would you recommend I get started reading about this? $\endgroup$ Jan 6, 2013 at 15:11
  • 6
    $\begingroup$ @Andrew: The second paragraph is not a quotation; the highlighting was used for journalistic reasons. The standard reference on the subject is the book "Metamathematics of First-Order Arithmetic" by Petr Hájek, and Pavel Pudlák (1998) [see the first chapter for $I\Delta_0 + exp$, and the last chapter for $I\Delta_0 + \Omega_1$]. This book is available on Project Euclid at projecteuclid.org/…. $\endgroup$
    – Ali Enayat
    Jan 6, 2013 at 16:15
  • 2
    $\begingroup$ @Ali: Goldstern is right. Your definition is an inessential variant of $x^2$, and is provably total in $I\Delta_0$. $\endgroup$ Jan 7, 2013 at 14:22
  • 4
    $\begingroup$ And of course, the incompleteness theorem is provable in much weaker fragments than $I\Delta_0+\Omega_1$, such as $\mathit{PV}_1$. $\endgroup$ Jan 7, 2013 at 14:26
17
$\begingroup$

You might already know this, but if you're looking for foundations of mathematics which are so weak that they don't prove the existence of non-r.e. sets, then you should study Simpson's book Subsystems of Second-Order Arithmetic, the "bible" of reverse mathematics. The weakest system in that book, RCA0, has as a model the recursive sets, and suffices for Goedel's first incompleteness theorem and even a weak version of Goedel's completeness theorem. More importantly, RCA0 suffices for a large amount of mathematics.

Simpson's book of course also investigates what can't be proved in RCA0. For example, Brouwer's fixed point theorem is unprovable in RCA0, roughly speaking because one can construct a continuous recursive map from the square into itself that has no recursive fixed point.

$\endgroup$
1
  • 1
    $\begingroup$ If the OP is averse not only to non-r.e. sets but also to non-recursive r.e. sets, then $\text{RCA}_0$ is indeed a good system for him to work with. His explicit mention of "non-r.e." leads me to suspect, though, that he might want to have all r.e. sets available, so he'd need a system where one cannot in general form the complement of a set of natural numbers. $\endgroup$ Jan 7, 2013 at 1:37
13
$\begingroup$

Here's a different way of looking at things. Use FPA to denote second-order Peano Arithmetic minus the Successor Axiom (the axiom which says that every natural number has a successor). FPA is neither weaker nor stronger than IΔ0+Ω1, since the latter assumes the Successor Axiom but assumes a weaker form of induction.

FPA can prove the First Incompleteness Theorem. Undoubtedly, fragments of FPA can as well.

More interesting is when one clarifies the nature of the logical system under metalogical study. Usually, the syntax of first-order logic is defined so that one can always concatenate two strings to form a larger one. E.g. one uses this principle in the Deduction Theorem, which is one of the first metalogical theorems one tends to prove. But this assumption, essentially equivalent to the Successor Axiom, is not necessary, and one can refrain from making it.

In this environment (where the syntax is not assumed to be unboundedly long), one can say this: FPA can prove the First Incompleteness Theorem. But Godel's proof seems only to work in the case of FPA + Successor Axiom. In the case FPA + not Successor Axiom, one basically formalizes the idea that a proof is generally longer than any axiom. It does not appear that Godel's proof of the Second Completeness Theorem goes through, and I do not know whether this can be repaired.

$\endgroup$
5
10
$\begingroup$

A very detailed, low-level proof of Gödel's incompleteness theorems is

  • S. Świerczkowski, Finite sets and Gödel’s incompleteness theorems, Dissertationes Mathematicae 422 (2003), 1-58, https://eudml.org/doc/285944

It's based on the theory of hereditarily finite sets, which is closely related to PA.

$\endgroup$
5
  • 1
    $\begingroup$ Several users consider this as a non-answer to the actual question. $\endgroup$
    – Todd Trimble
    Dec 24, 2013 at 23:26
  • 7
    $\begingroup$ This is not a non-answer. Świerczkowski shows that the proof of Gödel's theorem can be formalized in a set-theoretic system much weaker than ZFC, and this proof was the starting point for Lawrence Paulson's formalization of the theorem in Isabelle/HOL. See Paulson's paper, "A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets," which he seems to be too modest to mention himself. $\endgroup$ Dec 25, 2013 at 1:51
  • $\begingroup$ Thank you very much, @TimothyChow, for the clarification and information. $\endgroup$
    – Todd Trimble
    Dec 25, 2013 at 2:12
  • 1
    $\begingroup$ The link in this answer no longer works. $\endgroup$ Apr 24, 2019 at 13:20
  • 1
    $\begingroup$ @CarlMummert It still works for me. There's also a Wayback Machine copy. $\endgroup$ Apr 23, 2023 at 13:40
6
$\begingroup$

Looking at this question again, it seems to reveal misconceptions about how mathematics is done in general and how it was done by Gödel. The key phrase is "But, being theorems, what formal system are they theorems in? That is, what formal language is used to express them, how do I interpret that language as being about algorithms, what axioms are assumed, and what rules of inference are used to derive the incompleteness theorems?"

Although mathematics can be formalised, it isn't usually, and Gödel's work was no exception. He makes no explicit reference to any axioms or rules of inference except with respect to the formal system that his theorem is about. The very notion of an algorithm was unclear in 1931. The Church–Turing thesis was still many years away. Gödel relied on well-known and elementary properties of arithmetic and ordinary mathematical reasoning to arrive at his conclusions.

You also remark "ZFC refers to all sorts of things I don't believe exist (e.g. non recursively enumerable sets, choice functions for uncountable families...)". The word "exist" is ambiguous here, but almost everything in mathematics is problematical once you think deeply about it: non-computable real numbers, planes (infinite in extent, perfectly flat, infinitely thin), parallel lines.

$\endgroup$
1
  • 1
    $\begingroup$ Godel might not have been interested in identifying the weakest system in which his theorems can be proved, but we surely might be. $\endgroup$ Feb 15 at 23:29

Not the answer you're looking for? Browse other questions tagged or ask your own question.