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
material.
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)) ->
NOT(BEWEISBAR(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
statement.
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 ->
DB~p).
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).
B(Bf->f)->Bf
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
Undecided.
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.
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.domain.name.hidden
To unsubscribe from this group, send email to everything-list+unsubscribe.domain.name.hidden
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en
-~----------~----~----~----~------~----~------~--~---
Received on Mon Feb 16 2009 - 14:04:58 PST