Hi Aditya,
Sorry for answering late. Computer problems did make my mailbox quite
messy, and also I'm rather busy.
The "B" is a unary connector, like the negation "~". ~p is intended for
"not p" or "p is false".
"Bp" is intended for "provable p", or more precisely "provable by some
(fixed) sound lobian machine" (and a lobian machine is just a machine
"sufficiently rich" to prove the main elementary arithmetical
propositions (including the induction axioms pages: search the Podnieks
web page for more on this:
http://www.ltn.lv/~podnieks/
Obviously "Bp -> p" is true (by definition) for a *sound* lobian
machine. The interesting and fundamental point is that "Bp -> p",
although true, cannot be *proved* by the lobian machine, making the
logic of "Bp & p" (p provable and p true) different from the logic of
Bp, and this is what I exploit to distinguish formally the first and
third person discourse in the translation of UDA in a subset of
arithmetic (as a lobian machine's natural language). And this is needed
for isolating the logic of physical (observable) propositions in the
comp frame.
Solovay has succeeded in formalizing completely the true
(propositional) logic of B by a modal logic named G* and the provable
part of by the (weaker) modal logic G. It is the difference between G
and G* which makes comp formally consistent (and then necessary bu the
Universal Dovetailer Argument (UDA)).
A variant of quantum logic appears exactly where the UDA shows it needs
to appear would the comp assumption be correct.
Hope this helps. Don't hesitate to ask questions even very basic one. I
know we can lose time for simple notation problem (but then they are
simple to answer, also!)
Regards,
Bruno
Le 14-août-05, à 00:40, Aditya Varun Chadha a écrit :
> Hi Bruno,
>
> Can you please say exactly the meanings of B and Bp? does Bp mean "B
> and p"? or B parametrized by p? without their meanings specified your
> derivation isn't obvious to me.
>
> On 8/13/05, Bruno Marchal <marchal.domain.name.hidden> wrote:
>> And thus B(Bt -> t) is true. (or, by necessitation B(Bt -> t)
>> follows).
>
> --
> Aditya Varun Chadha
> adichad AT gmail.com
> http://www.adichad.com
>
>
http://iridia.ulb.ac.be/~marchal/
Received on Sat Oct 15 2005 - 09:52:52 PDT