Bruno: yes that is unfortunately true. Ronald On Dec 30, 10:25 am, Bruno Marchal <marc...@ulb.ac.be> wrote: > On 30 Dec 2009, at 03:29, ronaldheld wrote: > > > Bruno: > > Is there a UD that is implemented in Fortran? > > I don't know. If you know Fortran, it should be a relatively easy task > to implement one. > Note that you have still the choice between a fortran program > dovetailing on all computations by combinators, or on all computations > by LISP programs, or on all proofs of Sigma_1 complete arithmetical > sentences, or on all running of game of life patterns, etc. > Of you can write a Fortran program executing all Fortran programs. All > this will be equivalent. All UD executes all UDs, and this an infinity > of times. > > Good exercise. A bit tedious though. > > Bruno > > > > > > > > > On Dec 29, 4:55 am, Bruno Marchal <marc...@ulb.ac.be> wrote: > >> On 28 Dec 2009, at 21:24, Nick Prince wrote: > > >>>> Well, it is better to assume just the axiom of, say, Robinson > >>>> arithmetic. You assume 0, the successors, s(0), s(s(0)), etc. > >>>> You assume some laws, like s(x) = s(y) -> x = y, 0 ≠ s(x), the > >>>> laws > >>>> of addition, and multiplication. Then the existence of the > >>>> universal > >>>> machine and the UD follows as consequences. > > >>> Ok so the UD exists (platonically?) > > >> Yes. The UD exists, and its existence can be proved in or by very > >> weak > >> (not yet Löbian) arithmetical theories, like Robinson Arithmetic. > >> The UD exists like the number 733 exists. The proof of its existence > >> is even constructive, so it exists even for an intuitionist (non > >> platonist). No need of the excluded middle principle. > > >>>> Better not to conceive them as living in some place. "where" and > >>>> "when" are not arithmetical predicate. The UD exists like PI or the > >>>> square root of 2. > >>>> (Assuming CT of course, to pretend the "U" in the UD is really > >>>> universal, with respect to computability). > > >>> Fine so the UD has an objective existence in spite of whatever else > >>> exists. > > >> It exists in the sense that we can prove it to exist once we accept > >> the statement that 0 is different from all successor (0 ≠ s(x) for > >> all x), etc. > >> If you accept high school elementary arithmetic, then the UD exists > >> in > >> the same sense that prime numbers exists. > >> "exist" is used in sense of first order logic. This leads to the > >> usual > >> philosophical problems in math, no new one, and the UDA reasoning > >> does > >> not depend on the alternative way to solve those philsophical > >> problem, > >> unless you propose a ultra-finitist solution (which I exclude in comp > >> by arithmetical realism). > > >>>> There is a "time order". The most basic one, after the successor > >>>> law, > > >>>> is the computational steps of a Universal Dovetailer. > >>>> Then you have a (different) time order for each individual > >>>> computations generated by the UD, like > > >>>> phi_24 (7)^1, phi_24 (7)^2, phi_24 (7)^3, phi_24 (7)^4, ... > >>>> where "phi_i (j)^s" denotes the sth steps of the computation (by > >>>> the UD) of the ith programs on input j. > > >>> If the UD was a concrete one like you ran then it would start to > >>> generate all programs and execute them all by one step etc. But are > >>> you saying that because the UD exists platonically all these > >>> programs > >>> and each of their steps exist also and hence, by the existence of a > >>> successor law they have an implicit time order? > > >> Yes. The UD exist, and is even representable by a number. UD*, the > >> complete running of the UD does not exist in that sense, because it > >> is > >> an infinite object, and such object does not exist in simple > >> arithmetical theories. But all finite parts of the UD* exist, and > >> this > >> will be enough for "first person" being able to glue the > >> computations. > >> For example, you could, for theoretical purpose, represent all the > >> running of the UD by a specific total computable function. For > >> example > >> by the function F which on n gives the (number representing the) nth > >> first steps of the UD*. Then you can use the theorem which asserts > >> that all total computable functions are representable in Robinson > >> Arithmetic (a tiny fragment of Pean Arithmetic). That theorems is > >> proved in detail, for Robinson-ile arithmetic, in Boolos and Jeffrey, > >> or in Epstein and Carnielli. In Mendelson book it is done directly in > >> Peano Arithmetic. > > >>>> Then there will be the time generated by first person learning and > >>>> which relies eventually on a statistical view on infinities of > >>>> computations. > > >>> Is this because we are essentially constructs within these steps? > > >> It is because our "3-we", our bodies, or our bodies descriptions, are > >> constructed within these steps. But our first person are not, and no > >> finite pieces of the UD can give the "real experience". This is a > >> consequence of the first six steps: our next personal experience is > >> determined by the whole actual infinity of all the infinitely many > >> computations arrive at our current state. (+ step 8, where we abandon > >> explicitly the physical supervenience thesis for the computational > >> one). > > >>>> Time is not difficult. It is right in the successor axioms of > >>>> arithmetic. > > >>> Here again you confirm the invocation of the successor axioms. > > >> Yes. It is fundamental. I cannot extract those from logic alone. No > >> more than I can define addition or multiplication without using the > >> successor terms s(-) : > > >> for all x x + 0 = x > >> for all x and y x + s(y) = s(x + y) > > >> You have to understand that all the talk on the phi_i and w_i, > >> including the existence of universal number > >> (EuAxAy phi_u(<x,y>) = phi_x(y)) can be translated in pure first > >> order > >> arithmetic, using only s, + and *. > > >> I could add some nuances. "To be prime" is an intrinsic property of a > >> number. To be a universal number is not intrinsic. To define a > >> universal number I have to "arithmetize" the theory. The theory uses > >> variables x, y, z, ..., so I will have to represent "to be a > >> variable" > >> in the theory. The theory "understands" only numbers. I can decide to > >> represent the variables by even numbers (for example). "Even(x)" can > >> be represented by "Ey(x = s(s(0)) * y)". So "variable(x)" will be > >> represented by the same expression. Then I will represent "to be a > >> formula", "to be an axiom", to be a proof", "to be a computation", > >> using Gödel's arithmetization technic (which is just a form of > >> programming in arithmetic). This will lead to a representation of > >> being a universal number. > >> Now, would I decide to represent the variable in some other way (by > >> the odd numbers, for example), the preceding universal number will > >> still be in a universal number (intrinsically), but I will not been > >> able to see it, or to mention it explicitly. But here, you have to > >> just realize (cf the first six step of uda) that the first person > >> experience depends on all universal numbers, in all possible sense/ > >> arithmetical-implementations. > >> In particular "you here and now" are indeed implemented in arithmetic > >> in bot the universal numbers based on (variable(x) = even(x), and > >> variable(x) = odd(x)). *ALL* universal numbers will compete below > >> your > >> substitution level. > > >> The fact that elementary (Robinson) arithmetic is already (Turing) > >> universal is an impressive not obvious fact. But it is no more > >> astonishing than the fact that Conway Game of Life is already Turing > >> universal, or that the combinators S and K are Turing universal, etc. > > >> Bruno > > >>http://iridia.ulb.ac.be/~marchal/ > > > -- > > > You received this message because you are subscribed to the Google > > Groups "Everything List" group. > > To post to this group, send email to everything-l...@googlegroups.com. > > To unsubscribe from this group, send email to > > everything-list+unsubscr...@googlegroups.com > > . > > For more options, visit this group > > athttp://groups.google.com/group/everything-list?hl=en > > . > > http://iridia.ulb.ac.be/~marchal/- Hide quoted text - > > - Show quoted text -
-- You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to everything-l...@googlegroups.com. To unsubscribe from this group, send email to everything-list+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/everything-list?hl=en.