I Gödel's 1st Incompleteness Thm: Min Arithmetic Req'd?

  • I
  • Thread starter Thread starter nomadreid
  • Start date Start date
  • Tags Tags
    Arithmetic Theorem
AI Thread Summary
Gödel's First Incompleteness Theorem requires a consistent theory of numbers that includes a sufficient fragment of elementary arithmetic, with Robinson's Q being a candidate for the minimum requirement. Robinson Arithmetic is noted as sufficient for the theorem's proof, but there is uncertainty about whether any of its axioms can be omitted without affecting the theorem's validity. Tarski, Mostowski, and Robinson's work indicates that while Robinson's arithmetic is the weakest finitely axiomatizable undecidable theory, there exists a weaker, non-finitely axiomatizable theory, referred to as R, which is also essentially undecidable. R's axioms are derivable from Q, and it is shown that every recursive function is definable in R, leading to its incompleteness. The discussion highlights the complexities of the foundational requirements for Gödel's theorem and the accessibility of relevant literature.
nomadreid
Gold Member
Messages
1,750
Reaction score
243
I often read (for example, in Wikipedia on "Rosser's Trick") that in order for a proof of Gödel's First Incompleteness Theorem, one assumes an efficient consistent theory of numbers which includes a "sufficient fragment of elementary arithmetic". What minimum would qualify? Is Robinson's Q a minimum? (Among others, obviously.)
 
Physics news on Phys.org
Robinson Arithmetic is certainly sufficient, and is what is used in the versions of the proof that I have read.
I don't know if any of the Robinson axioms can be removed while still leaving the incompleteness theorem in place. My guess would be No, but I've never seen any investigation of it.
 
  • Like
Likes nomadreid
I suggest reading Tarski, Mostowski, and Robinson's Undecidable Theories, which shows that (a) Robinson's arithmetic is the weakest finitely axiomatizable theory which is essentially undecidable (cf. Theorem 11, where they prove that the omission of any of its seven axioms makes the theory decidable); (b) there is, however, a weaker theory which is not finitely axiomatizable and which is also essentially undecidable (they call it R in their paper). Using ##\Delta_n## as an abbreviation of ##S(S(\dots(0)))## (the successor function applied n times to 0), the axioms for R consist in the following schema (p. 53):

1. ##\Delta_p + \Delta_q = \Delta_{p+q}##;
2. ##\Delta_p \times \Delta_q = \Delta_{p \times q}##;
3. For each ##p, q## such that ##p \not =q##, ##\Delta_p \not = \Delta_q##;
4. ##x \leq \Delta_p \rightarrow x = \Delta_0 \vee \dots \vee x = \Delta_p##;
5. ##x \leq \Delta_p \vee \Delta_p \leq x##.

On pages 53-54, they show that all these axioms are derivable from Q (that is, Robinson's Arithmetic), thus, that R is weaker than Q. Next, they prove (Theorem 6) that every recursive function is definable in R. This, coupled with Corollary 2 (if T is a consistent theory in which all recursive functions are definable, then T is essentially undecidable), gives the result that R is essentially undecidable. Notice that, since R is recursively axiomatizable, it follows, by Turing's theorem (if a theory is recursively axiomatizable and complete, it is decidable), that it is incomplete.
 
  • Like
Likes PeroK, nomadreid, andrewkirk and 1 other person
Very interesting and extremely helpful, Nagase. I shall see if I can get hold of a copy. Thanks a million.
 
nomadreid said:
Very interesting and extremely helpful, Nagase. I shall see if I can get hold of a copy. Thanks a million.

You're welcome. Fortunately, the book is available as a very cheap Dover paperback, so it won't cost you much!
 
  • Like
Likes nomadreid
Nagase, you make the assumption that I am in a place where I have easy access to the purchase of Dover paperbacks. Since I am in a place where English is not an official language, there are only three ways to get such books: ordering from abroad (and sometimes the shipping is more than the book:))), or getting it online (which I have managed to do :smile:) or to find it in one of the obscure little bookshops carrying used English books (given that these bookshops contain mainly detective and romance fiction, the probability here is less than the proverbial epsilon).
 
I'm taking a look at intuitionistic propositional logic (IPL). Basically it exclude Double Negation Elimination (DNE) from the set of axiom schemas replacing it with Ex falso quodlibet: ⊥ → p for any proposition p (including both atomic and composite propositions). In IPL, for instance, the Law of Excluded Middle (LEM) p ∨ ¬p is no longer a theorem. My question: aside from the logic formal perspective, is IPL supposed to model/address some specific "kind of world" ? Thanks.
I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema): $$\begin{align} & (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\ & (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\ & (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\ & (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\ & (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\ & (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber...
Back
Top