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 inmytheses, 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 couldn't follow it from your thesis.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 betweenZ_1* and Z_1. The former is your quantum logic, but the latter hastheno 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 do your think?

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/