242:
axiomatization must be consistent, recursive, and powerful enough to express the idea of its own consistency - the so-called
Hilbert-Bernays-Löb derivability conditions . 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 Knowledge, 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
533:
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
84:
74:
53:
229:
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. —
22:
172:. 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,
701:
165:"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."
551:
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
365:
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
228:
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,
532:
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
191:
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
256:
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
405:
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
241:
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
552:
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. —
487:
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.
510:
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
369:
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
590:
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."
140:
293:
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
297:
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
452:
356:
222:
666:“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.)—
192:
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
606:
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
400:
358:-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
261:(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
732:
130:
518:, hence it is one of the oldest surviving bits of text in Knowledge. During all those eight long years, nobody but you found the style "misleading". —
727:
624:
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.
277:
And by the way, the
Hilbert–Bernays–Löb derivability conditions have nothing to do with it, you are confusing the two incompleteness theorems. —
106:
681:
621:
564:
The incompleteness theorems can be difficult to understand. I expanded the section with how this formulation relates to the original one.
262:
97:
58:
289:
Are you sure that "Hilbert–Bernays–Löb derivability conditions have nothing to do with it"? In strong formal systems in which
680:
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.
463:
The last two points are however irrelevant, because they do not concern the first incompleteness theorem per point 1. —
33:
542:
493:
310:
301:, and I don't see what sense will make to speak about Diophantine sets in weak formal systems, which cannot formulate
247:
181:
326:
incompleteness theorem (the one which states that certain theories are incomplete). It's standard proof only uses
685:
224:-formula which represents it in Q (different representations of the same axiomatization may yield nonequivalent
607:
21:
512:
596:
406:
extensions of
Robinson's arithmetic Q. It holds even in the strong sense that there is no consistent theory
538:
489:
306:
243:
177:
39:
362:
incompleteness theorem (the one which states that certain theories do not prove their own consistency).
319:
Congratulations, you just proved my point that you have absolutely no idea what you are talking about:
83:
302:
425:
329:
195:
534:
105:
on Knowledge. If you would like to participate, please visit the project page, where you can join
655:
632:
592:
565:
89:
73:
52:
618:
373:
174:
the constructed Diophantine equation will have solutions if the axiomatization is inconsistent
648:
646:
709:
625:
569:
670:
556:
522:
467:
281:
269:
233:
298:
294:
290:
168:
This is not correct theorem, because a necessary condition is the axiomatization to be
721:
651:
628:
642:
516:
705:
102:
667:
553:
519:
464:
278:
266:
230:
79:
713:
689:
673:
659:
636:
600:
573:
559:
546:
525:
497:
470:
314:
284:
272:
251:
236:
185:
15:
257:
involves a lot of irrelevant details, especially when it
537:
and that although it is quite weak it is incomplete.
428:
376:
332:
198:
101:, a collaborative effort to improve the coverage of
700:Strangely, I do not see it here. See for instance
446:
394:
350:
216:
616:A Course in Mathematical Logic for Mathematicians
366:in the usual language of arithmetic (0, s, +, Ă—).
515:article, which was merged here) from August 2001
614:. A quick google search suggests that Manin's
259:does not concern the main topic of the article
8:
19:
47:
438:
433:
427:
386:
381:
375:
342:
337:
331:
208:
203:
197:
645:and some independent sources do as well
49:
454:-formula defining an axiom system for
7:
458:in the standard model of arithmetic.
95:This article is within the scope of
402:, which do not have exponentiation.
38:It is of interest to the following
430:
334:
200:
14:
733:Mid-priority mathematics articles
115:Knowledge:WikiProject Mathematics
728:Start-Class mathematics articles
118:Template:WikiProject Mathematics
82:
72:
51:
20:
447:{\displaystyle \Sigma _{1}^{0}}
351:{\displaystyle \Sigma _{1}^{0}}
263:Gödel's incompleteness theorems
217:{\displaystyle \Sigma _{1}^{0}}
135:This article has been rated as
1:
714:17:50, 17 February 2018 (UTC)
574:11:16, 12 December 2014 (UTC)
109:and see a list of open tasks.
674:12:58, 8 November 2012 (UTC)
660:12:42, 8 November 2012 (UTC)
637:12:31, 8 November 2012 (UTC)
601:23:01, 9 December 2011 (UTC)
690:06:27, 3 October 2017 (UTC)
627:, which has preview in GB.
749:
322:We are discussing Gödel's
696:Universal Diophantine set
395:{\displaystyle S_{2}^{1}}
134:
67:
46:
560:14:34, 9 June 2009 (UTC)
547:11:44, 9 June 2009 (UTC)
526:10:34, 9 June 2009 (UTC)
498:03:05, 9 June 2009 (UTC)
471:10:34, 9 June 2009 (UTC)
315:02:55, 9 June 2009 (UTC)
285:10:09, 8 June 2009 (UTC)
273:10:04, 8 June 2009 (UTC)
252:17:09, 7 June 2009 (UTC)
237:10:36, 3 June 2009 (UTC)
186:05:41, 3 June 2009 (UTC)
141:project's priority scale
702:Matiyasevich, Chapter 4
641:Martin Davis uses MRDP
608:Hilbert's tenth problem
98:WikiProject Mathematics
513:Matiyasevich's theorem
448:
396:
352:
218:
28:This article is rated
449:
397:
353:
303:Diophantine equations
219:
612:Computability Theory
426:
374:
330:
196:
162:The main text says:
121:mathematics articles
535:Robinson arithmetic
443:
391:
347:
213:
444:
429:
392:
377:
348:
333:
214:
199:
90:Mathematics portal
34:content assessment
622:978-1-4419-0614-4
539:Danko Georgiev MD
490:Danko Georgiev MD
307:Danko Georgiev MD
244:Danko Georgiev MD
178:Danko Georgiev MD
155:
154:
151:
150:
147:
146:
740:
610:—Barry Cooper's
453:
451:
450:
445:
442:
437:
421:
401:
399:
398:
393:
390:
385:
357:
355:
354:
349:
346:
341:
305:at first place.
223:
221:
220:
215:
212:
207:
123:
122:
119:
116:
113:
92:
87:
86:
76:
69:
68:
63:
55:
48:
31:
25:
24:
16:
748:
747:
743:
742:
741:
739:
738:
737:
718:
717:
706:Boris Tsirelson
698:
682:173.228.123.121
588:
424:
423:
422:where Ď„ is any
419:
415:
372:
371:
328:
327:
194:
193:
160:
120:
117:
114:
111:
110:
88:
81:
61:
32:on Knowledge's
29:
12:
11:
5:
746:
744:
736:
735:
730:
720:
719:
697:
694:
693:
692:
677:
676:
663:
662:
639:
587:
584:
583:
582:
581:
580:
579:
578:
577:
576:
530:
529:
528:
503:
502:
501:
500:
482:
481:
480:
479:
478:
477:
476:
475:
474:
473:
461:
460:
459:
441:
436:
432:
417:
403:
389:
384:
380:
367:
363:
345:
340:
336:
299:exponentiation
295:exponentiation
291:exponentiation
275:
211:
206:
202:
159:
156:
153:
152:
149:
148:
145:
144:
133:
127:
126:
124:
107:the discussion
94:
93:
77:
65:
64:
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
745:
734:
731:
729:
726:
725:
723:
716:
715:
711:
707:
703:
695:
691:
687:
683:
679:
678:
675:
672:
669:
665:
664:
661:
657:
653:
649:
647:
644:
640:
638:
634:
630:
626:
623:
620:
617:
613:
609:
605:
604:
603:
602:
598:
594:
593:Stephanwehner
585:
575:
571:
567:
563:
562:
561:
558:
555:
550:
549:
548:
544:
540:
536:
531:
527:
524:
521:
517:
514:
509:
508:
507:
506:
505:
504:
499:
495:
491:
486:
485:
484:
483:
472:
469:
466:
462:
457:
439:
434:
413:
409:
404:
387:
382:
378:
368:
364:
361:
343:
338:
325:
321:
320:
318:
317:
316:
312:
308:
304:
300:
296:
292:
288:
287:
286:
283:
280:
276:
274:
271:
268:
264:
260:
255:
254:
253:
249:
245:
240:
239:
238:
235:
232:
227:
209:
204:
190:
189:
188:
187:
183:
179:
175:
171:
166:
163:
158:Error in text
157:
142:
138:
132:
129:
128:
125:
108:
104:
100:
99:
91:
85:
80:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
27:
23:
18:
17:
699:
615:
611:
589:
455:
411:
407:
359:
323:
258:
225:
173:
169:
167:
164:
161:
137:Mid-priority
136:
96:
62:Mid‑priority
40:WikiProjects
586:Reference ?
414:interprets
265:article. —
112:Mathematics
103:mathematics
59:Mathematics
30:Start-class
722:Categories
410:such that
170:consistent
652:Tijfo098
629:Tijfo098
226:formulas
416:Q + Con
139:on the
566:Nxavar
360:second
36:scale.
324:first
710:talk
686:talk
668:Emil
656:talk
643:here
633:talk
619:ISBN
597:talk
570:talk
554:Emil
543:talk
520:Emil
494:talk
465:Emil
311:talk
279:Emil
267:Emil
248:talk
231:Emil
182:talk
131:Mid
724::
712:)
704:.
688:)
671:J.
658:)
650:.
635:)
599:)
572:)
557:J.
545:)
523:J.
496:)
468:J.
431:ÎŁ
335:ÎŁ
313:)
282:J.
270:J.
250:)
234:J.
201:ÎŁ
184:)
176:.
708:(
684:(
654:(
631:(
595:(
568:(
541:(
492:(
456:T
440:0
435:1
420:,
418:Ď„
412:T
408:T
388:1
383:2
379:S
344:0
339:1
309:(
246:(
210:0
205:1
180:(
143:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
