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:

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.

I was saying that ( []p & ~p) is consistent. ( []p & ~[]~p) is "p is provable and p is consistent).
Mistaken belief is consistent with arithmetic.





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.




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

PA, ZF, all Löbian machines prove []p -> [][]p. That is why they are "intrspective enough". When they prove something, they can prove that can prove that something.

Robinson Arithmetic, which has no induction axiom at all, cannot. It is still sigma_1 complete, but cannot prove its own sigma_1 completeness, nor []p -> [][]p. RA is typically NOT Löbian.

sigma_1 completeness = a provability characterization of Turing universality. Löbian machines are universal, like RA, but unlike RA, thay can prove (heir universality (in some weak sense).


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?

As I say, by showing that PA proves all instances of p -> []p, for p sigma_1. This is long and subtle to show. Boolos 1979 sums it rather well, and Boolos 193, gives all the details (but it is more messy).





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


Did you mean [](p&q) <-> []p & []q?

Yes.

That theorem at least sounds
plausable as being about proof.

OK.

[]p -> [][]p is not so astonishing, because the induction axioms provides strong provability power to the theories. Let me try to say a bit more. If PA proves p, PA will proves []p. This is much more easy to prove, and is indeed captured by the necessaitation rule p/[]p. That is almost obvious, because if PA proves p, such a proof exists, and thus has a Gödel number, and the machines will prove it (provable('p') is sigma_1, and the theories are sigma_1 complete). That is true for both RA and PA. But PA, like ZF, can internalise that rule (p/[]p), they can proof in general that []p -> [][]p. This will be proved by induction on the complexity of the formula p, and well, it is not easy at all to see that.




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.

I would not trust my intuition about this.



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.

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

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.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.

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 everything-list+unsubscr...@googlegroups.com.
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.

Reply via email to