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
>slow.
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
theories
sufficiently rich to prove elementary theorem in arithmetic, or in any
richer
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
rule?)
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
argues
(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
sentences
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*
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
the
proving machine), and []p is interpreted by Bew('p'), with 'p' a
description
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
>are
>both true but unprovable?
Yes I am saying that. (I recall for the other that c is "<>true", or
-[]false,
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,
Bruno
Received on Fri May 11 2001 - 03:55:16 PDT
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:07 PST