# Re: AUDA and pronouns

```Disclaimer: No idea if I am even on the same planet on which this
discussion is taking place. So pardon my questions and confusions:```
```
On Sun, Oct 20, 2013 at 11:15 PM, Russell Standish <li...@hpcoders.com.au>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.
>
>
Why Isn't "mistaken belief" here merely unsound because it's propositional
variable, assuming we're speaking generally about all systems?

>
> >
> > >
> > >Obviously, one cannot prove []p & p, for very many statements, ie
> > >
> > >[]p & p does not entail []([o]p)
>

Isn't that a rule for any modal sentence though, independent of system?
[o]p is ([]p & p)

Isn't []p & p = []([o]p) the definition of fixed point theorem? That, plus
modalization conditionals to remove p from the G sentence so that every
sentence H is a fixed point of it?

So that you get that list of instances with (G sentence on left and H on
right) examples like the following:

[]p   corresponds to  T
¬[]p corresponds to  ¬[]⊥
[]¬p corresponds to  []⊥, which is pretty cool because you get a
provability statement that is arithmetically equivalent to its own
non-provability iff the statement is equivalent to the statement that
arithmetic is inconsistent. Because G proves in this fashion:

[o](p <=> [] ¬p) <=> [o](p<=> []⊥)

This is the kind of thing that clarifies the pronoun issue imho.

> >
> > []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?
>

But it nonetheless is everywhere in Boolos: []p -> [][]p IS a theorem of G,
and useful, unless Bruno shoots the cowboy, because he cannot prove it or
find his damned Boolos book.

>
>
> > (and []p -> []p, and p -> p) + ([](p & p) <-> []p & []q) (derivable
> > in G)
> >
>
> Did you mean [](p&q) <-> []p & []q?

I'm not sure of the q and whether you can just leave out the first bit.

> That theorem at least sounds
> plausable as being about proof.
>
>
> > 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...
>

Why?

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

Not sure, I'd guess we're comparing G's reasoning 3rd person "I" with
reasoning of a fixed point corresponding to some sentence of G 1st person
"I" in a modal/qualitative provability sense. PGC

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

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