# Re: AUDA and pronouns

```On Mon, Oct 21, 2013 at 03:52:14PM +0200, Bruno Marchal wrote:
>
> On 20 Oct 2013, at 23:15, 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:
> >>
> >>>
> >>>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.
>
> You are right, this is not so easy to prove. It follows from the
> "provable sigma_1 completeness", that is the fact that if p is a
> sigma_1 formula, then Peano Arithmetic can prove p -> Bp. (That is
> not easy to prove, but it is done in Hilbert-Bernays, also in the
> books by Boolos). It is the hard part of the second incompleteness
> theorem. It presupposes some induction axioms, like in Peano
> Arithmetic (PA).
> Then Bp is itself a sigma_1 arithmetical proposition, so []p -> [][]p.
> ```
```
i.e If p is the result of a computer program, then there exists a
program that proves p is correct?

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

In choosing axioms, intuition is all we have to go by. But you say
below that 4 is in fact a redundant axiom ... which makes it not so
clear cut.

>
>
> >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).
>
> It should be easy once we have a concrete formal proof. As far as I
> know, we don't have this for the 4 colour theorem. But once we have
> such proofs, it should be trivial to prove that the proof exists,
> making []p -> [][]p easy to prove for the particular case of p = 4-color.

How does it make it easy?

>
> A correct machine is automatically LĂ¶bian if she is sigma_1
> complete, and has enough induction axioms to prove its own sigma_1
> completeness (in the sense of proving all formula p -> []p, for p
> sigma_1).
>
> In fact "p-> []p" characterizes sigma_1 completeness (by a result by
> Albert Visser), and that is why to get the proba on the UD*, we use
> the intensional nuance []p & <>t  (= proba) starting from G extended
> with the axiom "p-> []p" (limiting the proposition to the UD).
>

proba?

--

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