Talk:Robinson arithmetic

Identity (Logic)

The link target for 'identity' in the first sentence under 'Axioms' points to Identity (mathematics) that doesn't really cover identity in the sense of 'first order logic with identity' (versus without identity). I think we either need to add a section to that article, or retarget this link to a more relevant location (possibly a new as-yet unwritten article?) Does anyone more familiar than I know of a more appropriate place? Zero sharp (talk) 05:37, 4 April 2008 (UTC)

I don't know of one on Wikipedia, but I am planning to rework the first order logic article, so I will try to keep this in mind when I do it. — Carl (CBM · talk) 13:38, 4 April 2008 (UTC)

Great, thanks Carl. Zero sharp (talk) 18:43, 4 April 2008 (UTC)

Presburger arithmetic

The article states that Q with any of the axioms removed is not essentially undecidable (any extension in the same language is also undecidable), this is quite true, but then goes on to state that some of its subtheories obtained by removing some of the states axioms are decidable - in particular, that one such subtheory is equivalent to Presburger arithmetic and so is decidable. This is simply incorrect, since any finitely axiomatizable, essentially undecidable theory is also hereditarily undecidable (any subtheory in the same language is also undecidable). The languages of Q and Presburger arithmetic are different (Presburger arithmetic doesn't have multiplication), so I don't think it makes sense to talk about them in this way. Should this be removed? (This is my first time doing this sort of thing, so I feel a little uneasy about altering things myself.) Jimbobbibliobus (talk) 21:13, 31 August 2008 (UTC)

Any serious university library should have a copy of Tarski et al (1953). Check it out and see if the entry does justice to what Tarski wrote. Incidentally, Pressburger arithmetic is not a subtheory of Q because Q lacks induction.123.255.28.93 (talk) 15:25, 4 December 2008 (UTC)

You are quite right, Jimbobbibliobus. — Emil J. 14:39, 5 December 2008 (UTC)

Addition Eliminable

There is an issue in the given interpretation of +. Specifically, since * is not associative in some models of Q, the parentheses should be included, or there it should be verified that they are irrelevant in this case. Thank you. Hitorikii (talk) 05:13, 2 December 2008 (UTC)

This section is based wholly on Boolos and Jeffrey. This definability of addition in terms of product and successor was discovered by Tarski. It is my understanding that product associates, given the intended interpretation of Q, although the general case is unprovable, because induction is lacking. I know nothing about models of Q in which product does not associate.

What I do not understand is how fragments of Q lacking the recursive definition of addition are uninteresting, given that addition is definable. Tarski et al (1953) asserted that all fragments of Q are either decidable, or have uninteresting models.123.255.28.93 (talk) 15:17, 4 December 2008 (UTC)

Peano axioms

I changed a sentence saying something like "Q, like the Peano axioms, has non-standard models of all infinite cardinalities" to say Peano arithmetic instead of Peano axioms. I usually think of "Peano axioms" as meaning the 19th century version which has a single induction axiom in full second-order logic, and which has no nonstandard models, while "Peano arithmetic" is the first-order axiomitization an infinite schema of induction axioms. I hope this change was appropriate -- please feel free to comment, I'm not any kind of expert. 66.127.55.192 (talk) 20:30, 18 January 2010 (UTC)

Robinson arithmetic

I noticed that Robinson arithmetic was the subject of some edits on the article. I was interested in that subject earlier this year, and when I looked into it this is what I found:

• Of course Q is strong enough for the standard proof of the first incompleteness theorem. This is what it was designed for, after all.
• The common belief among experts is that Q does not prove the Hilbert–Bernays derivability conditions that are needed for the standard proof of the second incompleteness theorem. However, there is no published proof that any particular derivability condition is not provable in Q. This was discussed on the FOM email list in September 2010.
• Nevertheless, there is an alternate proof that Q does not, in fact, prove Con(Q). In this limited sense, the second incompleteness theorem holds for Q. I believe that the first proof that Q does not prove Con(Q) is due to A. Bezboruah and J. C. Shepherdson, "Gödel's Second Incompleteness Theorem for Q", The Journal of Symbolic Logic Vol. 41, No. 2 (Jun., 1976), pp. 503-512, JStor

Regarding this edit [1], I have a slight quibble. The usual statement of the second incompleteness theorem includes as a hypothesis that the theory is able to prove the Hilbert–Bernays conditions (so "contains enough arithmetic" in the statement of the 2nd theorem is a stronger assumption than "contains enough arithmetic" in the statement of the 1st theorem). Therefore, as it is usually stated, the second incompleteness theorem does not apply to Q, because Q doesn't meet the hypotheses of the theorem. In my opinion the paragraph in the article beginning "Gödel's theorems only apply to axiomatic systems defining sufficient arithmetic to carry out the coding constructions " doesn't clearly distinguish between the hypotheses of the first and second theorems. I will try to edit the article to take this into account. — Carl (CBM · talk) 15:10, 2 December 2010 (UTC)

What do you mean by the "usual statement of the second incompleteness theorem"? As far as I am aware, the usual statement of the second incompleteness theorem is that for any consistent theory T containing <insert-your-favourite-theory-here> and every $\Sigma _{1}$-formula τ defining an axiom set for T in N, T does not prove Con_τ. The Hilbert–Bernays conditions are only used in the proof, not in the statement.—Emil J. 15:20, 2 December 2010 (UTC)

The theory is often left unspecified in the statement, but the <insert-your-favourite-theory-here> for the second incompleteness theorem isn't Q, it's something stronger than Q. By analogy, if I state a theorem in analysis with "any sufficiently smooth function has property X" and then in the proof I use the third derivative, what I really assumed in the hypotheses was that the function is 3 times differentiable. If I later prove that some particular function that is only once differentiable has property X, I cannot say that this new result was a consequence of my original theorem, since the original theorem only applied to functions that were 3 times differentiable.

For example, in Smorynski's article in the Handbook of mathematical logic, he lists three theories that can play the role of <insert-your-favourite-theory-here>: PRA, PA, and ZFC. When discussing the requirements of the second incompleteness theorem on p. 839, he emphasizes that for the second theorem "mere binumerability of the primitive recursive relations" is not sufficient. That "mere binumerability" is exactly what we get with Q.

In Pudlák and Hájek's book on p. 164 their statement of the second incompleteness theorem begins:

Let T be a theory containing Q and let π be a Σ₁ definition of the set of all T-provable formulas satisfying the provability conditions. Then ...

That statement doesn't apply to Q because Q does not verify the derivablity conditions for any Σ₁ definition of its provable formulas (or, at least, everyone believes that it doesn't). — Carl (CBM · talk) 15:37, 2 December 2010 (UTC)

I don't follow what you are trying to say. That Q is usually not employed as the <insert-your-favourite-theory-here> is because it requires a more complicated proof than for a stronger base theory (basically, you need to interpret in the theory a decent fragment of bounded arithmetic like $S_{2}^{1}$ on a cut, prove Hilbert–Bernays conditions for this fragment, and then use a variant of the standard diagonalization argument), and because there is a popular misconception that it can't be used. However, the statement is true with Q as the base theory. I don't know what exactly is the claim in Bezboruah and Shepherdson, but the Pudlák article I linked does state it in that form (well, he actually states it for finitely axiomatized theories, but there is no deep reason behind that).—Emil J. 15:51, 2 December 2010 (UTC)

Also, you are looking at the wrong chapter in Hájek and Pudlák. The second incompleteness theorem for extensions of Q (or rather, its strengthening in terms of restricted provability) is Thm. 5.28 (ii) on page 387.—Emil J. 16:03, 2 December 2010 (UTC)

(Edit conflict) Exactly – my point is that the theorem that they call the "Goedel's second incompleteness theorem" is the one on p.164. I wrote the following while you were writing.

Before I respond too much, I want to say I think we can find a wording in the article that is acceptable without resolving this disagreement, which is linguistic and not mathematical. I was satisfied with the wording you added after I made just a few cosmetic changes.

My opinion is that the standard, textbook statement of the second incompleteness theorem is the one that assumes the derivability conditions. So the proof that Pudlak gives is not what is usually called the "second incompleteness theorem" – it's a distinct, stronger theorem. This is parallel to how the Nagata–Smirnov metrization theorem is distinct from Urysohn's metrization theorem. Unfortunately, the situation we have in logic is like a world where Urysohn's theorem is commonly stated as "Any topological space with enough properties is metrizable".

In particular, I think that when we say "second incompleteness theorem" in an article we should assume readers will think of the theorem that assumes the derivability conditions. I think that this confusion is what led Grudeu to make the edits that he or she make to the article. I'm not saying that our articles should take a position on which theorem is "really" the incompleteness theorem, just that our articles should be written in a way that accommodates readers who are only familiar with the theorem stated in terms of the derivability conditions. — Carl (CBM · talk) 16:18, 2 December 2010 (UTC)

I don't think the analogy with Urysohn's metrization theorem works. What is called "second incompleteness theorem" is in any case different from Gödel's formulation, the statement has been generalized by relaxing the assumptions, so it's a kind of double standard to disallow another relaxation of the assumptions in the same spirit. But I can see what you mean. I am happy with the current formulation.—Emil J. 17:48, 2 December 2010 (UTC)

Addition eliminable

I am concerned about this subsection. Ignoring the fact that the link to Skolem arithmetic seems to go to an unintended target, I do not see how it is relevant to Robinson's arithmetic. The given definition of + in terms of S and · relies on basic properties like commutativity and associativity of + and ·, distributivity, and most importantly, cancelativity of + and ·. None of these are provable in Robinson's arithmetic. I'm fairly certain that + is not definable in terms of S and · in Q.—Emil J. 17:48, 2 December 2010 (UTC)

I went ahead and removed it. I don't have the edition of the reference that was cited (the 4th edition), but I was able to see the cited page on google books and it doesn't include the fact claimed. The 5th version, which I do have, also says nothing. So I can't say if this was a misreading of the reference or what, but in any case I agree with removing the section. For reference the text was added here [2] and the reference was tweaked here [3]. — Carl (CBM · talk) 21:00, 2 December 2010 (UTC)

I assume the IP simply didn't appreciate the difference between definability in the standard model of arithmetic and definability in a weak theory like Q.—Emil J. 13:25, 3 December 2010 (UTC)

Definable cut

In the clause "even if we additionally restrict Gödel numbers of proofs to a definable cut" what does "definable cut" mean? — Preceding unsigned comment added by 213.122.49.134 (talk) 21:52, 7 June 2012 (UTC)

A formula I(x) such that the theory proves I(0), $I(x)\to I(x+1)$, and $I(x)\land y\leq x\to I(y)$.—Emil J. 13:11, 8 June 2012 (UTC)

Dropping the axiom (3)

The author wrote: "... when any one of the seven axioms above is dropped. These fragments of Q ... have ... uninteresting models (i.e., models which do not extend the standard natural numbers)".

How can it be true? Let us drop the axiom (3). However, every term in form of "1+ ... +1" represents a natural number, and it's provable, that different such terms are not equal. That is, all standard natural numbers are contained in any given model of the theory, aren't they?

Eugepros (talk) 09:13, 6 July 2012 (UTC)

The sentence does not imply that the theory minus each one of the axioms should have uninteresting models, only that it does not satisfy Gödel’s theorems, and anyway the word is used here informally. However, for more clarity I changed extension to end-extension (one of the uninteresting models of Q minus (3) are the nonnegative reals).—Emil J. 11:59, 6 July 2012 (UTC)

Thank you, Emil, I understand. And one more: Could you say something about what the axiom (3) is necessary for? If I understand it right, the axiom (3) is a "weaker" replacement of induction scheme. But it doesn't make possible inductive inference. It excludes such models as nonnegative reals, but in my opinion such models are not worse than models with nonstandard numbers. Perhaps, not all computable functions are representable in the theory without the axiom (3), unlike Q? Is there an example of computable function, which is not representable in such theory?

Eugepros (talk) 06:24, 9 July 2012 (UTC)

The reals are decidable, and the only functions representable in them are piecewise algebraic. See real closed field#Model Theory: decidability and quantifier elimination.—Emil J. 13:30, 9 July 2012 (UTC)

Emil, maybe I'm going beyond the scope of the article, but it's interesting subject to be noted somewhere: If I'm not mistaken, the existence of decidable extention of the theory means inapplicability of the 1st Goedel's incompleteness theorem to the theory, doesn't it? And it's interesting where exactly Goedel's proof fails: To implement Goedel's numbering and formula of provability we should express factorization by formula of arithmetic. And it's very strange why this expression doesn't work without the axiom (3).

Eugepros (talk) 09:26, 10 July 2012 (UTC)

I understand! Without the axiom (3) we cannot prove, that prime numbers exist: So, the number 3 has dividers other than 1 and 3 - for example, 2 and 1.5 (in the model of nonnegative reals). Am I right?

Eugepros (talk) 09:46, 10 July 2012 (UTC)

What you write is correct. However, I would say that in the nowadays common proof of Gödel’s first incompleteness theorem using representability of computable functions or r.e. sets, the most fundamental property that fails without (3) is $\Sigma _{1}^{0}$-completeness of the theory: in order to show that a true bounded sentence of the form $\forall x\leq {\overline {n}}\cdots$ is provable in Q (where ${\overline {n}}$ denotes the numeral of n), you need Q to prove the formula $\forall x\,(x\leq {\overline {n}}\to x={\overline {0}}\lor x={\overline {1}}\lor \dots \lor x={\overline {n}})$, and this is impossible without (3).—Emil J. 12:03, 10 July 2012 (UTC)

Weaker theories

There is an ambiguity concerning the notion of weakness at the beginning of the article. An opening sentence reads, "Since Q is weaker than PA, it is incomplete." However, the article on Presberger arithmetic states, "Presburger arithmetic is much weaker than Peano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Presburger arithmetic is a decidable theory." That article goes on to state that Presberger arithmetic is "...complete: For each statement in Presburger arithmetic, either it is possible to deduce it from the axioms or it is possible to deduce its negation." It is true that the languages of these theories differ. My point is that the precise sense of 'weaker' intended here should be stated at the beginning of this article. FLengye| (ta|k) 23:48, 6 February 2013 (UTC)

I see that the question of weakness is the subject of edit reversions. The opening sentences of this article may not provide sufficient context for the statement in question, as the notion of a fragment of first-order arithmetic is not defined within Wikipedia. Buss defines a fragment of first-order arithmetic as an axiomatizable subtheory of first-order arithmetic in his chapter of the Proof Theory of Arithmetic. This definition might exclude the possibility that the subtheory contains no formula in which the multiplication symbol occurs. Some authors define a fragment of a theory to be a "syntactically restricted subset of formulae of the theory." In this sense, both Robinson's arithmetic and Presberger's arithmetic are fragments of Peano Arithmetic. This may not be what experts in the proof theory of arithmetic intend; nevertheless, there are references in the literature to both decidable and undecidable fragments of undecidable theories. The Wikipedia article on First-Order Logic contains examples of fragments in which the language is restricted: "For instance, first-order logic is undecidable, meaning a sound, complete and terminating decision algorithm is impossible. This has led to the study of interesting decidable fragments such as C₂, first-order logic with two variables and the counting quantifiers $\exists ^{\geq n}$ and $\exists ^{\leq n}$ (these quantifiers are, respectively, "there exists at least n" and "there exists at most n") (Horrocks 2010)." FLengye| (ta|k) 00:56, 7 February 2013 (UTC) FLeℵgyel (ta|k) 20:57, 4 June 2013 (UTC)

I for one think we should find a way to resolve these issues - but without too much verbiage. They do present a possibility for confusing someone who browses these articles. — Carl (CBM · talk) 01:01, 7 February 2013 (UTC)

I for one am certainly confused by the statement about weakness. Usually I see incompleteness described as a property of theories that are sufficiently strong. - Crisperdue (talk) 17:17, 4 September 2013 (UTC)

That’s the wrong way to think about it. Immediately from the definition, any subtheory of an incomplete theory that has the same language is also incomplete. Essential incompleteness (i.e., having no recursively axiomatizable complete extension) is preserved upwards, but that’s a different matter.—Emil J. 20:52, 4 September 2013 (UTC)

Mendelson's arithmetic

There is more than one reference to Mendelson's textbook, but that deals with a theory stronger than Q (though still weaker than PA). 86.132.221.167 (talk) 15:59, 21 November 2017 (UTC)

but the general statement x + y = y + x is not. Similarly, one cannot prove that Sx ≠ x

But with this statement it is proveble, two symbols are not one symbol just as x is not on the position of y....... Jonaw2024 (talk) 19:02, 5 June 2023 (UTC)

I'm not sure I fully understood your above posting. Do you have particular suggestions what to improve in the article and how? - Jochen Burghardt (talk) 20:33, 5 June 2023 (UTC)