tag:blogger.com,1999:blog-20067416.post4473364255380507029..comments2018-02-17T05:00:32.018-05:00Comments on Recursivity: Using a Decision Method to Prove a New Theorem in Number TheoryJeffrey Shallitnoreply@blogger.comBlogger9125tag:blogger.com,1999:blog-20067416.post-86076709367098334302017-07-14T14:39:57.419-04:002017-07-14T14:39:57.419-04:00I see, thanks!I see, thanks!sniffnoyhttp://sniffnoy.livejournal.com/noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-23704789955619824772017-07-13T09:34:09.418-04:002017-07-13T09:34:09.418-04:00Got it.
Well, sort of. I'm off to read someth...Got it.<br /><br />Well, sort of. I'm off to read something about the existential theory of the reals.lukebarneshttps://www.blogger.com/profile/03245704613008522157noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-20579696928938176832017-07-11T04:17:38.688-04:002017-07-11T04:17:38.688-04:00Luke:
The existential theory of the reals is not ...Luke:<br /><br />The existential theory of the reals is not stronger than, for example, Presburger arithmetic. They're not comparable. For one thing, in the existential theory of the reals it is not possible to express the assertion "x is an integer".Jeffrey Shallithttps://www.blogger.com/profile/12763971505497961430noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-68282982049414809582017-07-10T07:16:50.070-04:002017-07-10T07:16:50.070-04:00Extremely cool, though it leaves me a bit dizzy.Extremely cool, though it leaves me a bit dizzy.Joe Felsensteinhttps://www.blogger.com/profile/06359126552631140000noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-16537801414767428122017-07-07T09:18:29.401-04:002017-07-07T09:18:29.401-04:00Nifty. A lot of presentations of undecidability ma...Nifty. A lot of presentations of undecidability make it sound like nobody should ever care about it mathematically speaking because decidable theories are way too weak. But this is an intermediary case I wasn't aware of and gives the lie to that attitude.<br /><br />Now I wonder increasingly how this maps on to traditional programming and software concerns. I'm in application security now, and while it is true that AS is undecidable in general, I wonder about security properties of certain classes of programs increasingly. philosopher-animalhttps://www.blogger.com/profile/16505629919126188962noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-28883516738994936542017-07-07T06:40:20.071-04:002017-07-07T06:40:20.071-04:00That's fascinating.
I have a related question...That's fascinating.<br /><br />I have a related question. You say "GĂ¶del showed that, given any sufficiently powerful axiom system (roughly speaking, it's enough to be able to define addition and multiplication of integers), there would be true results lacking any formal proof."<br /><br />And yet I am told that the real numbers are complete and decidable. More precisely, wikipedia tells me, the natural first-order theory of arithmetic of real numbers (with both addition and multiplication) is complete and decidable, as was shown by Tarski (1948). This would seem to me (as a spectator, not a mathematician) as an example of a more powerful axiomatic system being complete and decidable. <br /><br />Again, I remember reading somewhere that, while one can add axioms to an incomplete axiomatic system to make statements decidable, this will result in other statements becoming undecidable. But that doesn't seem to be the case here. Or should I not be thinking of the reals as an "expansion" (in some sense) of the integers? I find the whole thing fascinating and confusing in equal measure.lukebarneshttps://www.blogger.com/profile/03245704613008522157noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-57832196004658078132017-07-06T19:26:04.606-04:002017-07-06T19:26:04.606-04:00This is just too much fun! Thanks for posting it.
...This is just too much fun! Thanks for posting it.<br /><br />~~ Paul<br />Paul C. Anagnostopouloshttps://www.blogger.com/profile/07146336984557843642noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-4135056556990302292017-07-06T14:07:59.079-04:002017-07-06T14:07:59.079-04:00V_k (n) is the highest power of k dividing n. Not...V_k (n) is the highest power of k dividing n. Not the exponent of the power, but the power itself.Jeffrey Shallithttps://www.blogger.com/profile/12763971505497961430noreply@blogger.comtag:blogger.com,1999:blog-20067416.post-83125639328504407782017-07-06T11:59:01.004-04:002017-07-06T11:59:01.004-04:00Sorry, just what is V_k? I couldn't find it i...Sorry, just what is V_k? I couldn't find it in the linked Walnut paper.sniffnoyhttp://sniffnoy.livejournal.com/noreply@blogger.com