Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail From: Ben Bacarisse Newsgroups: comp.theory Subject: Re: Simply defining =?iso-8859-1?Q?G=F6del?= Incompleteness and Tarski Undefinability away V24 (Are we there yet?) Date: Wed, 22 Jul 2020 02:03:47 +0100 Organization: A noiseless patient Spider Lines: 66 Message-ID: <87r1t4mkcs.fsf@bsb.me.uk> References: <87sgdrz49w.fsf@nosuchdomain.example.com> <874kq7yug9.fsf@nosuchdomain.example.com> <4dKdnXavpI9eu4zCnZ2dnUU7-S3NnZ2d@giganews.com> <87ft9qy3cn.fsf@nosuchdomain.example.com> <87imelefjh.fsf@bsb.me.uk> <87d04ser16.fsf@bsb.me.uk> <875zakwk73.fsf@nosuchdomain.example.com> <87v9ikcjdv.fsf@bsb.me.uk> <87k0yzcmhl.fsf@bsb.me.uk> <8fKdndiKLplIMYnCnZ2dnUU7-RvNnZ2d@giganews.com> <87ft9not86.fsf@bsb.me.uk> <87tuy1ofk4.fsf@bsb.me.uk> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Injection-Info: reader02.eternal-september.org; posting-host="c547eb430aacce872c2d79add73c34bc"; logging-data="12168"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/TlZkNQ35bSXNQiDwQpeDvZ+kha+8AUcE=" Cancel-Lock: sha1:OOw3GRQkJC7HZJvbjodzbjNvs3M= sha1:wkM8Yrd5AyYLVniX2Ku3u9KVJs8= X-BSB-Auth: 1.0326e5e258f0c9ddcbdb.20200722020347BST.87r1t4mkcs.fsf@bsb.me.uk Xref: csiph.com comp.theory:21850 olcott writes: > On 7/20/2020 7:52 PM, Ben Bacarisse wrote: >>> On 7/19/2020 8:44 PM, Ben Bacarisse wrote: >> Anyway, it, and a whole host of interrelated theorems, remain theorems, >> with dozens of interlocking and overlapping proofs, none of which have >> been shown to have any serious flaws. (I say that because an >> embarrassingly large number of published proofs do have minor, fixable, >> flaws.) > > If that all start with a single false premise then that all fail. If... >> Why won't you answer my question? > > I just showed you what decidable means. I think you are having trouble reading. That was not my question. I asked if there are any uncomputable functions in PO-land -- the land in which halting (and all the others I listed a few posts ago) are computable? >>> H.q0 wM w ⊢* H.qy >>> H.q0 wM w ⊢* H.qn >> >> Argh!! Again you fail to use the key part of this notation. > > Which part did I leave out? The bit I said you missed out right after I said you had: >> I have >> explained, time and time again, that without the criteria for each case >> these lines are useless. Can you see it now? >>> When we make this whole thing perfectly concrete fully encoding every >>> single detail then and only then is it impossible for things to slip >>> through the cracks of human understanding. >> >> You lied about having done that 18 months ago. To cover that lie you've >> been making excuses for why you have to write a whole steaming pile of >> X86 code just so you can bury whatever error it is you have made. > > I have never lied about this. The key algorithm was fully encoded in > pseudo-code "I now have the actual Turing machine that has been "proven" to not possibly exist. It can be actually executed within an actual UTM." Message-ID: "I have the Turing Machines H and Ĥ right now. What I do not have is the C++ UTM that executes H on input pair(Ĥ, Ĥ)." Message-ID: "I now have an actual H that decides actual halting for an actual (Ĥ, Ĥ) input pair. I have to write the UTM to execute this code, that should not take very long. The key thing is the H and Ĥ are 100% fully encoded as actual Turing machines." Message-ID: -- Ben.