Le 07-juin-05, à 00:31, Brent Meeker a écrit :
>> BM:
>> For knowability I take the S4 axioms and rules:
>>
>> 1) axioms:
>>
>> <all classical tautologies>
>>
>> BX -> X
>> BX -> BBX
>> B(X->Y) -> (BX -> BY)
>>
>> 2) Rule:
>>
>> X X -> Y X
>> ----------- ----- (Modus ponens, necessitation)
>> Y BX
>>
>> But in the interview of the Lobian machine I recover the S4 axioms +
>> Grz, from
>> defining "knowing X" by "proving X formally and X true" (I apply the
>> Theaetetus on
>> formal provability).
>>
>> I cannot use Gettier's given that I have no notion of causality to
>> start with. (Recall
>> I don't have any physical notion to start with).
>>
>> Bruno
>
> In that case, how does "true" differ from "provable"? If it is simply
> a formal
> system, with no facts which can make a proposition true by reference,
> then it
> seems that there is no separate notion of "true" apart from "provable".
I know you are honest, so I knew you would ask, and I am very glad
because you are putting your finger on the most utterly important
(admittedly subtle) point which gives sense to the interview of the
lobian machine, and which is really no less than Godel incompleteness
theorem (or better LOB's theorem, see below).
If B represents provability in sound (correct) formal system it is just
plainly true that
BX -> X
In particular if F represents a falsity (your favorite contradiction, P
& NOT P, for instance), then it is again plainly true that
BF -> F
BUT "BF -> F" is equivalent with NOT BF (P -> F has the same truth
table as NOT P).
So BF -> F is NOT BF, and this is a consistency statement: the false is
not provable.
So, given that we are talking about a sound formal system, we know that
BF->F is true, but as a consistency statement, we know also, by Godel's
second incompleteness theorem, that the system cannot prove its own
consistency: BF->F is true but not provable!!!!!!!!
Put in another way BF->F is true, but B(BF->F) is false. In particular
you see that B cannot behave like a knowledge modal operator!!!! In
particular again BF & F is truly equivalent to BF, but the machine
cannot prove that equivalence.
And so what logic does B obeys to?
Given the apparition of a gap between truth and provability we get two
logics, one for what the machine is able to prove about its own B, and
one for what is true about that B.
The first is G, and the second is G*. Note that the machine is sound,
which means all what the machine proves is correct, so that G is
included in G*. But G* is much larger than G. For example G* proves
that the machine is consistent -BF. G* proves that the machine cannot
prove its own consistency -B(-BF). G* prove that BP <-> (BP & P), but
the machine cannot prove it.
So it makes sense to define "knowledge", for the machine, by a new
modal operator Cp (say) defined by Cp = Bp & p. (Theaetetus) It can be
shown that it obeys the S4 axioms, and one more which is the grz
formula (the Grzegorczyk formula) which is rather ugly, it is:
B(B(p -> Bp) -> p)-> p
Perhaps ugly, but it should make Stephen happy, because it introduces
an irreversible temporality in the possible evolution of the machine
knowledge. To show this we should need the Kripke semantics stuff.
But my main point here is that by Godel incompleteness Bp -> p although
always true, is not always provable. LOB theorem says exactly when
Bp->p is provable, it is provable only when p is provable! The machine
M is closed for the rule:
if M proves Bp -> p then M proves p.
M can prove it! M proves B(Bp -> p) -> Bp
And Solovay will prove that this Lob's formula is enough, along with
B(p->q)->(Bp->Bq) to derive the whole discourse of the machine with the
modus ponens and the necessitation rule. (that's G). G* has as axioms
all the theorems of G, + Bp -> p, and is closed for the modus ponens
rule BUT NOT FOR THE NECESSITATION rule!!!!
Exercise 1: show that G* would be inconsistent if you add the
necessitation rule.
Exercise 2: what was precisely wrong in your comment?
Bruno
appendice:
Taken from my post:
http://www.escribe.com/science/theory/m2855.html
with [] = B here.
I recall that a formal presentation of G is:
AXIOMS [](p -> q) -> ([]p -> []q) K
[]([]p -> p) -> []p L
RULES p p -> q p
-------- Modus Ponens --- Necessitation
q []p
and G* is
AXIOMS Any theorem of G
[]p -> p
RULES p p -> q
-------- Modus Ponens(only! No Necessitation rule!!!)
q
(Plus some "obvious but tedious" substitution rules)
http://iridia.ulb.ac.be/~marchal/
Received on Tue Jun 07 2005 - 04:04:04 PDT