Robinson Arithmetic (Q) Proofs

[agapito]

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

 

[Evgeny.Makarov]

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?

 

[agapito]

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.

 

[Evgeny.Makarov]

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.

 

[agapito]

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.

 

[Evgeny.Makarov]

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.

 

[agapito]

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.

 

[Evgeny.Makarov]

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."