> On 9 Sep 2018, at 17:03, John Clark <[email protected]> wrote: > > On Sun, Sep 9, 2018 at 6:44 AM Bruno Marchal <[email protected] > <mailto:[email protected]>> wrote: > > >>Nobody on this planet uses the term "Löbian machine" except you. > > >It is just a more precise version of what popular books described by > >“sufficiently rich theory”. > > There is nothing precise about homemade slang used by nobody but you.
Let us talk on ideas, not on people. Take any Turing universal theory/machine, like Robinson arithmetic: Classical logic + 0 ≠ s(x) s(x) = s(y) -> x = y x = 0 v Ey(x = s(y)) x+0 = x x+s(y) = s(x+y) x*0=0 x*s(y)=(x*y)+x Or Combinator theory: i.e. axiom of identity + Kxy = x Sxyz = xz(yz) Both those theories/machines are Turing-complete/universal. They determine an entire Universal dovetailing. But none of them is Löbian. They are NOT “sufficiently rich”. But both becomes Löbian (verify and prove Löb’s formula []([]p->p)->[]p, and this obeys to the machine theology G*) once you add the induction axioms, i.e. the infinitely many axioms of induction: that is, with A an arbitrary formula (in the respective domain), the axioms: If A(0) and if (n)(A(n) -> A(s(n))) then (n)A(n) Or If A(K) and A(S), and if (x)(A(x) & A(y) ->. A(xy)), then (x)A(x). > > > There are many definition, but they are all equivalent. > > And there is nothing profound about a definition, it's easy to define a > perpetual motion machine but that doesn't mean they exist, I can define a > Clark Machine as a machine that can solve the halting problem but that > doesn't mean I have the any idea how to make one or can even show that such a > thing could in principle exist. Sure. > > >Any Turing complete theory of any universal machine, with sufficiently > >strong induction axiom (like sigma_1 induction) constitute a Löbian machine. > > In the physical world induction is just a rule of thumb that usually works > pretty well most of the time, but it seldom works perfectly and never works > continuously, eventually it always fails. ? You seem to confuse mathematical induction, and adductive inference. > > >>Turing explained exactly precisely how to build one of his machines but you > >>have never given the slightest hint of how to build a "Löbian machine" or > >>even clearly explained what it can compute that a Turing Machine can’t. > > >? > ! I have given a lot of example. Peano arithmetic is a Löbian machine. Zermelo-Fraenkel Set Theory is a Löbian Machine, all humans, as as as they are arithmetically correct, are Löbian machine. I gave other examples in my long text, and two examples are given above. You can define a Löbian machine by any theory or machine on which Löb’s theorem is applicable (and then it can be shown that they will be aware of this). Here is another definition: A machine is Turing universal iff for all sigma_1 proposition p -> []p is true. A machine is Löbian iff for all sigma_1 proposition p -> []p is provable by the machine. > > >That means just that you need to go being step 3 in my thesis, > > Step 3? Ah yes I remember now, that's the one with wall to wall personal > pronouns without a single clear referent in the entire bunch. No, you have agreed on each definition. You agreed that both the W-man and the H-man are honorable H-man survivor, and you did manage to take into account the first person/third person in some context (like in Everett).. It is you critic of step 3 which nobody understand. You are the only one person in the world that I know having taken so much time to get that extremely easy, if not obvious point. You did grasp it at repetition, and just adding something like it was obvious, but then never answer the step 4. > > > The notion of Löbian machine is easy to construct, > > The notion of a Perpetual Motion machine is also easy to construct as is the > Clark Machine that can solve the Halting Problem, but Turing did far more > than dream up a magical universal calculating machine, he showed exactly how > to make one. Yes, it did that too, but that does not change the fact that his recovery was in pure mathematics at first. Then later it has been shown to be in already pure arithmetic. > But we're not as smart as Turing, I can't do that with my Clark Machine and > you can't do that with your Löbian machine. Nobody ever pretended anything like that. Universal machine suffer intrinsic limitation (which Brough all the incompleteness nuance on G* which build the machine theology), and the only difference with the Löbian machine is that they know this: they prove their incompleteness theorem, like Gödel foresaw already at the end of his 1931 paper (but that will be proved by Hilbert and Bernays in 1937 for the first time, and extended in 1955 by Löb in an important way). > > > and the mathematical reality is full of example of Löbian machine, and > > Löbian god > > Löbian machine, Löbian god, the propositional part of the theology .... tell > me, have you ever wondered why so many people fail to take you seriously? Only pseudo-religious people have problem with those results. Academically, there are never been any problem, by any experts in the field. But I do get reports by people who told me they were asked to not cite my work, and when they ask why, they see that I am criticised on things which I have never claimed or write. > > >A Lpobian machine is just a universal machine capable of proving its own > >universality. > > I have no trouble believing a universal machine is universal, but no Turing > Machine can in general prove it will halt and but no machine of any sort, or > anything else for that matter, can prove its own consistency unless it is > inconsistent. Did I ever claim anything different. On the contrary, that is an important point: computability is absolute, provability is relative. Universal machine have important logical limitation, and Löbian machine have the same limitation, but are aware of those limitation, making them intrinsically modest (as Parikh and Smullyan called the Löbian machines). > > > Why do you want it to be able to do what a god can do? > > Odd question, who wouldn't want to do what a God can do? But if God can solve > the Halting Problem then He can also make a rock so heavy He can't lift it. > > >>How would things be different if "the propositional part of the theology" > >>were not decidable? > > >Solovay theorem would be false, and the subject of machine theology would be > >far more complex. > > I don't know if that's true or not because "machine theology" is more of your > homemade gibberish, just like "the propositional part of the theology”. No, it is the modal logic G*. I take the greco-endian definition of “theology”, then G* (and its intensional variants) becomes the theology of the (correct, sound) Löbian machine. I recall to you that by machine theology I just meant the modal logic G*. It is the logic of the true proposition that a machine can or cannot prove about itself. > > > Note that the theology of machine has highly undecidable at the first order > > level. > > And I don't know if that is true or not either because "the theology of > machine" is yet more of your patented homemade baby talk. It looks like it is enough I use a term for it to be BS. But that is only peremptory talk. I will wait for arguments. Mocking and derail-diing a reasoning cannot make it invalid. Bruno > > John K Clark > > > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected] > <mailto:[email protected]>. > To post to this group, send email to [email protected] > <mailto:[email protected]>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
