# Re: Rép : Modal Logic

```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

```
```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 <[EMAIL PROTECTED]> wrote:
```
```And thus B(Bt -> t) is true.   (or, by necessitation B(Bt -> t)
follows).
```
```
--
```http://iridia.ulb.ac.be/~marchal/