On 15 Feb 2009, at 23:00, russell standish wrote:

> On Sun, Feb 15, 2009 at 06:41:08PM +0100, Bruno Marchal wrote:
>>>> A good and important exercise is to understand that with the Kripke
>>>> semantics,  ~Dt, that is B~t, that is Bf, that is "I prove 0=1", is
>>>> automatically true in all cul-de-sac world. It is important because
>>>> cul-de-sac worlds exists everywhere in the Kripke semantics of the
>>>> self-reference logic G.
>>>> If you interpret, if only for the fun, the worlds as state of life,
>>>> then Bf is  really "I am dead".
>>>> Bruno
>>> Yes, but I have difficulty in _simultaneously_ interpreting logic
>>> formulae in terms of Kripke frames and B as provability. In the
>>> former, Bp means in all successor worlds, p is true, whereas in the
>>> latter it means I can  prove that p is true.
>>> How does one reconcile such disparate notions?
>> By Godel's theorems, Löb's theorems and Solovay theorems.
> ...
> The following snip did not answer my question on how one can
> simultaneously have Kripke semantics and provability semantics. Never
> mind.

It is technical. It just happen that the logic of the self- 
referential, or Gödelian Beweisbar provability predicate is completely  
and soundly axiomatized by the modal logic G and G*. And the modal  
logic G belongs to the type of logic which possesses a  
characterization in term of a Kripke semantics. (note that G* losses  
the Kripke semantics).

> I'm helping Kim Jones with the translation - maybe it'll make more
> sense when we get to that bit.

Thanks for helping. I will think about how to explain AUDA in simple  
terms. UDA shows that physics is in your head. AUDA shows that physics  
is in the head of any universal digital machine. This transforms the  
mind-body problem into a pure mathematical problem, or sequence of  
mathematical problems. Then we can compare the physics in the head of  
the machine and physics "out there", and so we can test the comp hyp.

Let me give a short try, for helping to answer your question of the  
reconciliation of Kripke multiverse and provability. It is standard  

Godel's second incompleteness theorem 1931 says that if the formal  
system Principia Mathematica PM is consistent then PM cannot prove  
that PM is consistent. Gödel did already completely understand that PM  
was able to prove its own incompleteness theorem (although the  
detailed proof will be given by Bernays and Hilbert later (and then  
brillantly simplified by Löb)).
PM can prove that if PM is consistent then PM cannot prove that PM is  
consistent. More simply: PM proves that "IF I am consistent, then I  
cannot prove that I am consistent":

PM proves    NOT(BEWEISBAR(FALSE)) ->  

where BEWEISBAR is Gödel's 1931 provability predicate, and FALSE is  
some Gödel number representing the statement "0 = 1" in PM language.  
The whole is a first order arithmetical sentence.

Now that first order arithmetical sentence look like a modal  
statement. Writing NOT with "~", BEWEISBAR with a box "B", and FALSE  
with f, the formal, that is really the one output by the machine or by  
the formal system becomes

~Bf -> ~B~Bf

or with the diamond (B~p is equivalent with ~Dp, and D~p is equivalent  
with ~Bp). t is ~f.

Dt -> DBf, which provides the reading that "If I am consistent then it  
is consistent that I am inconsistent".

Already here, given that this is a modal statement, it is natural to  
ask oneself if there is a Kripke "multiverse" satisfying that modal  
A Kripke multiverse satisfies a statement when the statement is true  
in all worlds of the multiverse. A multiverse here is just a set of  
worlds with an accessibility relation.

How to find an accessibility relation making the statement "Dt -> DBf"  
true in all worlds of a multiverse?

If Dt is true in a world ALPHA, say, you need to have DBf true in that  
world ALPHA  too (you want "Dt -> DBf" true everywhere!). But to have  
DBf true in ALPHA, you have to be able to access (by the accessibility  
relation) a world where Bf is true. (By the definition of Kripke  
semantics). But Bf can be true only in cul-de-sac worlds (if not f  
would be true in some world). So ti have Dt->~BDt, or Dt->DBf, you  
have to live in what I called a Papaioannou multiverse, or a realist  
multiverse (in Conscience et Mecanisme), that is a multiverse where  
all worlds have an access to a culd-de-sac world.

The same remains for the generalisation Dp -> ~BDp (equivalently Dp ->  

Now, if you remember that ~p is equivalent to p -> f (or redo the two  
lines truth table), you can write consistency, Dt, that ~Bf as Bf->f,  
by simple transformations:

~Bf -> ~B~Bf is equivalent with
B~Bf -> Bf by contraposition. And this is equivalent (by Bf equivalent  
with Bf -> f).


The generalization (f/p) of this formula gives the Löb formula B(Bp- 
 >p)->Bp, which is the formal (machine) version of the theorem of Löb,  
which indeed says that if PM proves BEWEISBAR('p') -> p then PM proves  
p. (Curiously enough, Boolos 1993 gives five reasons to be  
astonished!). See the arithmetical placebo in the same2004, or the  
"proof" of the existence of Santa Klaus, in the archive or Bools'  
books, or better Smullyan which varies about that theme in Forever  

Solovay shows that in the normal modal logics, Löb's formula, B(Bp->p)- 
 >Bp, axiomatizes completely the logic (G) of provabilty.

Now B(Bp->p)->Bp has more complex Kripke semantics, but one of them is  
given by the finite transitive irreflexive multiverse. You can verify  
this by hand on simple examples. Not only you have always access to  
dead end (cul-de-sac world), but all your path end somewhere. In term  
of life (which fortunately will NOT concern the first person), not  
only you can die at each "om", but you will eventually die. But as I  
say, and Torkel Franzen did see something similar here, the G world  
are not "OMs"; the G logic is really third person self-reference (its  
modal world are not OMs: it is more a logic of scientific  
communication than a logic a first person knowledge. The amazing  
things which I exploit, is that we can study the logic of the first  
person knowledge attached to the machine, despite it can be shown that  
the first person is not definable by the machine, or by PM, PA, ZF,  
whatever rich classical theory or Löbian machine. You cannot define  
the notion of first person, or of consciousness, or even the notion of  
Truth in the language of any (consistent) machines. Yet machines can  
reason about those notion indirectly. The trick is already in the  
Theaetetus of Plato, or even used by Plotinus (as Bréhier, the first  
french translator of Plotinus, suggested).
All this will concern all the mechanical or less mechanical consistent  
extensions of those machine or theories.

Hope this gives some clues. I guess we can come back on this. AUDA is  
technical for sure. G and G* is just two hypostases, but the others  
come from them.



You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To post to this group, send email to everything-l...@googlegroups.com
To unsubscribe from this group, send email to 
For more options, visit this group at 

Reply via email to