On Sun, Feb 12, 2012 at 1:07 PM, Bruno Marchal <marc...@ulb.ac.be> wrote:
> > > On 11 Feb 2012, at 23:09, Joseph Knight wrote: > > > > On Sat, Feb 11, 2012 at 11:41 AM, Stephen P. King > <stephe...@charter.net>wrote: > >> >> >> >> The diagram is strictly 3p. It would be helpful if you wrote up an >> informal article on the octolism. It is very difficult to comprehend it >> from just your discussion of the hypostases. >> > > I agree, this would be very helpful. I wouldn't mind if it got a little > technical, either. > > > Have you read the part 2 of sane04? (which starts at the page 12). It is a > concise version of AUDA. > I read it, and will review it further, but I feel like I don't have a good understanding of what's going on toward the very end of the paper (last 3-4 pages particularly). But take that with a grain of salt, since I haven't read most of the other papers on your website, which also discuss the matter. > > When I reread it now, I am frightened by my own style, and spelling. I > also see little mistakes here and there. But it explains the main thing. > > To interview a universal machine about itself (at some level) makes > necessary to describe the universal machine in its language (there is no > miracle). That part is usually long and tedious, but for someone capable > of programming in some universal language (be it fortran or lisp, or > whatever) the principle are not different from programming an interpreter > or a compiler. It is the writing of the code of an interpreter in the > language of that intepreter. I often skip that part, but refer to the basic > literature (Gödel 1931, ...). > > The more the universal system is simple, the more the translation is long > and tedious. In case the universal system is extremely simple (like a > universal degree 4 diophantine polynomial) the proof of universality is > very complex (it is the Putnam-Davis-Robinson-Matiyasevitch-Jones story). > > If you can write an interpreter lisp in the language lisp, an easy task, > you can better conceive that it is possible (and has been done) to write an > "interpreter of arithmetic" in arithmetic. > > That is mainly the one I call "B" for Gödel's beweisbar predicate, which > define Peano Arithmetic (say) in (Peano, Robinson) Arithmetic. > Beweisbar(x) is the arithmetical predicate for "x is provable", with x > coding arithmetically a proposition. Arithmetical means that it is defined > only with "E", f, ->, s, 0, and parenthesis). > > What is your familiarity with Gödel 1931? Gödel's original paper use > Principia Mathematica (a formal version of a Russell typed set theory). Do > you see the relation between Gödel numbering/beweisbar and > programming/universal-interpreter. Both RA and PA are sigma_1 complete, so > you can use them as programming language, and "B" refer to Turing universal > arithmetical predicate. But as a provability predicate, its range is > personal and different for RA, PA, ZF, you, me, etc. > > Hmm... I might have to insist that computability is an absolute notion > (with CT), but provability is always relative to a machine/number. > Provability becomes universal (with respect to the computable) when it is > Sigma_1 complete (like RA and PA). Sigma_1 complete provability is Turing > universal, and this ease the talk on computer science, and beyond, with the > machine. > > The (meta) theories (G, G*, S4Grz, ...) applies on all sound recursively > enumerable extensions of Peano Arithmetic. With comp it applies to us as > far as we are self-referentially correct, which is hard to know, especially > when betting on a personal digital substitution level. > It's all very exciting. I have a lot of learning to do. Right now I'm doing a lot of self study on logic, categories, toposes, sets, and so forth. Slow but rewarding work. > > > 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-list@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. > -- Joseph Knight -- You received this message because you are subscribed to the Google Groups "Everything List" group. To post to this group, send email to everything-list@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.
