Talk:Diophantine set

Error in text

The main text says:

"One can also derive the following stronger form of Gödel's first incompleteness theorem from Matiyasevich's result: Corresponding to any given axiomatization of number theory, one can explicitly construct a Diophantine equation which has no solutions, but such that this fact cannot be proved within the given axiomatization."

This is not correct theorem, because a necessary condition is the axiomatization to be consistent. For a layman the difference may not seem to be huge, but for every logician, the difference is huge, and is exactly what makes wrong Penrose's writings on Gödel's theorem and mind. Nobody can look at given axiomatization and say "aha, this is consistent", and there is no algorithm for this to be decided. I hope the guy who wrote the text, repairs himself his own error. In simpler words, the constructed Diophantine equation will have solutions if the axiomatization is inconsistent. Danko Georgiev MD (talk) 05:41, 3 June 2009 (UTC)[reply]

Well, yeah, the theory obviously has to be consistent in order not to prove that the equation has no solutions (or any other statement for that matter). I gather that the statement is intentionally informal, as otherwise one should also insist that the axiomatization is recursive, that the theory should contain Robinson's arithmetic, and moreover, under the usual circumstances the equation is not constructed using just the axiomatization itself, but also its chosen

\Sigma _{1}^{0}

-formula which represents it in Q (different representations of the same axiomatization may yield nonequivalent ~~formulas~~equations). This is all hidden in the undefined term "axiomatization of number theory". If a theory is inconsistent, it is not an axiomatization of number theory. Furthermore, your reformulation does not make sense. If the theory is inconsistent, then it is pointless to proceed in the first place, but nothing stops us from arranging the construction so that the constructed equation has no solutions. Even if one does not design the construction explicitly with this goal, different constructions will yield different result. For example, if one uses the standard Rosser sentence, then whether it's true or false will depend on the chosen formalization of syntax and axiomatization of the theory. — Emil J. 10:36, 3 June 2009 (UTC)[reply]

Hi, Thanks very much for the "obvious" comment, however this is mathematical non-sense. If one is to say a mathematical theorem in Encyclopedia, one should formulate it exactly - moreover, I would recommend that all your "obvious requirements" BE INSERTED in the main text - I mean - the axiomatization must be [1] consistent, [2] recursive, and [3] powerful enough to express the idea of its own consistency - the so-called Hilbert-Bernays-Löb derivability conditions [I don't think consistency and other stuff should be in the form of footnote]. Encyclopedia is not generally written for logicians with Ph.D. but for arbitrary person who wants to find exact knowledge. And to state mathematical theorem in the original form was ridiculous. I have contributed some stuff to PlanetMath and Wikipedia, but due to some destructive and agressive editors I am now not contributing anything. p.s. Nothing is hidden in the term "axiomatization of number theory" - I can provide you exact quotations from at least 10 current textbooks, according to which axiomatization is axiomatization, and axiomatization can be consistent or not, for example nobody knows whether ZFC is consistent. I saw that you are mathematician, but what you write is far from what a real mathematician should write. Mathematics is not about "hidden things", sorry to teach you that Danko Georgiev MD (talk) 17:09, 7 June 2009 (UTC)[reply]

This is an encyclopedia, not a math monograph. It is often advisable for the benefit of the reader to use an informal presentation instead of the full formal statement, which may be incomprehensible for many (precisely because, in your own words, it's not written for logicians with Ph.D.) and involves a lot of irrelevant details, especially when it does not concern the main topic of the article (which in this case are diophantine sets, not Gödel's theorem). The reader who wants to learn about the details can, and is supposed to, look them up in the Gödel's incompleteness theorems article. — Emil J. 10:04, 8 June 2009 (UTC)[reply]

And by the way, the Hilbert–Bernays–Löb derivability conditions have nothing to do with it, you are confusing the two incompleteness theorems. — Emil J. 10:09, 8 June 2009 (UTC)[reply]

Are you sure that "Hilbert–Bernays–Löb derivability conditions have nothing to do with it"? In strong formal systems in which exponentiation is formally defined you can express the idea of consistency of the formal system (the link to the Hilbert–Bernays–Löb derivability conditions), in contrast weak formal systems in which exponentiation is not formalised might not lead to derivability of incompleteness theorems and these weak systems are provably complete. However, in order to construct Diophantine equations you need exponentiation, and I don't see what sense will make to speak about Diophantine sets in weak formal systems, which cannot formulate Diophantine equations at first place. Danko Georgiev MD (talk) 02:55, 9 June 2009 (UTC)[reply]

Congratulations, you just proved my point that you have absolutely no idea what you are talking about:

We are discussing Gödel's first incompleteness theorem (the one which states that certain theories are incomplete). It's standard proof only uses $\Sigma _{1}^{0}$ -completeness and the diagonalization lemma, not any derivability conditions. The Hilbert–Bernays–Löb derivability conditions are used in the proof of Gödel's second incompleteness theorem (the one which states that certain theories do not prove their own consistency).
You most definitely do not need exponentiation to express solvability of a Diophantine equation, since all exponents in the equation are fixed natural numbers, the variables for which you solve appear only in the bases. Solvability of any Diophantine equation can be written as an existential formula in the usual language of arithmetic (0, s, +, ×).
The Hilbert–Bernays–Löb derivability conditions may not be provable in weak theories, but the threshold for "weak" is much lower than exponentiation. The conditions are provable in "polynomial-time theories" like $S_{2}^{1}$ , which do not have exponentiation.
Contrary to popular belief, the Hilbert–Bernays–Löb derivability conditions are not needed literally to hold for the theory to be subject to Gödel's second incompleteness theorem anyway. The second incompleteness theorem holds essentially under the same conditions as the first one, i.e., for extensions of Robinson's arithmetic Q. It holds even in the strong sense that there is no consistent theory T such that T interprets Q + Con_τ, where τ is any $\Sigma _{1}^{0}$ -formula defining an axiom system for T in the standard model of arithmetic.

The last two points are however irrelevant, because they do not concern the first incompleteness theorem per point 1. — Emil J. 10:34, 9 June 2009 (UTC)[reply]

And don't confuse the "informal style" with "misleading style". If you like you can formulate in informal style all requirements for the theorem to work, but you cannot omit these requirements, and give the conclusion as if it follows from less premises than actually they are. Danko Georgiev MD (talk) 03:05, 9 June 2009 (UTC)[reply]

I searched the article history, and much to my amusement, I found that the offending statement concerning Gödel's first incompleteness theorem appears in the same formulation in the very first revision of the article (more precisely, of the Matiyasevich's theorem article, which was merged here) from August 2001[1], hence it is one of the oldest surviving bits of text in Wikipedia. During all those eight long years, nobody but you found the style "misleading". — Emil J. 10:34, 9 June 2009 (UTC)[reply]

Well, if your last post is correct, then it would follow that the derivability conditions and the exponentiation are not necessary requirements for a diophantine equation to have no solutions and this to be unprovable in the discussed axiomatization. I was thinking of the original Godel coding of formulas by numbers composed of multiplying the primes each put on the power corresponding to the code given to each basic symbol, etc. Thus I falsely concluded that exponentiation is necessary for the first Goedel theorem also. Still, this does not invalidate my first correct comment that the axiomatisation must be consistent in order the diophantine equation to have no solutions. I saw you commented that you are adding note for "formalists", but let me tell you that the very idea of number is strictly dependent on the axiomatization (in case you call yourself "intuitionist", or "platonist"). Mathematics is about what can be communicated e.g. between two reasonable human beings, and has nothing to do with what someone might have thought but others were not able to guess. Thanks for pointing places where I was wrong, rationality requires constinuous self-assesment. p.s. I was curious to read the axioms of Robinson arithmetic and that although it is quite weak it is incomplete. Danko Georgiev MD (talk) 11:44, 9 June 2009 (UTC)[reply]

Well, perhaps there is no harm in mentioning consistency, as any reader who knows what is an axiomatization presumably also knows what consistency means. However, I maintain that it would be counterproductive to include any further formal details of "axiomatization of number theory". There are enough links there for anybody interested to find out. Mathematics, just like any other science, is better communicated using ideas and concepts rather than formal definitions. Nobody is left at "guessing" anything, since, to stress it again, the formal details are just one click away. — Emil J. 14:34, 9 June 2009 (UTC)[reply]

The incompleteness theorems can be difficult to understand. I expanded the section with how this formulation relates to the original one. Nxavar (talk) 11:16, 12 December 2014 (UTC)[reply]

Reference ?

Is there a reference for the assertion in Note 3 of the article, "the mathematical community has moved to calling the equivalence result the MRDP theorem or the Davis-Putnam-Robinson-Matiyasevich theorem." Stephanwehner (talk) 23:01, 9 December 2011 (UTC)[reply]

I don't know if the "MRDP" name is used anywhere, but the (long) history of the result (and the contributions of each of the four) is discussed in the first ref given in Hilbert's tenth problem—Barry Cooper's Computability Theory. A quick google search suggests that Manin's A Course in Mathematical Logic for Mathematicians ISBN 978-1-4419-0614-4 uses this name for the theorem (on p. 207, but not abbreviating their names to the initial though); this was the 1st hit, there are others, e.g. [2], which has preview in GB. Tijfo098 (talk) 12:31, 8 November 2012 (UTC)[reply]

Martin Davis uses MRDP here and some independent sources do as well [3] [4]. Tijfo098 (talk) 12:42, 8 November 2012 (UTC)[reply]

“MRDP theorem” is commonly used in my experience, but I’m not sure this is as universal a convention as the note suggests. (The note could also make use of some punctuation.)—Emil J. 12:58, 8 November 2012 (UTC)[reply]

I've also heard MRDP theorem. I don't know if it's preferred, but it should at least be mentioned. I'll add something. 173.228.123.121 (talk) 06:27, 3 October 2017 (UTC)[reply]

Universal Diophantine set

Strangely, I do not see it here. See for instance Matiyasevich, Chapter 4. Boris Tsirelson (talk) 17:50, 17 February 2018 (UTC)[reply]