- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Bruno Marchal <marchal.domain.name.hidden>

Date: Tue, 7 Jun 2005 09:55:54 +0200

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

Date: Tue, 7 Jun 2005 09:55:54 +0200

Le 07-juin-05, à 00:31, Brent Meeker a écrit :

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

*
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:10 PST
*