On 24 Aug 2012, at 12:15, Roger Clough wrote:
Hi Bruno Marchal
Could you explain a little about Bp & p duality ? Are they both
analytic, or does one of them us synthetic logic ?
I void using "synthetic" and "analytic". Bp is a modal formula and its
interpretation here is provable('p') where provable is Gödel
provability predicate, entirely defined in arithmetic,, and " 'p' " is
for the arithmetical description of some sentence of arithmetic, but
'p' is for the arithmetical proposition itself, which cannot be
described as such. Bp & p means that the machine can prove that she
can prove p, and that it is the case that p, or, if you prefer that p
is true for the machine (believed by the machine).
By incompleteness, the machine cannot prove Bf -> f (provable "0=1"
implies that 0 = 1). That is equivalent with ~provable (false), which
is equivalent with "I am consistent", with a third person description
of I.
So, if the machine is sound, we do have Bf -> f, but the machine
cannot know that. Yet, Bf & f typically implies false (as p & q
implies p). So, although Bp & p is equivalent with Bp (both proves the
same proposition of arithmetic) they obeys very different logic. Bp
obeys to the modal logic G, and Bp & p obeys to the modal logic of
knowledge S4.
You cannot define "Bp & p" in arithmetic, by a general arithmetical
predicate, and this makes the machine first person "I" quite non
analytical, as no third person description can ever be used for it,
from the machine perspective.
This explains why the mind-body problem befuddled the machines until
they realized their own universality and the incompleteness which
follows. That is quickly the case for universal machine believing in
the induction axiom, (having them as pre-wired axioms) which provides
them very deep cognitive abilities.
So you can see Bp as analytical, having third person description, like
in arithmetic, and you can see Bp & p as synthetic, as it cannot be
defined in term of the ontological element of the theory, nor any
third person construction made on them.
Bruno
Roger Clough, [email protected]
8/24/2012
Leibniz would say, "If there's no God, we'd have to invent him so
everything could function."
----- Receiving the following content -----
From: Bruno Marchal
Receiver: everything-list
Time: 2012-08-23, 14:17:50
Subject: Re: Male Proof and female acceptance of proof
On 21 Aug 2012, at 21:42, Stephen P. King wrote:
On 8/21/2012 2:28 PM, Bruno Marchal wrote:
On 21 Aug 2012, at 12:12, Roger Clough wrote:
Hi Bruno and Stephen,
This is the bicameral mind again. Right brain must accept left
brain decisions for human safety.
Ought must rule over is (or else we'd all be nazis, Hume, for the
safety of humanity)
Passion must rule over reason (or else we'd all be nazis, Hume,
for the safety of humanity)
Acceptace of proof dominates proof (common sense psychology)
Thus you can objectively, mathematically prove that 2+2=4, but
you still have to subjectively accept that psychologically.
Woman always gets the last word.
No problem here. That fits nicely with the Bp versus Bp & p
duality, which is just the difference between "rational belief"
and "rational knowledge" (true rational belief).
It took time to realize that when we define the rational belief by
formal proof, which makes sense in the ideal correct machine case,
although knowledge and belief have the same content (the same
arithmetical p are believed), still, they obey to different
logics. This is a consequence of incompleteness. Rational beliefs
obey to a modal logic known as G (or GL, Prl, K4W, etc.) and true
rational belief obeys to a logic of knowledge (S4), indeed known
as S4Grz.
G is
[](p -> q) -> ([]p -> []q)
[]p -> [][]p
[]([]p -> p) -> []p
with the rules A, A->B / B and A / []A
S4Grz is
[](p -> q) -> ([]p -> []q)
[]p -> [][]p
[]([](p -> []p) -> p) -> p
with the rules A, A->B / B and A / []A
Bruno
Dear Bruno,
It might help us immensely if you could tell us how to read
these symbolic representations. Not all of us speak that language!
There are English words for all of these symbols!
???
The only differences with elementary propositional logic are that we
have one symbol more, the box "[]", and one more inference rule.
It is a unary operator symbol, so if X is a formula, []X is a
formula, like ~X.
The inference rule is that you can derive []p from p. Careful, this
does not make p -> []p true in most modal logic.
I wrote often the box [] by using the letter B.
In the axiom above, it is better to not interpret the box, as this
can confuse with the representation theorem which associate
"meaning" mathematically.
I have often talked about Bp and Bp & p, with Bp having the
arithmetical provability meaning (G鰀el 1931).
G above is the logic of G鰀el's beweisbar predicate. For example the
second incompleteness theorem is given by Dt -> ~BDt, or <>t ->
~[]<>t, or consistent('t') -> NOT PROVABLE (CONSISTENT 't')), with
for example t = "0=0", et 't' = G鰀el number of "0=0".
S4Grz above is the corresponding logic of the first person
associated to the machine, given by beweisbar('p') & p, following
Theatetus, and then Boolos, Goldblatt, Artemov. I have provided many
explanations on this list, including an introduction to modal logic
and the Kripke semantics, but you can also open some book in logic
to help yourself.
G and S4Grz are the two machineries illustrating (and formalizing
completely at the propositional modal) two important arithmetical
hypostases discovered by the UM when looking inward. G is the logic
of third person self-reference and S4Grz is the logic of the first
person self-reference.
There are six other hypostases, or machine's points of view, three
of them playing a role in the "creation of the collective persistent
matter hallucination. Comp makes obligatory that persistence, and it
can be tested, and it can be argued that the presence of p -> []<>p
as a theorem in SGrz1 and Z1* and X1* confirms it in great part.
Interactions can be defined in a manner similar to Girard, and then
tested on those "material hypostases". I think that this is
explained in the second part of the sane04 paper.
The "1" added to the system refers to the fact that we eventually
limit the arithmetical translation of the sentence letters (p, q,
r, ...) to the sigma_1 sentences, which "models" the UD in arithmetic.
In particular Richard Ruquist's theory that fundamental physics is
given by string theory becomes testable with respect to comp, as UDA
shows that the physics is entirely retrievable from the S4Grz1, Z1*
and/or X1*, and their first order modal extension.
It is not as difficult as most paper your refer to, and it is only
one paper, and you got the chance to ask any question to the author :)
You recently allude to a disagreement between us, but I
(meta)disagree with such an idea: I use the scientific method, which
means that you cannot disagree with me without showing a precise
flaw at some step in the reasoning.
You seem to follow the seven first steps, so that in particular you
grasp apparently that COMP + ROBUST-UNIVERSE entails the reversal
physics/arithmetic, and the explanation why qualia and quanta
separate. Are you sure you got this? Step 8 just eliminates the
"ROBUST-UNIVERSE" assumption in step 7.
Then AUDA translates everything in UDA in terms of numbers and
sequences of numbers, making the "body problem" into a problem of
arithmetic. It is literally an infinite interview with the universal
machine, made finite thanks to the modal logic above, and thanks to
the Solovay arithmetical completeness theorem.
You cannot both claim that there is a flaw, and at the same time
invoke your dyslexia to justify you don't do the technical work to
present it.
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 [email protected].
To unsubscribe from this group, send email to [email protected]
.
For more options, visit this group at http://groups.google.com/group/everything-list?hl=en
.
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 [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
