# Re: AUDA and pronouns

```On 10/20/2013 2:15 PM, Russell Standish wrote:
```
```On Sun, Oct 20, 2013 at 06:22:15PM +0200, Bruno Marchal wrote:
```
`On 20 Oct 2013, at 12:01, Russell Standish wrote:`
```
```
```On Sun, Oct 20, 2013 at 08:52:41AM +0200, Bruno Marchal wrote:
```
```We have always that [o]p -> [o][o]p  (like we have also always that
[]p -> [][]p)

```
```
There may be things we can prove, but about which we are in fact
mistaken, ie
[]p & -p
```
```That is consistent. (Shit happens, we became unsound).

```
```Consistency is []p & ~[]~p. I was saying []p & ~p, ie mistaken belief.
```
```
ISTM that Bruno equivocates and [] sometimes means "believes" and sometimes
"provable".

Brent

```
```

```
```Obviously, one cannot prove []p & p, for very many statements, ie

[]p & p does not entail []([o]p)
```
```[]p -> [][]p  OK?

```
```Why? This is not obvious. It translates as being able to prove that
you can prove stuff when you can prove it.

If this were a theorem of G, then it suggests G does not capture
the nature of proof.

Oh, I see that you are just restating axiom "4". But how can you prove
that you've proven something? How does Boolos justify that?

```
```(and []p -> []p, and p -> p) + ([](p & p) <-> []p & []q) (derivable
in G)

```
```Did you mean [](p&q) <-> []p & []q? That theorem at least sounds

```
```so    []p & p -> [][]p & ([]p & p)
-> []([]p & p) & ([]p & p),

thus ([]p & p) ->  [][o]p    (& [o]p : thus [o]p -> [o][o]p)

```
```Therefore, it cannot be that [o]p -> [o]([o]p) ???

Something must be wrong...

```
```I hope I am not too short above, (and that there is not to much typo!)

Bruno

```
```And thus you've proven that for everything you know, you can know that
you know it. This seems wrong, as the 4 colour theorem indicates. We
can prove the 4 colour theorem by means of a computer program, and it
may indeed be correct, so that we Theatetically know the 4 colour
theorem is true, but we cannot prove the proof is correct (at least at
this stage, proving program correctness is practically impossible).

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