On 14 May 2015, at 20:44, meekerdb wrote:
On 5/14/2015 10:33 AM, Bruno Marchal wrote:
Then the math confirms this, as proved by the Löbian universal
machine itself, as on the p sigma_1, the first person variant of
the 3p G ([]p), that is []p & p, []p & <>t, and []p & <>t & p,
provides a quantization (namely [i]<i>p, with [i] being the
corresponding modality of the variants).
Went over my head. Can you expand on that?
What can an ideally correct machine proves on itself, at the right
level by construction? This can be handled with using the self
provided by the second recursion theorem, or the little song if D'x'
gives 'x'x'' what gives DD. The song is singed by some universal
system understanding the notation.
The math gives here the Beweisbar predicate of Gödel, for the finite
entities believing in enough induction axioms, which I call the Löbian
numbers or the Löbian combinators (depending if there is a "r" in the
month).
If you interpret the propositional variables (p, q, r ...) by
arithmetical propositions, and the modal box []p by beweisbar(code of
p in the language of the machine), Gödel and Löb's theorems prove the
soundness of the formula ~[]f -> ~[]~[]f , and []([]A->A)->[]A, etc.
Indeed Solovay's theorem will prove that G and G* characterize what
the machine can prove about its provability and consistency abilities,
and G* describes what is true about them.
If you define generously a mystic by any entity interested in its
self, then G is the abstract mystical science, and G* is the abstract
mystical truth.
Gödel already saw that G, well, it is not a logic of knowledge, like T
([]p->p), or S4 ([]p->p, []p -> [][]p).
This means, that contrarily to the intuition of some mathematicians
and scientists, formal provability is of the type belief, not
knowledge. But this gives the opportunity to define knowledge by using
Theaetetus idea: [k]p = [g]p & p, with [g] = the usual beweisbar [] of
Gödel. This does fit with Tarski mathematical analysis of truth, where
"il pleut" is true when it rains.
This leads to a (meta) definition of a knower, indeed axiomatized
soundly and completely by the modal logic S4Grz. Grz for Grzegorczyk
who discovered an equivalent formula, in the context of topological
interpretation of intuitionisic logic. Indeed S4Grz provides an
arithmetical (self-referential) interpretation of intuitionistic logic
(which the first person will be, from her own perspective).
But we want a probability measure of those things accessible by the UD.
G has a Kripke semantic. In particular, there, there are cul-de-sac
world everywhere, and they do contains sorts of white rabbits, as []f
is true in those cul-de-sac world. To get a probability, we need to
have the D axiom ([]p -> <>p).
What about the measure one? It is simpler to extract it than a measure
different from one. Recall what I asked 10 times to John Clark: you
are in Helsinki (so you are PA+"I am in Helsinki", say), and you will
be duplicated and reconstituted in Washington and Moscow, and you are
told that both reconstitutions will be offered a coffee cup. We want
to say that []A would do, as by completeness it entails truth in all
models, in particular true in all consistent extensions (PA + "I was
in Helsinki" + "I am in Moscow" + I got a cup of coffe"), and (PA + "I
was in Helsinki" + "I am in Washington" + I got a cup of coffee").
But [] does not intensionally acts like that and D is false, so to get
it you have to add explicilty that there is a consistent extension.
[b]p = []p & <>t (in Kripke semantic: "<>t" means that there is a
"world" in which t exists, as t is true in all worlds, this amount to
say that there is a world: it is a default hypothesis (an instinct)
made explicit. the "b" of [b]p is for bet.
To get physics, through comp, you have to restrict the local
continuations to the UD's work, or to the sigma_1 reality.
So the propositional logic of physics (the logic of yes no experiment)
must be given by the logic of [b]p with p sigma_1 sentence.
Then it happens that quantum logicians have already a nice
representation of quantum logic in modal logic, and roughly a modal
logic known as B, (with main axiom []p -> p, p -> []<>p) interpret
quantum logic through a quantization of the classical proposition
([]<>A, that is B proves []<>p for the atomic proposition when and
only when quantum logic proves p).
Now, the three of SGrz1 ( = S4Grz restricted to the sigma_1), Z1* (the
part of Z, restricted to sigma_1, and proved by G*, when translated),
X1*, provide such a quantization, and a corresponding different
quantum logics.
Nobody complained that I got three quantum logics. But then as Van
Frassen said: there is a labyrinth of quantum logics, and here comp
provides a sort of etalon.
All logic can be proved to be emulated/represented by the decidable
logic G, so they are all decidable, and with the exception of the X
logics ([]p & <>t & p), they have been axiomatized.
From Gödel's "[]p" we do three things:
- intensional nuances (from []p to []p & <>t, ...)
- restriction of the arithmetical truth to the sigma_1 arithmetical
truth
- views going from G to G* (the proof/truth nuances)
Without incompleteness (a quasi-obvious consequence of Church thesis),
all those nuances would have collapsed into classical propositional
calculus.
Feel free to ask any precision.
Bruno
Brent
--
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.
