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

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

Date: Wed, 14 Aug 2002 16:38:45 +0200

Wei Dai wrote:

*>Thanks for your answers. They are very helpful.
*

Y're welcome. I want just add something.

Your general question was "Why using modal logic when

quantifying on worlds is enough". My basic answer was

that Kripke's possible world semantics works only on a

subset of the possible modal logics.

You can do modal logics without semantics. In fact modal

logic appeared because of apparent existence of modalities.

The main one is "possible" and "necessary". But others

occurred like "permitted" and "obligatory"; "provable" and

consistent", "believable" and "imaginable", etc.

The fundamental motivation of a logician is to give purely

syntactical formula and rules for manipulating formula so that

we can reason and communicating reasoning *without* any

meaning. The traditional joke is that a logician does not

want understand what he talk about!

When you do that you fall automatically on the following sort

of problem:

Take a formal theory like S4, again:

(I suppose a language with the usual logical symbol

including the propositional constant f and t, + the [])

AXIOMS: <axioms of classical propositional logic>

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

[]p -> p

[]p -> [][]p

RULES: p p->q p

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

q []p

This gives at once an infinity of formula: those derivable

from the axioms by using finitely many times the rules.

I recall that -p is an abbreviation for (p->f), and <>p is

an abbreviation for -[]-p.

The question is: is the formula []p -> <>[]p derivable in S4?

Now that question is not so hard and you can solve it *syntactically*.

Just find a pathway from the axioms to the formula by using the

rules of inference. (That is: just prove []p -> <>[]p in S4).

But I can say this because I know the solution!

Now logician want not only prove theorems in their system, they

want also know if the system is consistent, that is, if the system

does not prove f, and question like that.

For example, and this is a *very* difficult exercise, try to prove

that S4 does *not* prove the formula p -> <>[]p.

Before the rise of semantics such question was almost not answerable

in general. You cannot solve them by searching all the proofs

because you have an infinity of proofs.

Something like Kripke semantics makes such an exercise very easy,

once you have soundness and completeness metatheorem relating your

logic (here S4) with the semantics.

Now it not very difficult to prove such completeness and soundness

theorem for system as simple as S4 (see also ref in the archive

below). I give you only the two main metatheorems we can use here.

I recall that a Kripke frame is just a set (of "worlds") with some

binary relation among them (the accessibility relation).

A model is a frame with, for each world w, a function from L in {0,1}.

L = our set of propositional letters {p, q, r, ...}.

(That is: a model assigns truth to the proposition in each world).

I recall also that classical logic is verify in each world, that is:

if p is true in world w and q is true in world w, then "p->q" is

true in world w, etc. Now the S4/Kripke-semantics soundness

and completeness (S&C) metatheorem is:

S&C theorem: S4 proves A if and only if A is true in any

world of any model based on a reflexive and transitive frame.

Now, if "p -> []<>p" was derivable in S4 it would follow from

the S&C metatheorem that "p -> []<>p" would be true in any world

of any model based on a reflexive and transitive frame.

So, to prove that "p -> []<>p" is not a theorem of S4 it is

enough to find a model based on a reflexive and transitive frame

in which "p -> []<>p" is false in some world.

Let us build that counterexample. For having "p -> []<>p" false

in a world w1, by classical logic, you need a world with "p" true

in it, and "[]<>p" false in it, i.e. "-[]<>p" true in it.

But "-[]<>p" is equivalent with "<>[]-p", so it is enough to join

a unique world w2 with "-p" true in it.

Our counterexample is:

The frame = {w1, w2}

The accessibility relation R is given by w1Rw1, w2Rw2, w1Rw2

(if you prefer: R = {(w1 w1) (w2 w2) (w1 w2)}

The model is given by making p true in w1, and false in w2.

R being reflexive and transitive, and "p -> []<>p" being false at

w1, "p -> []<>p" has been shown not derivable in S4.

Another use of Kripke C&S result is to show that S4, for example,

is decidable (and then write a theorem prover for S4). This is easy

if you succeed in refining the completeness part of the C&S theorem

above with "finite frame" instead of any frame. In that case

you know that if a counterexample exist you can find it.

But Kripke semantics is useless with a "non normal"

logic, for example a modal logic without the necessitation rule.

Chellas excellent book has a chapter on Scott-Montague semantics

(also known as "minimal model") which can be used in the same

way for weaker modal logic. The Scott-Montague semantics gives

"topological" or "quasi-topological" structure on the set of worlds.

In Kripke []p is true at world w if p is true at all worlds x such

that wRx. In Scott-Montague semantics []p is true at w if the set

of worlds in which p is true belongs to the neighborhoods of w.

Just to give you an idea of another semantics for modal logic.

Bruno

PS I recall my conversation on modal logic with George Levy in

this list. For example:

Modalities and Aristotle Square

http://www.escribe.com/science/theory/m2643.html

Leibtniz Semantics

http://www.escribe.com/science/theory/m2689.html

Kripke Semantics

http://www.escribe.com/science/theory/m2689.html

Received on Wed Aug 14 2002 - 07:46:15 PDT

Date: Wed, 14 Aug 2002 16:38:45 +0200

Wei Dai wrote:

Y're welcome. I want just add something.

Your general question was "Why using modal logic when

quantifying on worlds is enough". My basic answer was

that Kripke's possible world semantics works only on a

subset of the possible modal logics.

You can do modal logics without semantics. In fact modal

logic appeared because of apparent existence of modalities.

The main one is "possible" and "necessary". But others

occurred like "permitted" and "obligatory"; "provable" and

consistent", "believable" and "imaginable", etc.

The fundamental motivation of a logician is to give purely

syntactical formula and rules for manipulating formula so that

we can reason and communicating reasoning *without* any

meaning. The traditional joke is that a logician does not

want understand what he talk about!

When you do that you fall automatically on the following sort

of problem:

Take a formal theory like S4, again:

(I suppose a language with the usual logical symbol

including the propositional constant f and t, + the [])

AXIOMS: <axioms of classical propositional logic>

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

[]p -> p

[]p -> [][]p

RULES: p p->q p

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

q []p

This gives at once an infinity of formula: those derivable

from the axioms by using finitely many times the rules.

I recall that -p is an abbreviation for (p->f), and <>p is

an abbreviation for -[]-p.

The question is: is the formula []p -> <>[]p derivable in S4?

Now that question is not so hard and you can solve it *syntactically*.

Just find a pathway from the axioms to the formula by using the

rules of inference. (That is: just prove []p -> <>[]p in S4).

But I can say this because I know the solution!

Now logician want not only prove theorems in their system, they

want also know if the system is consistent, that is, if the system

does not prove f, and question like that.

For example, and this is a *very* difficult exercise, try to prove

that S4 does *not* prove the formula p -> <>[]p.

Before the rise of semantics such question was almost not answerable

in general. You cannot solve them by searching all the proofs

because you have an infinity of proofs.

Something like Kripke semantics makes such an exercise very easy,

once you have soundness and completeness metatheorem relating your

logic (here S4) with the semantics.

Now it not very difficult to prove such completeness and soundness

theorem for system as simple as S4 (see also ref in the archive

below). I give you only the two main metatheorems we can use here.

I recall that a Kripke frame is just a set (of "worlds") with some

binary relation among them (the accessibility relation).

A model is a frame with, for each world w, a function from L in {0,1}.

L = our set of propositional letters {p, q, r, ...}.

(That is: a model assigns truth to the proposition in each world).

I recall also that classical logic is verify in each world, that is:

if p is true in world w and q is true in world w, then "p->q" is

true in world w, etc. Now the S4/Kripke-semantics soundness

and completeness (S&C) metatheorem is:

S&C theorem: S4 proves A if and only if A is true in any

world of any model based on a reflexive and transitive frame.

Now, if "p -> []<>p" was derivable in S4 it would follow from

the S&C metatheorem that "p -> []<>p" would be true in any world

of any model based on a reflexive and transitive frame.

So, to prove that "p -> []<>p" is not a theorem of S4 it is

enough to find a model based on a reflexive and transitive frame

in which "p -> []<>p" is false in some world.

Let us build that counterexample. For having "p -> []<>p" false

in a world w1, by classical logic, you need a world with "p" true

in it, and "[]<>p" false in it, i.e. "-[]<>p" true in it.

But "-[]<>p" is equivalent with "<>[]-p", so it is enough to join

a unique world w2 with "-p" true in it.

Our counterexample is:

The frame = {w1, w2}

The accessibility relation R is given by w1Rw1, w2Rw2, w1Rw2

(if you prefer: R = {(w1 w1) (w2 w2) (w1 w2)}

The model is given by making p true in w1, and false in w2.

R being reflexive and transitive, and "p -> []<>p" being false at

w1, "p -> []<>p" has been shown not derivable in S4.

Another use of Kripke C&S result is to show that S4, for example,

is decidable (and then write a theorem prover for S4). This is easy

if you succeed in refining the completeness part of the C&S theorem

above with "finite frame" instead of any frame. In that case

you know that if a counterexample exist you can find it.

But Kripke semantics is useless with a "non normal"

logic, for example a modal logic without the necessitation rule.

Chellas excellent book has a chapter on Scott-Montague semantics

(also known as "minimal model") which can be used in the same

way for weaker modal logic. The Scott-Montague semantics gives

"topological" or "quasi-topological" structure on the set of worlds.

In Kripke []p is true at world w if p is true at all worlds x such

that wRx. In Scott-Montague semantics []p is true at w if the set

of worlds in which p is true belongs to the neighborhoods of w.

Just to give you an idea of another semantics for modal logic.

Bruno

PS I recall my conversation on modal logic with George Levy in

this list. For example:

Modalities and Aristotle Square

http://www.escribe.com/science/theory/m2643.html

Leibtniz Semantics

http://www.escribe.com/science/theory/m2689.html

Kripke Semantics

http://www.escribe.com/science/theory/m2689.html

Received on Wed Aug 14 2002 - 07:46:15 PDT

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