Hi, I'm sorry. I realise I made an omission error in the post I send the Wed, 17 Nov 1999 at 06:24:30:
http://www.escribe.com/science/theory/m1417.html (the post I refer to George yesterday (8 may 2001) for getting an acquaintance with G and G*). Perhaps you have seen it. The omission error is in the definition of G* (i'm very sorry!) I said: G* has as axioms all theorems of G, and, as ONLY rule of inference, the modus ponens. Well, if that was the definition of G*, G* would be included in G! (actually G* would be equal to G in the sense of having the same theorems). It is, (as I have said in other posts): G* has as axioms all theorems of G, all wff []A->A, and has, as ONLY rule of inference, the modus ponens. For exemple G* proves []false -> false, that is G* proves <>true, that is G* proves the consistency of the sound machine which we are interviewing. Of course the sound machine itself is mute on that question. The machine (and the guardian) both can justify that silence, both G and G* proves <>true -> -[]<>true ("Godel's second incompleteness theorem"). Note that G* is not closed for the necessation rule (of inference), and cannot be! If you add the necessitation rule to G*, it is easy to see that G* becomes inconsistent. Indeed G* proves <>true, so we the necessitation rule you have that G* proves []<>true. But G* proves <>true -> -[]<>true, and also <>true, so by the modus ponens rule, G* proves []<>true. So G* proves []<>true & -[]<>true. But G* proves all ((A & -A) -> false) by classical propositional calculus, so G* proves (([]<>true & -[]<>true) -> false) and by modus ponens again G* proves false. You could find a shorter proof using only Loeb 's formula L instead of Goedel's second theorem). Recall L is ([]([]A->A)) -> []A Bruno