# Re: AUDA and pronouns

```
On 21 Oct 2013, at 23:03, Russell Standish wrote:```
```
```
```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?
```
```
```
If p is the result of a computer program P, then "p is the result of a computer program P" is itself the result of a computer program (it can be P itself in case P is sigma_1 complete).
```No notion of correctness is involved here.

```
```

```
```
```
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.
```
```
```
The axiom 4 ([]p -> [][]p) is indeed an axiom in the classical theory of knowledge (the modal logic 4).
```
```
But, then, in arithmetic, when we define knowledge with the Theaetetus's method, it becomes a theorem (a scheme of theorems, for each arithmetical p) of arithmetic. That's why we can say that we recover the classical theory of knowledge in arithmetic.
```

```
```

```
```

```
```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?
```
```
```
Because if the proof is formal, the proof that the proof is formal is easily made itself formal, and can be checked mechanically. The case of the 4 colour theorems is not easy, because there thousand of lemma, checked by many different computers, by humans not using exactly the same software. The last thing I heard was that some lemma have been discovered not having been checked at all.
```

```
```
```
```
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?
```
```
```
What prevent []p to define a proba is only the existence of cul-de-sac worlds. For a modal axiomatization of proba we want the axiom []p -> <>p. But we don't have that in arithmetic (with [] = Gödel beweisbar).
```
But we get it with the nuance  ([]p & <>p). (or Bp & Dp, or Bp & Dt)

```
Example. I said yesterday to John Clark that P(W xor M) = 1, in Helsinki, because (W xor M) is true in the two accessible (from helsinki) realities W and M.
```
```
This makes sense only because I assume comp, that is, I assume I will survive the teletransportation, that is, I assume that Helsinki is not a cul-de-sac world.
```
```
The nuance "Bp & Dp" is only that: an implcit assumption that we are not in a cul-de-sac world. It contains a little bit of comp already.
```
```
Bp is true for all p, true and false, in the cul-de-sac world (world in Kripke sense, here, not yet in Everett sense!).
```
Bruno

```
```
--

----------------------------------------------------------------------------
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 to everything-list+unsubscr...@googlegroups.com.
```To post to this group, send email to everything-list@googlegroups.com.
```
```
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
To post to this group, send email to everything-list@googlegroups.com.