47

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.

LSpice
  • 11,423
Andrew Critch
  • 11,060
  • 13
    PRA, http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic, suffices. – Andrés E. Caicedo Jan 06 '13 at 06:34
  • 3
    Also, note that the theorems apply to Robinson Arithmetic, which is weaker than Peano. – David Roberts Jan 06 '13 at 07:55
  • 1
    Thanks for this! Could you recommend me a good reference for reducing proof theory to PRA? (Though Godel's proofs are a clear illustration of how one can do it.) It's a bet weird that the Wikipedia article on Proof Theory has nothing about what foundations it uses, but the PRA article at least mentions that it's used as a foundation of proof theory... – Andrew Critch Jan 06 '13 at 15:12
  • 2
    See also: http://mathoverflow.net/questions/55311/subsystems-of-peano-arithmetic-and-incompleteness-theorem – Andrés E. Caicedo Jan 06 '13 at 19:48
  • 3
    @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". – Carl Mummert Jan 06 '13 at 23:21
  • 12
    @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! – Timothy Chow Jan 07 '13 at 04:08
  • @Andrew, although it is often mentioned that PA or PRA suffices, it is very hard to find the right material that tells how. There are some tricks to go from numbers to more complex datastructures and proves of that. Loops in programs can be rather easily expressed in closures. But, then you need the basic properties of closures. See for a detailed build of theorems:

    http://www.staff.science.uu.nl/~ooste110/syllabi/peanomoeder.pdf

     – Lucas K. Jan 08 '13 at 21:46
  • A minor point that I think is worth mentioning is that PRA still in some sense can talk about non-r.e. sets of natural numbers. They are definable in it (although they're not first-class objects of course). – James Hanson Nov 27 '23 at 15:49

5 Answers5

47

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.

Zuhair Al-Johar
  • 9,152
Ali Enayat
  • 17,058
  • 2
    Really $2^{|x|}$, not $2^{|x|^2}$? – Goldstern Jan 06 '13 at 12:54
  • 1
    Thanks for this! Is that grey box a quotation? If so, where from? Where would you recommend I get started reading about this? – Andrew Critch Jan 06 '13 at 15:11
  • 6
    @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 http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.pl/1235421926. – Ali Enayat Jan 06 '13 at 16:15
  • 1
    @Martin: Thanks, I fixed the def. of $\Omega_1$. The right one is between what I had written and what you suggested; see p.272 of the Hájek-Pudlák text mentioned in my comment to Andrew (it is in Ch. V of the book). – Ali Enayat Jan 06 '13 at 16:23
  • 2
    @Ali: Goldstern is right. Your definition is an inessential variant of $x^2$, and is provably total in $I\Delta_0$. – Emil Jeřábek Jan 07 '13 at 14:22
  • 4
    And of course, the incompleteness theorem is provable in much weaker fragments than $I\Delta_0+\Omega_1$, such as $\mathit{PV}_1$. – Emil Jeřábek Jan 07 '13 at 14:26
  • @Emil: thanks for your comments. I will add a note on the answer. – Ali Enayat Jan 07 '13 at 18:34
  • 1
    Ali, the totality of $2^{2|x|}$ is not an equivalent formulation of $\Omega_1$, it is simply wrong. I think you are confused by the fact that the subscripts of $\omega_i$ in Hájek and Pudlák are off by one from both the usual convention and from the subscripts in $\Omega_i$. – Emil Jeřábek Jan 07 '13 at 19:00
  • @Emil: thanks again; comedy of errors at work. – Ali Enayat Jan 07 '13 at 21:42
17

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.

Timothy Chow
  • 78,129
  • 1
    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. – Andreas Blass Jan 07 '13 at 01:37
13

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.

abo
  • 1,844
10

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.

Timothy Chow
  • 78,129
Lawrence Paulson
  • 531
  • 1
    Several users consider this as a non-answer to the actual question. – Todd Trimble Dec 24 '13 at 23:26
  • 7
    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. – Timothy Chow Dec 25 '13 at 01:51
  • Thank you very much, @TimothyChow, for the clarification and information. – Todd Trimble Dec 25 '13 at 02:12
  • 1
    The link in this answer no longer works. – Carl Mummert Apr 24 '19 at 13:20
  • 1
    @CarlMummert It still works for me. There's also a Wayback Machine copy. – Timothy Chow Apr 23 '23 at 13:40
6

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.

Lawrence Paulson
  • 531
  • 1
    Godel might not have been interested in identifying the weakest system in which his theorems can be proved, but we surely might be. – provocateur Feb 15 '24 at 23:29