# Re: COMP theology

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