On 23 Mar 2015, at 21:50, Telmo Menezes wrote:
On Sun, Mar 22, 2015 at 6:19 PM, Bruno Marchal <[email protected]>
wrote:
On 21 Mar 2015, at 21:38, Telmo Menezes wrote:
It is the p in []p & p, which makes "machine's knowledge" not
definable in term of number and machine. S4Grz formalizable at a
level, what the machine cannot formalize about herself (but can
bet on, ...).
Thanks to incompleteness, the Theaetetus' definition makes sense,
and distinguish the knower from the rational believer for the
machine.
Don't hesitate to ask precision. I am very literal here: the
knower is defined by the true believer. It is a modest definition
of knowledge, and it is not similar with "I know for sure that",
which needs some amount of consistency (like <>t, or <><>t, or
<><><> t, etc.).
What's the difference between <>t and <><>t and so on?
In the Kripke semantics, <>p means that you can, by starting form
the world you are in, access to another world where t is true. It
means that you are not in a cul-de-sac world. It means that you are
"alive", you can access some world. But <>t -> <>[]f. So you
despite being alive, you might be dead in that next world. That
next world might be a cul-de-sac world, where <>t is false, and
thus []f is true. Now, if you are in a world where <><>t is true,
then you can access a world in which <>t is true, so that you are
still alive.
<>t = I can access some world (t is true in all worlds), but that
world might be a cul-de-sac world.
<><>t = I can access some world where <>t is true, so from there I
can access some other world.
Put differently:
<>t I am alive (but can die at the next instant)
<><>t, I am alive and I can access to an instant where I am still
alive.
Ok, but it's not obvious to me how temporality (a sequence of
instants) is introduced here.
Here, it is "introduced" simply through the Kripke semantics of the
modal logic involved, G in this case.
Keep in mind that we are in arithmetic. <>t abbreviates ~beweisbar
'~( 2+2=4').
here '~( 2+2=4' denote some number, denoting some falsity. It is
equivalent with the arithmetical
consistent('2+2=4'), which is true, but not provable by the system
itself.
By Gödel's completeness theorem, which applies still on most correct
machine if they follow some recommendation in their way of talking,
consistent('p') is equivalent (from outside) with "there is a model
which satisfy my beliefs and p".
So, literally, <>p means if you add p to my beliefs, it will not
leads to a contradiction (semantically: a cul-de-sac world)
So, there is a sort of interpretation of <>p in "there is some
reality in which p is true", and, as t (true) is true in all worlds,
you can interpret <>t by "there is a world" (or there is a reality,
or there is some truth, or there is some god, or ...).
Ok got it.
[0]p = []p, and obeys to G, and fully described by G* (at the
propositional level).
[1]p = []p & p, and obeys to S4Grz,
[2]p = []p & <>t obeys and define the logic Z
[3]p = []p & <>t & p
I definitely don't understand [2]p and [3]p.
[]p & <>t is a weakening of []p & p. Instead of asking p being
true, we ask only for p being consistent
(([]p & <>t) -> ([]p & <>p)).
If you can prove for all p that []p -> p (like with [1]), then you
can prove for all p []p -> <>t or []p & <>p.
So the logic of provability-and-consistency is weaker than the
logic of provability-and-truth.
Provability and consistency avoids the probability one for the
false, which would exist if we take []p as provability. The passage
[]p =====> []p & <>p, approximate the main things for a probability
one.
What does "provability one" mean?
Come on Telmo, it takes me a lot of concentration to write
"probability" instead of "provability", with those damn "b" and "v"
which are so much together.
It's a bit funny that you find this to be a problem and meanwhile
write long emails where half of them are square brackets, arrows and
other weird notations :)
And in our case the distinction is of importance, and can be made
quite clear in arithmetic:
Provability is beweisbar , what is translated in the modal logic of
provability by the box [], usually []p.
Probability is beweisbar-and-consistent, the []p & ~[]~p, or
(equivalent) []p & <>t.
The difference is that with Provability, we can access cul-de-sac
world, in which you have []f. (= ~<>t).
For proVability, we need to add the "by-default hypothesis" that we
will not die during the experience.
When you bet on a coin: the events
Ok, so even if you prove you have to bet on consistency, right?
Not necessarily. PA can prove that 2+2=4 without betting on
consistency. If PA bet on consistency, it would mean to add
consistency as a new axiom. If done cautiously if speeds PA.
But are you saying then then that cul-de-sac worlds are not
consistent?
They are consistent. "inconsistency" is true there, but inconsistency
does not imply the false there.
You don't have to take those semantic literally, but that helps for
getting familiar with the logic.
In the logic of "life/intelligence", to be alive means to be in a
transitory world. To be dead means to be in cul de sac world. In a cul-
de-sac world <>t is false, and so []f is true. But false f is false
there, so it illustrates well the consistency of inconsistency. <>p ->
~ []<>p is equivalent, in the Kripke semantics, to say that all
transitory worlds access to a cul-de-sac world. We die at each
instant, or we can die at each instant, in that semantics.
Babies knows an instantiation of that theory, where <>t means "I stand
up", and []f means I fall on the ground. <>t -> []<>f (equivalent with
<>t -> ~[]<>t) means "If I stand up, It stands up that I fall on the
ground" (it works in french as stands up is the same as making sense,
and that is the main point of Gödel *completeness* theorem.
{H} or {T}, {H, T} have probability one, because semantically we
abstract from the asteroïds which can smash the playing table, the
dice and the betters.
By forcing <>t on each state (like Theaetetus did with the truth) we
abstract from the cul-de-sac world, by imposing the existence of
some accessible world.
Why are cul-de-sac worlds not accessible?
They are, but no more with the intensional variants [2]p = []p & <>t.
Z proves <2>t, but no more [2]t.
Like the Kripke world become self-accessible when you define [1]p =
[]p & p.
I never explored these ideas very thoroughly (I suspect they have
been discussed to death here before my time).
Since Pythagorus. Well as far as we can see. But Pythagorus was a big
traveller, and keep notes.
You propose that comp entails quantum immortality, correct?
IF QM is correct. But comp entails comp immortality, even if QM is non
correct.
It is not a simple subject. It is not much that comp entails
immortality, it is more than mortality is not provable, nor make much
sense for most self-referential modalities.
Logically, at first sight, it looks like a weakening of Theaetetus'
idea of restricting []p on the truth, but arithmetically, or
mechanicalistically (if I can say), that is by incompleteness, it
appears that replacing "p" by <>p, is an strengthening, yet dual of
some sort of []p.
You might need to revise a little bit the Kripke semantics of modal
logic, and the arithmetical logic of (machine) self-reference. It
works also for machine + oracles.
Ok.
It models what the guy in Helsinki can be sure if, like drinking a
cup of coffee (in the protocol where he get a cup in both W and M).
It abstract (locally) from the cul-de-sac world. It use the bet on
<>t implicit in the yes-doctor.
I don't know about the cup of coffee protocol either, could you
explain it?
Imagine that you are in Helsinki, and you will be duplicated (cut
and copied) and sent (by waves) to Washington and Moscow, where you
are reconstituted-reincarnated, OK?
But this time, we add in the protocol that both in Moscow, *and* in
Washington, they will offer a cup of coffee to the reconstituted
person.
The question (that, btw, I have asked many times to J. Clark without
any answer) is: what is your expectation, when you are still in
Helsinki (of course) of drinking a cup of coffee after the
duplication?
Of course, we, including the guy in Helsinki, *assumes*
computationalism. We assume the correctness of the substitution
level chose, and we agree with the default hypotheses (no
asteroïds). We already agree that the expectation of drinking a cup
of coffee is the same (modulo comp and the default hypothesis) after
a simple digital teleportation than with using a plane (assuming it
does not crash and the usual default hypotheses).
So, what do you think?
Ok, I think the expectation is the same (p_coffee = 1).
Thanks for reassuring me.
What the Löbian Universal Machine thinks, is that provability,
knowledge, observable, sensible, obeys different modal logics, and
that most of those modalities splits into a justifiable part and a
non justifiable part.
Then we can test the theory by comparing the machine internally
defined notion of observable ([]p & <>p + p sigma_1) with the
empirically observable. Curiously, at first sight, is that the
quantum only appears on the non justifiable part(*), but that is
normal: physics is first person plural, and that is (arguably)
confirmed: QM (without collapse) makes the splitting of observers
contagious to their colleagues. If you look at the schroedinger cat,
the story differentiates into a story where you see the dead cat,
and a story where you see the cat alive, but the day after, when
your colleagues (in the respective stories) ask you how was the cat,
they will split too at the occasion. To be sure, they would have
already splitted/differentiated, by the natural gossip of the
sufficiently hot environment.
It *does* look like the quantum aspect of reality is explained by
the way the sigma_1 arithmetical truth can look to itself, in the
observable mode.
Bruno
(*) (Z1*, X1*, not X1 nor Z1. To be sure a quantization and a
quantum logic also appear on S4Grz1 which does NOT split. The outer
God does not add anything to what the inner God already knew. And,
now, the inner god has already a foot in matter! This shocked my
intuition, as it makes matter still more on the first person side
than I thought, but it fits better with Plato, Plotinus, East and
West Mystics, and even with the salvia reports and some other
reports you can find on Erowid or on Salvia webpages.
Ok, most of what you say here makes sense to me intuitively, but
there are some technical aspects that I have to study by myself, I
think (I study some modal logic when I have time, but the progress
is slow).
Modal logic is to self-reference what tensor calculus is to
relativity. Just a tool.
We have to be careful, as there are tuns of modal logic (even a
continuum between S4 and S4Grz, I think). Here the modal logics G and
G* are just deep sum up of what Ideal machine can prove about
themselves in the third person way. The real result which starts all
this are the incompleteness theorems.
The bomb is really Gödel 1931, and the Church-Turing-Post thesis. The
modal logic are just the telescope.
We might come back on this. Still a bit overwhelmed for some time.
Have you the book "Forever undecided" by Smullyan? It is a gentle
introduction to the modal logic G, in which all the others are
represented/emulated, including G*.
Thanks!
The pleasure is mine.
Bruno
Telmo.
Thanks!
Telmo.
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to everything-
[email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google
Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it,
send an email to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
http://iridia.ulb.ac.be/~marchal/
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.
