# Re: Another shot at how spacetime emerges from computational reality

```
On 31 Dec 2013, at 22:39, meekerdb wrote:```
```
```
```On 12/31/2013 2:41 AM, Bruno Marchal wrote:
```
To be sure, the material hypostases are not transitive, so when we observe, we don't observe that we observe, but when we feel or know, it is the case that we feel feeling and we know that we know (although not as such).
```
Here I use comp + Theaetetus.
```
```
```
But then to "know that we know" requires only that we know that we have a belief and that it's true:
```
B(Bp+p)+(Bp+p) = B(Bp)+Bp+p

```
that seems like an easy path to knowledge, since I suppose that Bp- >B(Bp).
```
```
We do have Bp -> BBp (as BP itself is sigma_1, and LĂ¶ban machine proves p -> Bp for all sigm_1 proposition).
```

```
```In this system isn't it the case that

((p+q)->s)->((Bp+Bq)->Bs)
```
```
(p+q) -> s
thus by necessitation
B((p+q) -> s)
```
B((p+q) -> s) -> (B(p+q) -> Bs) instance of the axiom K : B(a-> b) - > (Ba -> Bb)
```B(p+q) <-> Bp + Bq    (normal modal logic)
B((p+q) -> s) -> ((Bp+Bq) -> Bs) substitution preceding line
((Bp+Bq) -> Bs)  (modus ponens)

So it looks we can derive your:((p+q)->s)->((Bp+Bq)->Bs)

```
But alas we have just use the deduction rule, which is not valid in the modal context when we use the necessitation rule. If not we could derive p -> Bp from the necessitation rule, and this is incorrect. "p -> Bp" is usually wrong. This is easy to show by using Kripke semantics. Just take a world alpha with p true, accessing a world beta with p false. In alpha, p -> Bp is false.
```
```
```
Yet the rhs doesn't generally hold.
```
```
```
It does not. You confuse the necessitation rule (we can derive Bp from p), and the so called "trivial" formula: p->Bp.
```
In G we have neither Bp -> p, nor p -> Bp.
```
We do have have p -> Bp in G1 (the "G" we obtained when we limit the arithmetical interpretation of the variable atomic sentence (p, q, ...) on the sigma_1 sentence.
```
Bruno

```
```
Brent

--
```
You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com.
```To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.
```
```
http://iridia.ulb.ac.be/~marchal/

--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email