Why Does Robinson Arithmetic (Q) Require Induction for O3 but Not O2?

In summary: One can prove O3 without invoking induction, but then one has to say something like "... and so on", so the proof becomes less precise. Similarly, I guess, one can use meta-theoretical induction in the proof of O2 because one has to construct a derivation that considers $n+1$ different cases $x=\bar{0},\ldots,x=\bar{n}$, and without induction one has to say, "continuing like this, ..." or something similar. The important point is that the resulting formal derivation does not contain the induction axiom.In summary, the author proves that O2 is not order-adequate by induction. Q3 is not proved by induction
  • #1
agapito
49
0
In Peter Smith's Godel book, 2 conditions are proven of several that make Q "order adequate"

O2: For any n, Q ⊢ ∀x ({x=0 v x=1 v...v x=n} → x≤n)

03: For any n, Q ⊢ ∀x (x≤ n → {x=0 v x=1 v...v x=n})

O3 is proved by induction. O2 is not. It would appear as if induction would be required in both cases.

Any guidance on why?

Many thanks, am
 
Technology news on Phys.org
  • #2
agapito said:
O3 is proved by induction. O2 is not. It would appear as if induction would be required in both cases.
Why do you think Q3 is proved by induction if Q does not include the induction axiom and the book says that all these properties are provable in Q?
 
  • #3
Evgeny.Makarov said:
Why do you think Q3 is proved by induction if Q does not include the induction axiom and the book says that all these properties are provable in Q?

Thanks for replying. I'm not sure I understand what you mean, can you please elucidate. Thanks again for helping me.
 
  • #4
agapito said:
O3 is proved by induction.
It was you who said that O3 is proved by induction. (I should have written O3 instead of Q3.) Why do you think so? Doesn't the book say that Robinson's arithmetic does not include induction axiom and still O3 is proved in Robinson's arithmetic? Induction is the main difference between Robinson's arithmetic and Peano arithmetic.
 
  • #5
Evgeny.Makarov said:
It was you who said that O3 is proved by induction. (I should have written O3 instead of Q3.) Why do you think so? Doesn't the book say that Robinson's arithmetic does not include induction axiom and still O3 is proved in Robinson's arithmetic? Induction is the main difference between Robinson's arithmetic and Peano arithmetic.
Author proves O3 by induction. In a case like this, should he have explicitly stated that the axiom of induction must be incorporated into Robinson's arithmetic? There is no indication of this in the text.

Also, how would one go about proving O3 without invoking induction? Alternatively, can O2 be proven by induction?

I greatly appreciate you helping me out with this, regards.
 
Last edited:
  • #6
agapito said:
Author proves O2 by induction.
Perhaps you mean he proved O3 by induction, as you said in the first post. This happens in section 11.8 in my book (An Introduction to Gödel’s Theorems, second edition, 2013). I was initially confused because in Section 11.3, where order-adequacy properties are introduced, the author says that their proofs are boring and does not seems to include them.

Now induction in the proof of O3 is meta-theoretical rather than a part of Robinson's arithmetic. That is, this induction is a part of the reasoning we use to prove claims about derivability of formulas in Q. You may note that the author says several times, "Arguing inside Q". This means that the part that follows can be converted into a formal derivation inside Q, and the English text is an outline of that derivation. In such case we can't use induction. But we can, for example, prove the claim $Q\vdash \forall x, y\;S^n x=S^n y\to x = y$ for every fixed natural number $n$ by meta-theoretical induction. That is, we prove that if there exists a derivation of $\forall x, y\;S^n x=S^n y\to x = y$, then there exists another derivation of $\forall x, y\;S^{n+1} x=S^{n+1} y\to x = y$. Neither derivation includes the axiom of induction because it is not listed in axioms of Q in Section 10.3.

One can prove O3 without invoking induction, but then one has to say something like "... and so on", so the proof becomes less precise. Similarly, I guess, one can use meta-theoretical induction in the proof of O2 because one has to construct a derivation that considers $n+1$ different cases $x=\bar{0},\ldots,x=\bar{n}$, and without induction one has to say, "continuing like this, ..." or something similar. The important point is that the resulting formal derivation does not contain the induction axiom.

In the future, please refer to precise places in the book that you are asking about.
 
  • #7
Evgeny.Makarov said:
Perhaps you mean he proved O3 by induction, as you said in the first post. This happens in section 11.8 in my book (An Introduction to Gödel’s Theorems, second edition, 2013). I was initially confused because in Section 11.3, where order-adequacy properties are introduced, the author says that their proofs are boring and does not seems to include them.

Now induction in the proof of O3 is meta-theoretical rather than a part of Robinson's arithmetic. That is, this induction is a part of the reasoning we use to prove claims about derivability of formulas in Q. You may note that the author says several times, "Arguing inside Q". This means that the part that follows can be converted into a formal derivation inside Q, and the English text is an outline of that derivation. In such case we can't use induction. But we can, for example, prove the claim $Q\vdash \forall x, y\;S^n x=S^n y\to x = y$ for every fixed natural number $n$ by meta-theoretical induction. That is, we prove that if there exists a derivation of $\forall x, y\;S^n x=S^n y\to x = y$, then there exists another derivation of $\forall x, y\;S^{n+1} x=S^{n+1} y\to x = y$. Neither derivation includes the axiom of induction because it is not listed in axioms of Q in Section 10.3.

One can prove O3 without invoking induction, but then one has to say something like "... and so on", so the proof becomes less precise. Similarly, I guess, one can use meta-theoretical induction in the proof of O2 because one has to construct a derivation that considers $n+1$ different cases $x=\bar{0},\ldots,x=\bar{n}$, and without induction one has to say, "continuing like this, ..." or something similar. The important point is that the resulting formal derivation does not contain the induction axiom.

In the future, please refer to precise places in the book that you are asking about.

I will be more precise in the future in referring to the book.

I really appreciate you explaining this. It's sometimes difficult for me to separate proofs in both systems (formal and meta) and how they relate to each other. Your help is invaluable and I thank you for it.

As you are familiar with Smith's book, do you consider it an effective way to begin to learn this subject or are others more highly recommended?

Thanks again, best regards.
 
  • #8
In fact, I have not read Smith's book, and I've only seen section 10-12, but I liked them. So it's probably not the worst source to study Gödel's theorem. There is also "Gödel Without (Too Many) Tears" book and Open Logic project, but I am not familiar with them, either. Another classical book is Computability and Logic by Boolos and Jeffrey, but while it is thorough, in my opinion it does not put an emphasis on making clear the idea behind the proof. It reminds me a description by Gregory Chaitin (one of the discoverers of algorithmic complexity) of Gödel's proof itself in the book "Meta Math!": "Why couldn't I understand Gödel's proof? Well, I could follow it step by step, but it was like trying to mix oil and water. My mind kept resisting. In other words, I didn't lack the necessary intelligence, I just plain didn't like Gödel's proof of his fabulous result. His original proof seemed too complicated, too fragile! It didn't seem to get to the heart of the matter, because it was far from clear how prevalent incompleteness might in fact be."
 

FAQ: Why Does Robinson Arithmetic (Q) Require Induction for O3 but Not O2?

1. What is Robinson Arithmetic (Q)?

Robinson Arithmetic (Q) is a formal system of arithmetic developed by mathematician Raphael Robinson in the 1940s. It is a simplified version of Peano Arithmetic (PA) and is used to study the foundations of mathematics.

2. What are "Q Proofs"?

"Q Proofs" are formal proofs within the Robinson Arithmetic system. They involve using the axioms and rules of inference in Q to demonstrate the validity of mathematical statements.

3. How does Robinson Arithmetic differ from Peano Arithmetic?

Robinson Arithmetic is a subset of Peano Arithmetic, meaning it contains fewer axioms and rules of inference. This makes it a simpler system to work with and study, but it also means that not all statements provable in PA can be proven in Q.

4. What are some applications of Robinson Arithmetic?

Robinson Arithmetic is primarily used in the study of foundations of mathematics, specifically in the area of logic. It has also been used in the development of computer programs to assist in formal mathematical proofs.

5. Are there any limitations to Robinson Arithmetic?

Yes, Robinson Arithmetic is not a complete system and cannot prove all statements that can be proven in Peano Arithmetic. It also does not have the same expressive power as PA, meaning some mathematical concepts cannot be fully represented or studied in Q.

Similar threads

Replies
10
Views
2K
Replies
32
Views
4K
Replies
5
Views
2K
Replies
6
Views
2K
Replies
1
Views
1K
Back
Top