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
>>> 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 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
> 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/
Received on Tue Aug 02 2005 - 07:00:16 PDT