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

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

Date: Fri May 11 03:55:16 2001

George Levy wrote:

*>Thanks Bruno.... this is much more than I bargained for... I can barely keep
*

*>afloat...I have a lot of homework to do.
*

*>
*

*>I am also very busy these days with my regular work so I don't mind going
*

*>slow.
*

Let us going slow.

*>Just a couple of questions:
*

*>
*

*>1) What is Godel's "Bew". Probably not something he drank.
*

"Bew" is Godel's provability predicate. Bew is for "beweisbar" which means

"provable" in German. Bew(x) or Bew x means x is provable. (x being a

representation of a sentence in the language of a fixed theory

or proving machine under discussion).

What Godel did was to show that it was possible to translate Bew(x) in

theories

sufficiently rich to prove elementary theorem in arithmetic, or in any

richer

theory T. You can also think at T as a proving machine.

Let us fix such a machine/theory T.

Godel shows that "T proves p" can be translated in the language of the T.

(The basic reason is that if T proves p there is a formal proof q of p

from the

axioms of T, and there is a mechanical procedure for verifying that q is

a proof

of p, and mechanical procedure can be represented (mirrored) in T).

This is what is tedious to show precisely if T is arithmetic. It is as

simple as

programming in *machine language* and as boring too!

I am still thinking how to do that in some friendly way ...

Godel Hilbert Bernays Lob shows then that (I sum up some stories here):

T proves p entails T proves Bew(p) (do you smell the Necessitation

rule?)

T proves Bew(p->q)->(Bew(p)->Bew(q)) (do you smell the K formula?)

T proves Bew(p) -> (Bew(Bew(p))) (do you smell the "4" formula?)

For any p q arithmetical propositions.

So you see that if you take the modal system K4 + MP,Nec, you get a sound

axiomatisation of the provability in T.

A natural question is: is K4 a complete axiomatisation of T provability?

The answer is no.

For exemple K4 does not prove <>t -> -[]<>t (t = true)

But the machine proves , for any p arithmetic, (con p) -> -(bew con p);

(con p is - bew -p, of course).

(The machine proves the Godel's second theorem as Godel convincingly

argues

(but it has been Hilbert and Bernays who proved that in all details).

Is K4C + MP,Nec (with C = <>p -> -[]<>p) complete then?

The answer is still no.

Well, you know the answer of course: Solovay will prove that the system

KL + MP,Nec is a sound and complete axiomatisation of the provable

sentences

on the provability by

the machine. KL + MP,Nec is the system G.

And Solovay gives us a little more: The system [all theorems of G] with

the formula []p->p + MP (but without Nec!!!) is a sound and complete

axiomatisation of all the *true* sentences on the provability by machines.

[all theorems of G] with the formula []p->p + MP (but without Nec!!!) is

G*

G* proves also the true but unprovable sentences by the machine, like the

machine's consistency ( <>t ).

So the corona G* \ G (\ = set difference) formalises the true but

unprovable (by T) provability sentences.

In some sense, G* \ G captures the incompleteness realm. It is a decidable

set as are G and G*. (a set is decidable if you can mechanically verify

if something belongs or not in the set).

Later I will give you the rigorous relationship between provability logic

and the modal systems. En gros the propositional variables are interpreted

by arbitrary arithmetical sentences (or any sentences in the language of

the

proving machine), and []p is interpreted by Bew('p'), with 'p' a

description

of p in the language of the machine. Of course it follows that <>true will

be interpreted by con(true).

*>I am not sure if I understand. You are saying that c and (c -> -[]c) -> c
*

*>are
*

*>both true but unprovable?
*

Yes I am saying that. (I recall for the other that c is "<>true", or

-[]false,

it is the machine (self)consistency statement)

*> So the statements "I am" and
*

*>"I think therefore I am" is not provable?
*

I appreciate your interpretation of "<>true" as "I am", although strictly

speaking it is "I am consistent".

Slezak interprets, like you, (c -> -[]c) by I doubt/I think. I prefer to

translate I doubt by something like (c-> (-[]c & -[]-c)), but in any case

that remains unprovable (but true: it belongs to G* \ G).

Well, you know that the cartesian doubt cannot really give a communicable

proof that you exist, how convincing it can appear to you!

*>You say:
*

*>the GA can prove # -> c (# = any proposition).
*

*>
*

*>Interestingly the reverse
*

*>
*

*>c -> #
*

*>
*

*>means that if there is a consciousness, then the plenitude exists, I
*

*>think, or
*

*>maybe more appropriately from the relativistic point of view, if "I am" then
*

*>"the plenitude is."
*

I'm afraid you misinterpretes #.

When I say # is for any proposition, it is really *any* proposition

including the false proposition. So the reverse "c -> #" is certainly

false (when # is for a false proposition).

*>It would be interesting to see if we can derive the Anthropic principle.
*

*>
*

*>c -> W
*

*>
*

*>and the principle of sufficient reason
*

*>
*

*>W -> #
*

*>
*

*>from logic.
*

I propose we come back to this later. But don't hope too much because I

will not try to tackle quantified provability logic (and quantified modal

logics) which I think would be needed for expressing Leibnizian principle

or other sophisticated philosophical principle. We will see.

(The miracle is that I will not need to make that move for extracting the

quantum probabilities (well the particular case of probability one)).

*>The question is how to define W, "that specific world that
*

*>sustains the existence of c.
*

Note that I don't really think that world will be necessary.

*>Take your time....
*

You too. Just try to range in some order the posts so that I can refer

to them occasionally.

I am thinking for giving you the crux of the proof in a nutshell.

Have a good week-end,

Bruno

Received on Fri May 11 2001 - 03:55:16 PDT

Date: Fri May 11 03:55:16 2001

George Levy wrote:

Let us going slow.

"Bew" is Godel's provability predicate. Bew is for "beweisbar" which means

"provable" in German. Bew(x) or Bew x means x is provable. (x being a

representation of a sentence in the language of a fixed theory

or proving machine under discussion).

What Godel did was to show that it was possible to translate Bew(x) in

theories

sufficiently rich to prove elementary theorem in arithmetic, or in any

richer

theory T. You can also think at T as a proving machine.

Let us fix such a machine/theory T.

Godel shows that "T proves p" can be translated in the language of the T.

(The basic reason is that if T proves p there is a formal proof q of p

from the

axioms of T, and there is a mechanical procedure for verifying that q is

a proof

of p, and mechanical procedure can be represented (mirrored) in T).

This is what is tedious to show precisely if T is arithmetic. It is as

simple as

programming in *machine language* and as boring too!

I am still thinking how to do that in some friendly way ...

Godel Hilbert Bernays Lob shows then that (I sum up some stories here):

T proves p entails T proves Bew(p) (do you smell the Necessitation

rule?)

T proves Bew(p->q)->(Bew(p)->Bew(q)) (do you smell the K formula?)

T proves Bew(p) -> (Bew(Bew(p))) (do you smell the "4" formula?)

For any p q arithmetical propositions.

So you see that if you take the modal system K4 + MP,Nec, you get a sound

axiomatisation of the provability in T.

A natural question is: is K4 a complete axiomatisation of T provability?

The answer is no.

For exemple K4 does not prove <>t -> -[]<>t (t = true)

But the machine proves , for any p arithmetic, (con p) -> -(bew con p);

(con p is - bew -p, of course).

(The machine proves the Godel's second theorem as Godel convincingly

argues

(but it has been Hilbert and Bernays who proved that in all details).

Is K4C + MP,Nec (with C = <>p -> -[]<>p) complete then?

The answer is still no.

Well, you know the answer of course: Solovay will prove that the system

KL + MP,Nec is a sound and complete axiomatisation of the provable

sentences

on the provability by

the machine. KL + MP,Nec is the system G.

And Solovay gives us a little more: The system [all theorems of G] with

the formula []p->p + MP (but without Nec!!!) is a sound and complete

axiomatisation of all the *true* sentences on the provability by machines.

[all theorems of G] with the formula []p->p + MP (but without Nec!!!) is

G*

G* proves also the true but unprovable sentences by the machine, like the

machine's consistency ( <>t ).

So the corona G* \ G (\ = set difference) formalises the true but

unprovable (by T) provability sentences.

In some sense, G* \ G captures the incompleteness realm. It is a decidable

set as are G and G*. (a set is decidable if you can mechanically verify

if something belongs or not in the set).

Later I will give you the rigorous relationship between provability logic

and the modal systems. En gros the propositional variables are interpreted

by arbitrary arithmetical sentences (or any sentences in the language of

the

proving machine), and []p is interpreted by Bew('p'), with 'p' a

description

of p in the language of the machine. Of course it follows that <>true will

be interpreted by con(true).

Yes I am saying that. (I recall for the other that c is "<>true", or

-[]false,

it is the machine (self)consistency statement)

I appreciate your interpretation of "<>true" as "I am", although strictly

speaking it is "I am consistent".

Slezak interprets, like you, (c -> -[]c) by I doubt/I think. I prefer to

translate I doubt by something like (c-> (-[]c & -[]-c)), but in any case

that remains unprovable (but true: it belongs to G* \ G).

Well, you know that the cartesian doubt cannot really give a communicable

proof that you exist, how convincing it can appear to you!

I'm afraid you misinterpretes #.

When I say # is for any proposition, it is really *any* proposition

including the false proposition. So the reverse "c -> #" is certainly

false (when # is for a false proposition).

I propose we come back to this later. But don't hope too much because I

will not try to tackle quantified provability logic (and quantified modal

logics) which I think would be needed for expressing Leibnizian principle

or other sophisticated philosophical principle. We will see.

(The miracle is that I will not need to make that move for extracting the

quantum probabilities (well the particular case of probability one)).

Note that I don't really think that world will be necessary.

You too. Just try to range in some order the posts so that I can refer

to them occasionally.

I am thinking for giving you the crux of the proof in a nutshell.

Have a good week-end,

Bruno

Received on Fri May 11 2001 - 03:55:16 PDT

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