# Re: AUDA and pronouns

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

>
> >
> >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).

--

----------------------------------------------------------------------------
Prof Russell Standish                  Phone 0425 253119 (mobile)
Principal, High Performance Coders
Visiting Professor of Mathematics      hpco...@hpcoders.com.au
University of New South Wales          http://www.hpcoders.com.au
----------------------------------------------------------------------------

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