tag:blogger.com,1999:blog-4987609114415205593.post3440712405413556964..comments2021-06-14T17:02:48.428+01:00Comments on M-Phi: Here we go again: "PA is inconsistent" (Edward Nelson)Jeffrey Ketlandhttp://www.blogger.com/profile/01753975411670884721noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-4987609114415205593.post-19445125130282707962012-12-09T19:12:47.346+00:002012-12-09T19:12:47.346+00:00E.Nelson.Warning Signs of a Possible Collapse of C...E.Nelson.Warning Signs of a Possible Collapse of Contemporary Mathematics. https://web.math.princeton.edu/~nelson/papers/warn.pdf<br />Actually E. Nelson asserts that:(1) the standard model of the ZFC and (2) even standard model of the PA obviously does not exist. Nevertheless there is no necessity to prove inconsistency PA.<br />For overthrow of classical mathematics that achieves E.Nelson, it is enough to prove inconsistency ZFC.<br />J.F.https://www.blogger.com/profile/14378069762140227312noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-43140645540544749452012-12-08T14:46:55.285+00:002012-12-08T14:46:55.285+00:00Even if the error is not repairable, this is no im...Even if the error is not repairable, this is no importent, because ZFC is inconsistent.<br /><br />http://ru.scribd.com/doc/115667544?secret_password=2gzzmxsoylip718oxbvd<br /><br />http://math.stackexchange.com/questions/251803/inconsistent-countable-set-in-zfcAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-82652188456645270502011-09-30T02:53:15.659+01:002011-09-30T02:53:15.659+01:00It's instructive to contrast this episode with...It's instructive to contrast this episode with the "proof" of P=NP earlier this year, when the math blogs were filled with daily chatter on the subject for months. In that case, the "proof" was amorphous and most effort went in to determining if anything substantial and new had been proven.<br /><br />In this case, a coherent system was presented in a verifiable form, and a serious flaw was detected within hours. The reserved silence of the community has been almost eerie as an acknowledgement of the error is awaited, possibly with a modification or indication of the next step.<br /><br />Even if the error is not repairable, this episode marks a victory for mathematical discourse.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-60029220121898528182011-09-29T04:49:57.384+01:002011-09-29T04:49:57.384+01:00D Tausk has clarified the sense in which Tao takes...D Tausk has clarified the sense in which Tao takes the Kolmogorov complexity of a number to depend on a theory.<br />It appears that at a minimum Professor Nelson will need to modify his proof.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-58809253218780075372011-09-28T10:04:09.557+01:002011-09-28T10:04:09.557+01:00I do not think that RoyTCook's point is correc...I do not think that RoyTCook's point is correct. If, while working within a formal language system, one can prove its inconsistency by obtaining a statement within the system that is both true and false, then one has indeed invalidated the proof, but the proof is needed no longer. That is, the only way in which the proof is invalidated is if the theory of syntax in which it is carried out is inconsistent in the first place.Jayantnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-78719848189986232962011-09-28T07:44:18.600+01:002011-09-28T07:44:18.600+01:00Theorem: Nelson's proof can't be right.
P...Theorem: Nelson's proof can't be right.<br /><br />Proof: The formal system within which Nelson carries out his proofs requires a theory of syntax. This theory is surely at least as strong as PRA. So:<br /><br />(1) If Nelson's proof is right, then it follows that Nelson's proof is wrong.<br /><br />Since, if the proof that PRA is inconsistent were correct, then it would presuppose, in the account of syntax for the language in which it is carried out, an inconsistent theory. <br /><br />Even an intuitionist will admit that the above is equivalent to:<br /><br />(2) Nelson's proof is wrong.<br /><br />QED.<br /><br />[There is a serious point being made here about the role of arithmetic in formulating syntax - one which Jeff has made elsewhere. In essence, you can't prove ANYTHING in a formal system without assuming some basic arithmetic. So if you show that the basic arithmetic in question is faulty, then you can't prove ANYTHING. So even if Nelson is in some sense 'right', there is some reason for thinking that, even by his own lights, he hasn't actually proven anything.]RoyTCookhttps://www.blogger.com/profile/05233569728242084863noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-28829437452750485912011-09-27T22:21:19.536+01:002011-09-27T22:21:19.536+01:00I checked the first paragraphs of the book quickly...I checked the first paragraphs of the book quickly and as a result I wanted to ask you about a very interesting point I noticed in Nelson's attempt to proof that PA is inconsistent.<br /><br />(In page 11 and above) It seems like he is trying to push the argument against finitsm. In order to do that, he argues against mathematical induction. The argument (more or less) depends on the fact that natural numbers' properties are due to the very concept of standard model which, in turn needs ZF theory to prove some results about numbers and numerals. Therefore, finitsm has an infinitist foundation, which means the entire idea of finitism crashed.<br /><br />Did I get it (a little bit) right? What did you understand?<br /><br />And more important: Could anyone see this as a negative result about standard models?<br /><br />Of course ruling out standard models is a big issue and could have colossal results for example in work with paradoxes involving infinite constructions.Damianhttp://www.accionfilosofica.comnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-18196005288794526142011-09-27T19:21:03.348+01:002011-09-27T19:21:03.348+01:00@jrshipley, thanks for the pointer! I've added...@jrshipley, thanks for the pointer! I've added an update linking both to the n-Category Cafe' post and to the G+ thread (gotta love G+!)Catarinahttps://www.blogger.com/profile/03277956118114314573noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-31654456887739603032011-09-27T14:32:35.923+01:002011-09-27T14:32:35.923+01:00The logical system employed is not intuitionistic....The logical system employed is not intuitionistic. This becomes apparent at least from Theorem 7 onward.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-53292262056069477432011-09-27T13:25:00.390+01:002011-09-27T13:25:00.390+01:00Commenting on John Baez share of this at g+, Teren...Commenting on John Baez share of this at g+, Terence Tao wrote: <br /><br />"I think I can reconstruct enough of the argument to figure out where the error in reasoning is going to be. Basically, in order for Chaitin's theorem (10) to hold, the Kolmogorov complexity of the consistent theory T has to be less than l. But when one arithmetises (10) at a given rank and level on page 5, the complexity of the associated theory will depend on the complexity of that rank and level; because there are going to be more than 2^l ranks and levels involved in the iterative argument, at some point the complexity must exceed l, at which point Chaitin's theorem cannot be arithmetised for this value of l."jrshipleyhttps://www.blogger.com/profile/05991272871497674850noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-78913259799438681622011-09-27T11:15:02.972+01:002011-09-27T11:15:02.972+01:00Ok, so inside the book he does refer to automated ...Ok, so inside the book he does refer to automated theorem-proving, not only theorem-checking. I am also fascinated by this idea, that's why I singled it out as something particularly thought-provoking in the claims being made by Nelson.Catarinahttps://www.blogger.com/profile/03277956118114314573noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-87596845324793640562011-09-27T11:05:23.947+01:002011-09-27T11:05:23.947+01:00Perhaps I misunderstood the difference between a t...Perhaps I misunderstood the difference between a theorem prover and a theorem checker. <br /><br /><br />But by skimming through the book is working on, I found page 40 more explanations on qea:<br />"The simple proof was automatically generated from the text proof by a program called<br />qea. Proofs generated by qea are simple proofs consisting of five parts...."<br /><br />When I read this passage, I understand that the tool does not only check but gives proofs, at least for the simple ones. Perhaps a lot of them were trivial but anyway, the tool gives the proof and checks it at the same time. Then from page 41 to the end, a long list of definitions and theorems are given (the last is numbered 733). Surely, most of these theorems are automatically generated by qea.<br /><br />I find this way of working really interesting. <br /><br />MathieuAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-12304276671631541762011-09-27T09:51:59.522+01:002011-09-27T09:51:59.522+01:00As I understood him, Nelson is not using an automa...As I understood him, Nelson is not using an automated theorem-prover, but rather a theorem-*checker*.<br />He does say that all proofs are indirect proofs, so presumably there is something very classical in the background.Catarinahttps://www.blogger.com/profile/03277956118114314573noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-83624501542350230002011-09-27T09:29:35.810+01:002011-09-27T09:29:35.810+01:00The use of an automatic theorem-prover is really i...The use of an automatic theorem-prover is really interesting. It saves time and produces an output that can be integrated directly in a book or a paper. The use of this type of tools is really the future and will certainly change the practice of the logician and of the mathematician. We can compare it to the apparation of the calculator. Today, almost nobody will check by hand that [(145 + 256) * 7] + 942 = 3812 and use instead a software to compute it. Why bother to produce and check simple proofs if a tool can do it? Anyway, without clear specification about its software, we can ask ourself what kind of logic is implemented. It seems that only classical logical steps are used in this case.<br /><br />Concerning his claim about the inconsistency of PA, it's really too high level for me.<br /><br />MathieuAnonymousnoreply@blogger.com