George Levy wrote:

>Thanks Bruno.... this is much more than I bargained for... I can barely keep
>afloat...I have a lot of homework to do.
>I am also very busy these days with my regular work so I don't mind going

Let us going slow. 

>Just a couple of questions:
>1) What is Godel's "Bew". Probably not something he drank.

"Bew" is Godel's provability predicate. Bew is for "beweisbar" which means
"provable" in German. Bew(x) or  Bew x  means x is provable. (x being a
representation of a sentence in the language of a fixed theory 
or proving machine under discussion).

What Godel did was to show that it was possible to translate Bew(x) in 
sufficiently rich to prove elementary theorem in arithmetic, or in any 
theory T. You can also think at T as a proving machine.
Let us fix such a machine/theory T. 
Godel shows that "T proves p" can be translated in the language of the T.
(The basic reason is that if T proves p there is a formal proof q of p 
from the
axioms of T, and there is a mechanical procedure for verifying that q is 
a proof
of p, and mechanical procedure can be represented (mirrored) in T).
This is what is tedious to show precisely if T is arithmetic. It is as 
simple as 
programming in *machine language* and as boring too! 
I am still thinking how to do that in some friendly way ...

Godel Hilbert Bernays Lob shows then that (I sum up some stories here):

T proves p   entails   T proves Bew(p)  (do you smell the Necessitation 
T proves Bew(p->q)->(Bew(p)->Bew(q))    (do you smell the K formula?)
T proves Bew(p) -> (Bew(Bew(p)))        (do you smell the "4" formula?)

For any p q arithmetical propositions.

So you see that if you take the modal system K4 + MP,Nec, you get a sound
axiomatisation of the provability in T.

A natural question is: is K4 a complete axiomatisation of T provability?

The answer is no. 

For exemple K4 does not prove <>t -> -[]<>t    (t = true)
But the machine proves , for any p arithmetic, (con p) -> -(bew con p);
(con p is - bew -p, of course).
(The machine proves the Godel's second theorem as Godel convincingly 
(but it has been Hilbert and Bernays who proved that in all details).

Is K4C + MP,Nec   (with C = <>p -> -[]<>p)   complete then?

The answer is still no.

Well, you know the answer of course: Solovay will prove that the system
KL + MP,Nec is a sound and complete axiomatisation of the provable 
on the provability by
the machine. KL + MP,Nec is the system G.

And Solovay gives us a little more: The system [all theorems of G] with
the formula []p->p + MP (but without Nec!!!) is a sound and complete
axiomatisation of all the *true* sentences on the provability by machines.

[all theorems of G] with the formula []p->p + MP (but without Nec!!!) is 

G* proves also the true but unprovable sentences by the machine, like the
machine's consistency ( <>t ).

So the corona G* \ G   (\ = set difference)  formalises the true but
unprovable (by T) provability sentences. 
In some sense, G* \ G captures the incompleteness realm. It is a decidable
set as are G and G*. (a set is decidable if you can mechanically verify
if something belongs or not in the set).

Later I will give you the rigorous relationship between provability logic
and the modal systems. En gros the propositional variables are interpreted
by arbitrary arithmetical sentences (or any sentences in the language of 
proving machine), and []p is interpreted by Bew('p'), with 'p' a 
of p in the language of the machine. Of course it follows that <>true will
be interpreted by con(true).

>I am not sure if I understand. You are saying that  c and (c -> -[]c) -> c 
>both true but unprovable?

Yes I am saying that. (I recall for the other that c is "<>true", or 
                         it is the machine (self)consistency statement)

> So the statements "I am" and
>"I think therefore I am" is not provable?

I appreciate your interpretation of "<>true" as "I am", although strictly
speaking it is "I am consistent".
Slezak interprets, like you, (c -> -[]c) by I doubt/I think. I prefer to
translate I doubt by something like (c-> (-[]c & -[]-c)), but in any case
that remains unprovable (but true: it belongs to G* \ G). 

Well, you know that the cartesian doubt cannot really give a communicable
proof that you exist, how convincing it can appear to you!

>You say:
>the GA can prove   # -> c  (# = any proposition).
>Interestingly the reverse
>c -> #
>means that if there is a consciousness, then the plenitude exists, I 
>think, or
>maybe more appropriately from the relativistic point of view, if "I am" then
>"the plenitude is."

I'm afraid you misinterpretes  #.
When I say # is for any proposition, it is really *any* proposition
including the false proposition. So the reverse "c -> #" is certainly
false (when # is for a false proposition).

>It would be interesting to see if we can derive the Anthropic principle.
>c -> W
>and the principle of sufficient reason
>W  -> #
>from logic.

I propose we come back to this later. But don't hope too much because I
will not try to tackle quantified provability logic (and quantified modal
logics) which I think would be needed for expressing Leibnizian principle
or other sophisticated philosophical principle. We will see.
(The miracle is that I will not need to make that move for extracting the
quantum probabilities (well the particular case of probability one)).

>The question is how to define W, "that specific world that
>sustains the existence of c.

Note that I don't really think that world will be necessary. 

>Take your time....

You too. Just try to range in some order the posts so that I can refer
to them occasionally.

I am thinking for giving you the crux of the proof in a nutshell.

Have a good week-end,


Reply via email to