George Levy wrote: >Thanks Bruno.... this is much more than I bargained for... I can barely keep >afloat...I have a lot of homework to do. > >I am also very busy these days with my regular work so I don't mind going >slow.
Let us going slow. >Just a couple of questions: > >1) What is Godel's "Bew". Probably not something he drank. "Bew" is Godel's provability predicate. Bew is for "beweisbar" which means "provable" in German. Bew(x) or Bew x means x is provable. (x being a representation of a sentence in the language of a fixed theory or proving machine under discussion). What Godel did was to show that it was possible to translate Bew(x) in theories sufficiently rich to prove elementary theorem in arithmetic, or in any richer theory T. You can also think at T as a proving machine. Let us fix such a machine/theory T. Godel shows that "T proves p" can be translated in the language of the T. (The basic reason is that if T proves p there is a formal proof q of p from the axioms of T, and there is a mechanical procedure for verifying that q is a proof of p, and mechanical procedure can be represented (mirrored) in T). This is what is tedious to show precisely if T is arithmetic. It is as simple as programming in *machine language* and as boring too! I am still thinking how to do that in some friendly way ... Godel Hilbert Bernays Lob shows then that (I sum up some stories here): T proves p entails T proves Bew(p) (do you smell the Necessitation rule?) T proves Bew(p->q)->(Bew(p)->Bew(q)) (do you smell the K formula?) T proves Bew(p) -> (Bew(Bew(p))) (do you smell the "4" formula?) For any p q arithmetical propositions. So you see that if you take the modal system K4 + MP,Nec, you get a sound axiomatisation of the provability in T. A natural question is: is K4 a complete axiomatisation of T provability? The answer is no. For exemple K4 does not prove <>t -> -<>t (t = true) But the machine proves , for any p arithmetic, (con p) -> -(bew con p); (con p is - bew -p, of course). (The machine proves the Godel's second theorem as Godel convincingly argues (but it has been Hilbert and Bernays who proved that in all details). Is K4C + MP,Nec (with C = <>p -> -<>p) complete then? The answer is still no. Well, you know the answer of course: Solovay will prove that the system KL + MP,Nec is a sound and complete axiomatisation of the provable sentences on the provability by the machine. KL + MP,Nec is the system G. And Solovay gives us a little more: The system [all theorems of G] with the formula p->p + MP (but without Nec!!!) is a sound and complete axiomatisation of all the *true* sentences on the provability by machines. [all theorems of G] with the formula p->p + MP (but without Nec!!!) is G* G* proves also the true but unprovable sentences by the machine, like the machine's consistency ( <>t ). So the corona G* \ G (\ = set difference) formalises the true but unprovable (by T) provability sentences. In some sense, G* \ G captures the incompleteness realm. It is a decidable set as are G and G*. (a set is decidable if you can mechanically verify if something belongs or not in the set). Later I will give you the rigorous relationship between provability logic and the modal systems. En gros the propositional variables are interpreted by arbitrary arithmetical sentences (or any sentences in the language of the proving machine), and p is interpreted by Bew('p'), with 'p' a description of p in the language of the machine. Of course it follows that <>true will be interpreted by con(true). >I am not sure if I understand. You are saying that c and (c -> -c) -> c >are >both true but unprovable? Yes I am saying that. (I recall for the other that c is "<>true", or -false, it is the machine (self)consistency statement) > So the statements "I am" and >"I think therefore I am" is not provable? I appreciate your interpretation of "<>true" as "I am", although strictly speaking it is "I am consistent". Slezak interprets, like you, (c -> -c) by I doubt/I think. I prefer to translate I doubt by something like (c-> (-c & --c)), but in any case that remains unprovable (but true: it belongs to G* \ G). Well, you know that the cartesian doubt cannot really give a communicable proof that you exist, how convincing it can appear to you! >You say: >the GA can prove # -> c (# = any proposition). > >Interestingly the reverse > >c -> # > >means that if there is a consciousness, then the plenitude exists, I >think, or >maybe more appropriately from the relativistic point of view, if "I am" then >"the plenitude is." I'm afraid you misinterpretes #. When I say # is for any proposition, it is really *any* proposition including the false proposition. So the reverse "c -> #" is certainly false (when # is for a false proposition). >It would be interesting to see if we can derive the Anthropic principle. > >c -> W > >and the principle of sufficient reason > >W -> # > >from logic. I propose we come back to this later. But don't hope too much because I will not try to tackle quantified provability logic (and quantified modal logics) which I think would be needed for expressing Leibnizian principle or other sophisticated philosophical principle. We will see. (The miracle is that I will not need to make that move for extracting the quantum probabilities (well the particular case of probability one)). >The question is how to define W, "that specific world that >sustains the existence of c. Note that I don't really think that world will be necessary. >Take your time.... You too. Just try to range in some order the posts so that I can refer to them occasionally. I am thinking for giving you the crux of the proof in a nutshell. Have a good week-end, Bruno