# Re: Further modal logic queries

```Hi Russell,

```
Le 30-juil.-05, à 08:13, Russell Standish wrote out-of-line (but gives me the permission to answer online, which I will do to encourage others to invest a little more in the technics). But those who have never heard about G and G* can skip it ... for the moment :)
`(One day those posts will seem incredibly easy, I'm sure).`
```

```
```On Fri, Jul 29, 2005 at 06:26:56PM +0200, Bruno Marchal wrote:
```
```Dear Russell,

```
```I note that S4Grz=S4Grz* - is this not because
Cp -> p, so there is no difference between the starified and non
starified logics?
```
```
It is related to that but this is not enough. S4Grz = S4Grz* has been
proved by Goldblatt (and perhaps Boolos). The proof is in Boolos 1979
or 1993. It is not entirely obvious.

```
```
If so, then Op -> p, and so X=X* by the same argument.
```
```
```
Op -> p is true (with Op = Bp & ~B~p & p). But this does not entail X =
```X*.
```
```
I'll take your word for it for the moment - I'm impatient, you see!
```
```

```
I recall Op can be seen as an abbreviation of Bp & ~B~p & p. Where Bp can be interpreted by BEW('p') and BEW is the machine probability predicate of Godel 1931, and 'p' is a representation of machine-language proposition p (it is the so-called godel number in the case the machine "talk arithmetic"). Note that I limit my machine interview on sound machine, for which Bp -> p is true for any p, and thus ~p -> ~Bp is true also for any p, and thus p -> ~B~p is true, and thus, it is true that
```
Bp <-> Op

```
BUT, the machine cannot prove it, making B and O, different for the machine!!!!! G* proves Bp <-> Op (for any p) but G does not prove it.
```
```
Now X is the logic of what the machine can prove about that Op. And X* is the logic of what is true about that Op. Put in another way X corresponds to what G can prove about O, and X* is logic of what G* proves about O.
```
```
X is different from X* because G* proves ~B~t, but G does not prove it. So X does not even prove Ot although G* proves it. (G does not prove Bt & ~B~t & t, G* proves it). We see that the adjunct of "~B~p" is quite non trivial. It makes Ot false. Now in any classical Kripke "Multiverse" Bt is true in all words, and the failure of X to prove Ot show that the X logic, the logic of O, cannot have a Kripke semantics!. (later I will explain why this is a quite good news for the serach of the measure on the "OMs").
```

```
```
```
```My next question concerns your statement that S4Grz_1* is a quantum
logic. In your thesis, you seem to indicate that p->[]<>p is a
necessary theorem of QLs, and that this is proved for []=P applied to
V* and presumably []=O (although my modal logic ability is still
rather undeveloped), however why should it be true for []=C? This
seems implausible.
```
```
```
As I said in a footnote of SANE04 I have been wrong on that point in my
```theses, where I say that S4Grz_1 collapse into propositional calculus.
I was wrong but it is a little long to explain. I could do it online
someday (although it could look cumbersome without drawings!!)

```
```
Maybe written up as a paper?
```
```

```
A good journal has ordered me a paper and I will even be paid! The paper is finished and accepted but I am not sure I can put it right now on my web page. It is better, imo, than my preceding papers, but it is not yet the "official technical presentation of my PhD", which will still take some time. One of the reason is that I would like to get more results. I would like to optimize somehow my theorems provers
```(cf  http://iridia.ulb.ac.be/~marchal/G.html ).
```
Thanks anyway for encouraging me. And as you have seen I have still some "wording" problems, and it is hard to satisfy simultaneously the susceptibilities of the cognitive scientists, the physicists and the computer scientists. In the "scientific world" diplomats are still often "killed!"
```

```
```
```
```
```
```What is the exact derivation of p->[]<>p - I
```
```
I have prove it by using the Kripke Semantics that Visser found for V
(and V*).

```
```
I did it using a somewhat shorter version of the proof you gave in
your thesis (which I never understood BTW). It was

p
=> []p (Using p->[]p, which holds for V, V*)
=> []p v <> p = -P-p  (T v x = T)
=> []-P-p   (Using p->[]p)

Now you also say that the rule of possibilisation holds for G* (and
V*) (I don't understand this point, but am taking your word for it
here)

So

-P-p => <>-P-p
=> []-P-p ^ <>-P-p = P-P-p (or p->[]<>p, where []=P)

I also did a slight variant of this proof for []=O, and it seemed to
work, but couldn't replicate it for []=C
```
```

```
That is not too bad :). One problem though is that you are using the "p->Bp" with p substituted by ~P~p (I recall from SANE04 that Pp is for Bp & ~B~p). But p can be substituted only by atomic formula or boxed formula; if not you would be able to get ~B~t -> B~B~t, contradicting Godel's incompleteness Theorem. The next lines are correct. To understand why G* (and V*) are closed for the possibilisation (i.e. that if G* proves A then G* proves ~B~A, or G* proves DA where D is ~B~, the diamond), just remember that by Solovay's theorem, if G* proves A then A is true for the machine, and thus obviously consistent. Careful: the machine itself cannot do that reasoning, but can bet on it, but only bet on it! A proof which is much clearer than in my thesis has been given in this list here, where "p->BDp" is called LASE, for Little Abstract Schroedinger Equation:
```http://www.escribe.com/science/theory/m2855.html

```
```
```
```
```
```
I'm also still trying to get my head around the difference between
```
Z_1* and Z_1. The former is your quantum logic, but the latter has the
```no cul-de-sac conjecture proven.
```
```
Ot = Bt & Dt.     (with D ==  ~B~) D is the diamond.
V* proves it but not V (because G* prove Dt and G does not).
So Z_1* proves Ot, but Z_1 does not. OK?

```
```Any chance of an interpretation?
```
```
In which sense? (I must go now)

```
```
I'm looking for an English interpretation, like G = logic of belief (or
provability), and G* = logic of truth, G*\G = unbelievable truth

Note that the modal operator B represent mathematical belief, but that
everyday (or perhaps scientific) belief seems to be more like P. What
```
```

Roughly speaking:

```
Bp is the formal scientist (it "means" provable p in a checkable way, it could mean "paper accepted :)
```
```
Bp & p is the knower, or the correct justifier. I use Theaetetus' idea that 'knowing p' is "p is correct (true) and justified". It is the most basic (and solipsistic) definition of the first person notion. New name: THEAE_1 (from my last paper). It gives Cp.
```
```
Bp & ~B~p is the gambler. Cf my explanation to Lee Corbin: p is true in all accessible world, and we escape the cul-de-sac problem by explicitly adding the existence of an accessible world by the adjunct of ~B~p to Bp. Careful the price is formally big given that we loose the Kripke semantics, and this will entail the probable disparition of universes capable of glueing together all the machines' dreams. It corresponds to the first person plural (where populations of machine are coherently duplicated). New name: THEAE_2. It is written Pp (In SANE04).
```
```
Bp & ~B~p & p is the correct gambler, or the "feeler". It makes possible to talk with the machine about phantom limbs! New name: THEAE_3. (Op in SANE04).
```
```
Probably: everyday beliefs are some consistent or inconsistent mixture of those "primitive" machine's beliefs.
```
```
We are not a long way from the COMP-PHYSICS; which is given by the composition of three moves: SOL, which exploits the G-G* gap, THEAE_i (which exploits the Theaetetus's ideas), and COMP, which is just given by the adjunct of p->Bp to G, p atomic!, and which corresponds to the translation of comp in the language of the machine:
```
COMP-PHYS_i = SOL(THEAE_i(COMP(G)))

```
The UDA reasoning shows (in a non speculative way, I insist) that if comp is true then physics is derivable from computer science. The translation of the UDA in computer language gives the actual derivation of physics from computer science: it is what I called COMP-PHYS, and so to test comp it is enough to compare COMP-PHYS to Physics. As you see, there are some room for maneuvers due to the fact that we have 3 main Theaetetus moves). Amazingly enough the three moves gives a sort of quantum logics. But this I will explain later after some introduction to non classical logic in general and quantum logics in particular. The combinators can help here, and I have used it in my last paper.
```
Hope this helps a little bit.

Kind Regards,

Bruno

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

```