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.

<x-tad-bigger>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)</x-tad-bigger>

http://iridia.ulb.ac.be/~marchal/