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

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

Date: Fri, 16 Aug 2002 17:07:42 +0200

At 10:11 -0700 14/08/2002, Wei Dai wrote:

*>Let me generalize my question then. Is it true that for any modal logic
*

*>that has a semantics, any sentence in that logic has a corresponding
*

*>sentence in non-modal quantificational logic with the same meaning?
*

It depends of the semantics. It depends of the order of quantification.

It depends what you want to do.

At 10:11 -0700 14/08/2002, Wei Dai wrote:

*>Before the invention of possible world semantics, people had to reason
*

*>about modalities on a purely syntactical basis. Are there still modal
*

*>logics for which no semantics is known?
*

There are the modal logics of your servitor :-)

Z, Z1, Z*, Z1* and X, X1, X*, X1*

Those are well-defined modal logics. It is easy to prove them even

decidable. I have partial soundness theorem for Z and Z1. No

completeness! None of those logics have not even been axiomatized.

(Open problems!).

Remember the high constraint due to the fact that I "interview"

sounds universal machines. The "mother box" corresponds to the

Goedelian "beweisbar" predicate. If we interpret the propositional

letters p, q, r ... by arithmetical sentences, and "[]p" is interpreted by

beweisbar(godel-number-of(p)) then a natural question, which curiously did

not appear in Godel 1933, is: which modal logic, if any, does the beweisbar

box obey?

Thanks to the work of Lob, Magari, Boolos, Solovay and others we know

such a logic exists and it is G. Here is a presentation of G:

AXIOMS: [](p -> q) -> ([]p -> []q)

[]([]p -> p) -> []p

[]p -> [][]p (this one can been shown redundant)

RULES: p p->q p

--------, ---

q []p

A class of Kripke frames (there exists others!) is set of finite,

irreflexive, transitive frames.

Actually G gives the part of that logic which remains provable by the

machine itself. Solovay showed much more: the following *non normal*

(indeed: NON necessetation rules) logic gives the whole propositional

logic, including what is true but such that the machine cannot prove:

AXIOMS: <All theorems of G>

[]p -> p

RULES: p p->q

--------

q

In particular G* minus G gives the set of all 0-order modal propositions

corresponding to true unprovable (by the sound machines), but bettable

self-referential sentences.

G* has no Kripke semantics, but it can be shown G* has some "natural"

semantics in term of sequences of Kripke models.

All the logics defined in my work are defined syntactically *from* G and G*,

so that it is non trivial at all to find semantics. Roughly speaking

the "knower" is defined by ([]p & p), the observer/bet-ter by []p & <>p,

the "observer/better-embedded-in-UD*-with-comp-true" is []p & <>p with p

interpretation restricted on "\Sigma_1" sentences (if they are true there

are provable). The sensible observer = []p & <>p & p , with p \Sigma_1)

At 10:11 -0700 14/08/2002, Wei Dai wrote:

*>We know that in general syntactical formulas and rules are not powerful
*

*>enough to always let us reason without meaning, because the set of
*

*>mathematical truths that are derivable syntactically from a fixed set of
*

*>axioms is just a subset of all mathematical truths.
*

Yes but self-transforming "theories" or "machine/brains" can learn

to makes bets and change themselves. That never gives the "whole" truth,

a priori, but can help a machine to progress or just survive.

At 10:11 -0700 14/08/2002, Wei Dai wrote:

*>The rest can only be
*

*>obtained by considering the semantic consequences of the axioms. I think
*

*>the point of syntax is just to give us a way to obtain at least some of
*

*>the truths through syntactical manipulation - a way to grab the
*

*>low-hanging fruit.
*

Yes. And it is a point of the brain/body too.

Bruno

Received on Fri Aug 16 2002 - 08:14:22 PDT

Date: Fri, 16 Aug 2002 17:07:42 +0200

At 10:11 -0700 14/08/2002, Wei Dai wrote:

It depends of the semantics. It depends of the order of quantification.

It depends what you want to do.

At 10:11 -0700 14/08/2002, Wei Dai wrote:

There are the modal logics of your servitor :-)

Z, Z1, Z*, Z1* and X, X1, X*, X1*

Those are well-defined modal logics. It is easy to prove them even

decidable. I have partial soundness theorem for Z and Z1. No

completeness! None of those logics have not even been axiomatized.

(Open problems!).

Remember the high constraint due to the fact that I "interview"

sounds universal machines. The "mother box" corresponds to the

Goedelian "beweisbar" predicate. If we interpret the propositional

letters p, q, r ... by arithmetical sentences, and "[]p" is interpreted by

beweisbar(godel-number-of(p)) then a natural question, which curiously did

not appear in Godel 1933, is: which modal logic, if any, does the beweisbar

box obey?

Thanks to the work of Lob, Magari, Boolos, Solovay and others we know

such a logic exists and it is G. Here is a presentation of G:

AXIOMS: [](p -> q) -> ([]p -> []q)

[]([]p -> p) -> []p

[]p -> [][]p (this one can been shown redundant)

RULES: p p->q p

--------, ---

q []p

A class of Kripke frames (there exists others!) is set of finite,

irreflexive, transitive frames.

Actually G gives the part of that logic which remains provable by the

machine itself. Solovay showed much more: the following *non normal*

(indeed: NON necessetation rules) logic gives the whole propositional

logic, including what is true but such that the machine cannot prove:

AXIOMS: <All theorems of G>

[]p -> p

RULES: p p->q

--------

q

In particular G* minus G gives the set of all 0-order modal propositions

corresponding to true unprovable (by the sound machines), but bettable

self-referential sentences.

G* has no Kripke semantics, but it can be shown G* has some "natural"

semantics in term of sequences of Kripke models.

All the logics defined in my work are defined syntactically *from* G and G*,

so that it is non trivial at all to find semantics. Roughly speaking

the "knower" is defined by ([]p & p), the observer/bet-ter by []p & <>p,

the "observer/better-embedded-in-UD*-with-comp-true" is []p & <>p with p

interpretation restricted on "\Sigma_1" sentences (if they are true there

are provable). The sensible observer = []p & <>p & p , with p \Sigma_1)

At 10:11 -0700 14/08/2002, Wei Dai wrote:

Yes but self-transforming "theories" or "machine/brains" can learn

to makes bets and change themselves. That never gives the "whole" truth,

a priori, but can help a machine to progress or just survive.

At 10:11 -0700 14/08/2002, Wei Dai wrote:

Yes. And it is a point of the brain/body too.

Bruno

Received on Fri Aug 16 2002 - 08:14:22 PDT

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