MODAL+Re: [foar] Amoeba's Secret, by Bruno Marchal available from Kindle store

25 views
Skip to first unread message

Bruno Marchal

unread,
Apr 11, 2014, 11:10:27 AM4/11/14
to fo...@googlegroups.com
On 10 Apr 2014, at 03:52, LizR wrote:

> I received my copy yesterday and am up to page 25. Very interesting
> so far, and "discretely charming" :)

Thank Liz. I was euphoric when writing it, as I thought that 20 years
of stress would end up, but I was naive.
I feel like I should write a sequel, but I have not the mind up to it.
Yet there would nice chapters, like the everything-list, Plotinus,
Salvia divinorum, Eric Vandenbussch (who solved the first
conjecture), ... But also more dark chapters. Not sure I could avoid
9/11, climate changes and the general problem of the (Löbian) possible
deception(s). How far nature and arithmetic play that game already ?
You can interpret the formal "Gödel incompleteness theorem", <>t ->
<>[]f, into the machine's understanding that if she is in the lucky
situation where shit does not happen, then, necessarily shit can
happen. We are warned at the real start!
May be it is time to reread Alan Watts "The wisdom of insecurity".

Tell me, do you know the second incompleteness theorem? Do you see it
is <>t -> ~[]<>t, or ~[]f -> <>[]f? (When Gödel's provability
predicate beweisbar('p') interprets []p in arithmetic, with 'p' being
a number describing p.

(I ask your for planning the sequel of the math thread, if you are
still interested).
Are you still trying to prove (W, R) respects <>A -> []<>A iff R is
euclidian? It is the last which remains.

I recall that the goal is the derivation of physics from arithmetic,
(through a detour in "machine theology").
This necessitates a good understanding of UDA1-7, and, a good
understanding of how to translate "provable(x)" in arithmetic.
The relation with computation is that provable(x) is sigma_1 complete
and defines a universal number/program/machine.
Comp can exploit a bit of computer science. There is no rush, but the
path is a bit long. I guess I will have to explain more on first order
logic. I have to explain enough so that you can grasp the enunciation
of the theorems used in the derivation.

Bruno



http://iridia.ulb.ac.be/~marchal/



LizR

unread,
Apr 12, 2014, 12:05:48 AM4/12/14
to fo...@googlegroups.com
I had forgotten that there was a problem remaining. My mind is rather fuzzy at the moment so I can't do it right now. I will have to look at it later...






--
You received this message because you are subscribed to the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this group and stop receiving emails from it, send an email to foar+unsubscribe@googlegroups.com.
To post to this group, send email to fo...@googlegroups.com.
Visit this group at http://groups.google.com/group/foar.

For more options, visit https://groups.google.com/d/optout.

LizR

unread,
Apr 12, 2014, 5:35:54 PM4/12/14
to fo...@googlegroups.com
(W, R) respects <>A -> []<>A
iff
R is euclidian  (meaning that if aRb and aRc, then bRc)  (sub exercise: show that if R is both reflexive and euclidean, then R is an equivalence relation (reflexive, transitive and symmetric. The converse is trivial). 

Euclidean-ness can be read as "all worlds accessible from a are accessible to each other. (I think this actually implies that all worlds that are accessible to a form a sub-multiverse of all possible worlds, which is like a mini Leibniz style multiverse. Or does it?)

(W, R) respects <>A -> []<>A can be read (I think) as

If there exists a proposition A that is true in at least one world accessible from world a, that implies that for all worlds accessible from a proposition A is true in at least one world accessible from that world.

Well if my supposition above it true (that all worlds accessible from a form a Leibniz type universe, an "island universe" which is completely interconnected within itself), then this has to be true.

But is my supposition correct? OI can't see what I've done wrong but I am still a bit fuzzy, I think I caught some bug...

Bruno Marchal

unread,
Apr 13, 2014, 11:03:08 AM4/13/14
to fo...@googlegroups.com
WARNING FOR BRENT:

The following post contains the proof of "if (W,R) is Euclidian, then
(W,R) respects <>A -> []<>A", given by Liz.

BTW, Liz gave a direct proof, you might try to find a proof by
reductio ad absurdum.

It does not contain the proof of the reverse: if (W,R) respects <>A ->
[]<>A then (W,R) is Euclidian, though.


On 12 Apr 2014, at 23:35, LizR wrote:

> (W, R) respects <>A -> []<>A
> iff
> R is euclidian (meaning that if aRb and aRc, then bRc) (sub
> exercise: show that if R is both reflexive and euclidean, then R is
> an equivalence relation (reflexive, transitive and symmetric. The
> converse is trivial).
>
> Euclidean-ness can be read as "all worlds accessible from a are
> accessible to each other. (I think this actually implies that all
> worlds that are accessible to a form a sub-multiverse of all
> possible worlds, which is like a mini Leibniz style multiverse. Or
> does it?)

It does. Well seen.




>
> (W, R) respects <>A -> []<>A can be read (I think) as
>
> If there exists a proposition A that is true in at least one world
> accessible from world a, that implies that for all worlds accessible
> from a proposition A is true in at least one world accessible from
> that world.

I was going to question the meaning of "accessible from a
proposition?" until I realize you meant "accessible from
alpha" (writing "a" for alpha). OK.
A comma would have helped (like in the NDAA!).


>
> Well if my supposition above it true (that all worlds accessible
> from a form a Leibniz type universe, an "island universe" which is
> completely interconnected within itself),

That is true. If you have some doubt, you should try to prove it a bit
more formally. That will also help you to understand the
"deducibility" notion later.



> then this has to be true.

That's right.


>
> But is my supposition correct? OI can't see what I've done wrong but
> I am still a bit fuzzy, I think I caught some bug...

Your "supposition" is correct, try to convince yourself of it.

But still, you have only prove that: if (W,R) is Euclidian, then
(W,R) respects <>A -> []<>A.

You forget again that we ask a proof of an "iff" statement. You must
still prove the reverse:

If (W,R) respects <>A -> []<>A, then (W,R) is euclidian.

Bruno


http://iridia.ulb.ac.be/~marchal/



LizR

unread,
Apr 14, 2014, 6:38:10 AM4/14/14
to fo...@googlegroups.com
You're right, by the time I had managed to reach the proof I had (again) forgotten the "iff" part. I will have to think about that too.


LizR

unread,
Apr 14, 2014, 8:11:48 PM4/14/14
to fo...@googlegroups.com
To recap here is the "if" part...
 
(W, R) respects <>A -> []<>A
iff
R is euclidian  (meaning that if aRb and aRc, then bRc)  (sub exercise: show that if R is both reflexive and euclidean, then R is an equivalence relation (reflexive, transitive and symmetric. The converse is trivial).
 
Euclidean-ness can be read as "all worlds accessible from a are accessible to each other. (I think this actually implies that all worlds that are accessible to a form a sub-multiverse of all possible worlds, which is like a mini Leibniz style multiverse. Or does it?)
 (W, R) respects <>A -> []<>A can be read (I think) as
 
If there exists a proposition A that is true in at least one world accessible from world a, that implies that for all worlds accessible from a proposition A is true in at least one world accessible from that world.
 
Well if my supposition above it true (that all worlds accessible from a form a Leibniz type universe, an "island universe" which is completely interconnected within itself), then this has to be true.

Well, if the multiverse is non-Euclidean, that means there is at least one aRb for which ~bRa (I think that's the correct symbol for not, or is it a sideways L?)

Hmm. A weaker case - it can have cul-de-sacs, so ~bRx, where x is any world including b. In this case we can have that A is only true in b, which means that []<>A isn't true because it isn't true in any world accessible from b.

Does non-Euclidean always imply cul-de-sacs? It may but I can't see that it does, so I will have to think some more.


Bruno Marchal

unread,
Apr 15, 2014, 12:34:51 PM4/15/14
to fo...@googlegroups.com
On 15 Apr 2014, at 02:11, LizR wrote:

To recap here is the "if" part...
 
(W, R) respects <>A -> []<>A
iff
R is euclidian  (meaning that if aRb and aRc, then bRc)  (sub exercise: show that if R is both reflexive and euclidean, then R is an equivalence relation (reflexive, transitive and symmetric. The converse is trivial).
 
Euclidean-ness can be read as "all worlds accessible from a are accessible to each other. (I think this actually implies that all worlds that are accessible to a form a sub-multiverse of all possible worlds, which is like a mini Leibniz style multiverse. Or does it?)
 (W, R) respects <>A -> []<>A can be read (I think) as
 
If there exists a proposition A that is true in at least one world accessible from world a, that implies that for all worlds accessible from a proposition A is true in at least one world accessible from that world.
 
Well if my supposition above it true (that all worlds accessible from a form a Leibniz type universe, an "island universe" which is completely interconnected within itself), then this has to be true.

Well, if the multiverse is non-Euclidean, that means there is at least one aRb for which ~bRa (I think that's the correct symbol for not, or is it a sideways L?)

There is no correct symbol in logic. Or all symbols are correct. You can use anything as a symbol for something. You could use whales for example. It might not be politically correct though, and non measurably unpractical, so, using a whale to symbolize negation is utterly ridiculous. Yet there is no sense to say that it would be an incorrect symbol.

Instead of living whales or cuttlefishes, logicians use little sign easily recognizable, and, very frequently logicians, on this planet, use the sideways L.
In fact, in books of logics, it happens that "~" is for negation. in many books "~" is for equivalence, although "<->" is more frequent. 
I would probably used the sideways L, if it was a standard mail symbol, like I would use ◊ instead of <> if Russell would update his mailing reader program :)

Coming back on the subject, I am not sure that non-Euclidian means there is at least one aRb for which ~bRa, or do you mean this in the cloud of some other world?   (with the cloud of alpha defined by the set of beta such that aRb).

Euclidian is defined by , for all a, b, c (aRb & aRc) -> bRc

In particular (aRb and aRb) -> bRb, and this implies the cloud of alpha being reflexive. Similarly you saw, or guess correctly, that, in the cloud of alpha, R will be symmetrical and transitive, making its cloud into a Leibnizian "sub-multiverse".

Now, being non euclidian will mean that there are a, b, c, such that ~((aRb & aRc) -> bRc) OK?
And "(aRb & aRc) -> bRc" is false if (aRb & aRc) is true, and  bRc is false.

For example {a, b}, with aRb (only) is non euclidian (but {a, b} with aRb and bRb, *is* euclidian.



Hmm. A weaker case - it can have cul-de-sacs, so ~bRx, where x is any world including b. In this case we can have that A is only true in b, which means that []<>A isn't true because it isn't true in any world accessible from b.

if beta, b, is a cul-de-sac world, <>A is always false, and so <>A -> []<>A is always true.

The set {alpha}, with R empty, so that ~aRa, is euclidian.



Does non-Euclidean always imply cul-de-sacs?

Why should that be? Imagine a multiverse with the cloud of some alpha being reflexive , like W = {a, b, c} and aRb, aRc, NOT (bRc), and thus not euclidian, and yet with bRb and cRc. It is non euclidian, and there is no cul-de-sac world.

On the contrary, the multiverse respecting <>A -> ~[]<>A, have necessarily cul-de-sac worlds. The "realist" multiverse.




It may but I can't see that it does, so I will have to think some more.


OK.
I will sum up the euclidian case, but I let you think more before if you prefer. 

Liz, I would suggest (advise?) you to always state clearly what you want to prove, before doing the proof. 
It will help you, ... and the reader.
It will help you doubly so in logic, where we reason about statements.

Bruno






--
You received this message because you are subscribed to the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this group and stop receiving emails from it, send an email to foar+uns...@googlegroups.com.

To post to this group, send email to fo...@googlegroups.com.
Visit this group at http://groups.google.com/group/foar.
For more options, visit https://groups.google.com/d/optout.

Russell Standish

unread,
Apr 15, 2014, 8:18:15 PM4/15/14
to fo...@googlegroups.com
On Tue, Apr 15, 2014 at 06:34:51PM +0200, Bruno Marchal wrote:
> In fact, in books of logics, it happens that "~" is for negation. in
> many books "~" is for equivalence, although "<->" is more frequent.
> I would probably used the sideways L, if it was a standard mail
> symbol, like I would use ◊ instead of <> if Russell would update his
> mailing reader program :)

Actually, my mail program has no trouble displaying ¬ - it's just ◊ or
◇ that causes problems. Bizarre. I don't know what it has against
lozenges or diamonds. Actually, it is not the email client that's at
fault here, but rather the font that that terminal window uses to
display it characters.

Actually, if I select the option "Unicode Best" under the font menu, I
can even get lozenges to display. The font appears ugly to my eyes,
but in time, I'd probably get used to it. I have now figured out how
to get that option selected by default when I start the email program,
so I'll suck it and see.

But it is probably not wise in general to assume email clients can
handle anything other than standard ASCII, unless you know the
specific capabilities of your correspondent. Which is why TeX markup
is often used.

Cheers
--

----------------------------------------------------------------------------
Prof Russell Standish Phone 0425 253119 (mobile)
Principal, High Performance Coders
Visiting Professor of Mathematics hpc...@hpcoders.com.au
University of New South Wales http://www.hpcoders.com.au

Latest project: The Amoeba's Secret
(http://www.hpcoders.com.au/AmoebasSecret.html)
----------------------------------------------------------------------------

Gary Oberbrunner

unread,
Apr 16, 2014, 9:19:49 AM4/16/14
to FoAR
How cool would it be if we could write TeX and have it show up as proper equations in email!  BTW, I use gmail's webmail in Chrome on Windows, and it has no problem with ¬, ◊ or ◇.  (That's sideways-L not, and two diamond/lozenge chars).


--
You received this message because you are subscribed to the Google Groups "Fabric of Alternate Reality" group.
To unsubscribe from this group and stop receiving emails from it, send an email to foar+uns...@googlegroups.com.
To post to this group, send email to fo...@googlegroups.com.
Visit this group at http://groups.google.com/group/foar.
For more options, visit https://groups.google.com/d/optout.



--
Gary

Bruno Marchal

unread,
Apr 16, 2014, 3:40:52 PM4/16/14
to fo...@googlegroups.com

On 16 Apr 2014, at 02:18, Russell Standish wrote:

> On Tue, Apr 15, 2014 at 06:34:51PM +0200, Bruno Marchal wrote:
>> In fact, in books of logics, it happens that "~" is for negation. in
>> many books "~" is for equivalence, although "<->" is more frequent.
>> I would probably used the sideways L, if it was a standard mail
>> symbol, like I would use ◊ instead of <> if Russell would update
>> his
>> mailing reader program :)
>
> Actually, my mail program has no trouble displaying ¬ - it's just
> ◊ or
> ◇ that causes problems.

Like in the cul-de-sac world. (I am joking)



> Bizarre. I don't know what it has against
> lozenges or diamonds.

Yeah! Machines are like that. They can develop prejudices.



> Actually, it is not the email client that's at
> fault here, but rather the font that that terminal window uses to
> display it characters.
>
> Actually, if I select the option "Unicode Best" under the font menu, I
> can even get lozenges to display. The font appears ugly to my eyes,
> but in time, I'd probably get used to it. I have now figured out how
> to get that option selected by default when I start the email program,
> so I'll suck it and see.
>
> But it is probably not wise in general to assume email clients can
> handle anything other than standard ASCII, unless you know the
> specific capabilities of your correspondent. Which is why TeX markup
> is often used.

No problem, the use of <> and [] has a lot of charm. B and D are often
used. Hughes and Cresswell, who wrote a nice book in modal use L and
M. There are no real standard notations.

http://www.amazon.com/A-New-Introduction-Modal-Logic/dp/0415126002

Best,

Bruno

>
> Cheers
> --
>
> ----------------------------------------------------------------------------
> Prof Russell Standish Phone 0425 253119 (mobile)
> Principal, High Performance Coders
> Visiting Professor of Mathematics hpc...@hpcoders.com.au
> University of New South Wales http://www.hpcoders.com.au
>
> Latest project: The Amoeba's Secret
> (http://www.hpcoders.com.au/AmoebasSecret.html)
> ----------------------------------------------------------------------------
>

Russell Standish

unread,
Apr 16, 2014, 8:10:51 PM4/16/14
to fo...@googlegroups.com
On Wed, Apr 16, 2014 at 09:19:49AM -0400, Gary Oberbrunner wrote:
> How cool would it be if we could write TeX and have it show up as proper
> equations in email! BTW, I use gmail's webmail in Chrome on Windows, and
> it has no problem with ¬, ◊ or ◇. (That's sideways-L not, and two
> diamond/lozenge chars).
>

There is a LaTeX editor plugin in Javascript that might be used to
implement this - but only if you like writing your emails in a web
browser (which I do not!).

Plus, you still have to deal with people using plain text email
clients - you could place the raw LaTeX in the plain text branch, and
a PNG rendering of the equation in the HTML version, I suppose.

By the way, to produce those characters above, I use the emacs "mule"
option, and select the TeX input method. Then typing \neg, \lozenge and
\diamond produces those symbols (ie inserts the UTF8 sequences for
them). I find it an excellent way of unicoding my software, and I can
continue using 8 bit characters everywhere in my application.
Reply all
Reply to author
Forward
0 new messages