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
