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.
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.
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.
