On 29 May 2013, at 22:46, meekerdb wrote:

On 5/29/2013 9:52 AM, Bruno Marchal wrote:On 29 May 2013, at 18:37, Bruno Marchal wrote:On 29 May 2013, at 17:47, Quentin Anciaux wrote:http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#Construction_of_a_statement_about_.22provability.22 2013/5/29 John Clark <johnkcl...@gmail.com>On Wed, May 29, 2013 at 2:37 AM, Bruno Marchal<marc...@ulb.ac.be> wrote:>> If you want to communicate why should I need to search atall? And if even Google doesn't know what the hell Bp&p is thenit's ridiculous to expect your readers to know what you'retalking about.> Come on, John. Search for "true opinion". Bp & p is a formulausing some notation for this,So when I read your post and you said "Bp & p" I should have saidto myself "obviously if I Google "true opinion" it will tell mewhat Bp & p means. Well, that is not obvious to me at all but itdoesn't matter because I just Googled "true opinion" and I stillcan't find a damn thing about Bp & p.Bp = I believe in p, or 'my opinion is that it is the case thatp', or, in the context of ideally correct (and simple machine):Beweisbar('p').p, when produced by some system, means, in all books on logic,that p is true (from the system pov).So Bp & p is a ay to model true opinion, in some system.When I write I always ask myself if anybody will understand whatI say, I may not always be successful in making myself clear butat least I try. You're not even trying.I have explained this more than one times on this list, todifferent people, because once you get it you can't forget.You have come perhaps too much recently, but you can always askquestion. You should not focus on the formula, but on what itrepresents. It is also explained in sane04, and basically, in allmy papers on this subject. Probably with different notations.Or perhaps you just agree with what Niels Bohr said "I refuse tospeak more clearly than I think".Bp is for "I believe p", produced by some machinery (machine,formal system, ...).In particular, it is an expression in some modal logic. 'Belief'obeys usually the axioms:1. B(p->q) -> B(p -> Bq) 2. Bp -> BBpBp & p means "(I believe in p) and p". P alone, in the assertativemode of some entity means "it is the case that p". (independentlyof the veracity of p).For knowledge, we use the axiom: 3. Bp -> pAs Gödel saw in 1933, beweisbar, or provability, does not obey tothat third axiom, and so provability cannot modelknowledgeability. Indeed no consistent machine can prove B('0=1') -> 0=1, which is equivalent with ~B('0=1'), which is self-consistency.I'm not sure I understand this. Are you saying we cannot take "(Bp->p) for all p" as an axiom because it would entail Bf ->f and then~f->~Bf, and since ~f is true by definition it would entail that themachine is consistent?

Yes.

`More generally p -> f is equivalent with ~p, as you can verify by`

`doing the truth table:`

p -> f 1 0 0 0 1 0

`That's why Löb's theorem B(Bp -> p) -> Bp generalizes Gödel's second`

`incompleteness theorem: just replace p by f. B(~Bf) -> Bf, ~Bf ->`

`~B(~Bf), Dt -> ~BDt.`

Bruno 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?hl=en. For more options, visit https://groups.google.com/groups/opt_out.