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

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

Date: Thu Mar 22 10:32:25 2001

Hi George,

I make the foolish promise to give you my

proof. Here is Leibniz semantics for modal

logic. It is a preamble.

Don't hesitate to tell me if it is too difficult

or too easy, or too technical ...

I suppose you know a little bit of classical logic.

If you don't, just tell me. As a matter of fact

most physicist and philosopher today does not

know it.

It is necessary for the second part of my thesis.

(At least for a rigorous understanding of it).

It could be fun also, but if you don't like it

I can understand. It's also a matter of taste.

Remeber that my (long term) goal is just to make

you appreciate how big, and well structured, is

the plenitude from "the point of view of the

modest machine"!

Bruno

====================

We have some atomic propositions p, q, r, ...

And connectives &, v, ->, - (intended for "and", "or",

"if...then", "not").

We know what is a semantics for Classical Propositional

Logic (CL). Basicaly it an assignement of truth values,

among {FALSE, TRUE} for the atomic propositions.

The semantics of well formed formula like p & (q v r)

will follow by the usual use of truth table. For exemple:

A v B A -> B

1 1 1 1 1 1

1 1 0 1 0 0

0 1 1 0 1 1

0 0 0 0 1 0

Note that the truth value of a formula is completely

determined by the truth value of its compounds.

The problem is to provide a clean semantics (meaning) for

sentence like []p -> p or <>p -> []q, ... with the intuitive

reading "if necessary p then p","if possible p then

necessary q"...

Like the not "-", the box "[]" and the diamond "<>" are unary

connective and it is obvious that we cannot define them

truth functionaly (unless we define the box by the

identity and the diamond by not, but that would be rather

trivial). The truth value of a formula will no more completely

be determined by the truth value of its compounds!

In "Leibniz semantics" there is a collection W of worlds.

That collection of world is called a frame.

The frame W becomes a model (W,V) when there is given

a valuation V, assigning truth values to the atomic

propositions in each world.

Each world is supposed to "obey" classical logic. This means

that if p is true in world w and if q is true in world w, then

p & q is true in world w, etc.

I will say that the model (W,V) is based on the frame W.

Here is Leibniz semantics for modal propositions.

In any world, []p will be considered true if p is true

in all worlds of W. And in any world, <>p will be considered true,

if there is (at least one) world in W in which p is true.

This captures the intuitive idea that "p is necessary" means

p is true in all possible conceivable situations, worlds, states,

etc. and "p is possible" if there is at least one world (states ...)

where p is true. That's the idea often attributed to Leibniz.

Validity is the key notion (generalising the notion of tautology

in the non modal case).

I will say that a formula is valid in a frame, if the formula

is true in all the worlds of all models based on that frame.

A simple (non modal) tautology is of course valid. For exemple

"p v -p" is true in all world independently of the valuations.

[]p v -[]p is also valid.

Exercices: 1) is []p -> p valid? 2) is p -> []p valid?

Solution: Yes []p -> p is valid. let take an arbitrary world w

in an arbitrary model (W,V) if []p is true in w, it means p

is true in all world of the model (W,V), then it is true

in particular in w, so []p -> p is true in w. This works

for all w (note that if []p is false in w, then []p -> p is

automatically true in w. So []p -> p is valid.

2) no p -> []p is not valid. Take a frame with two worlds

w1 and w2, and take a valuation which makes p true in w1 and

which make p false in w2. Clearly in w1 you have p and -[]p,

so in w1 p -> []p is false.

Exercices. Show that the following sentences are valid:

p -> <>p

[]p -> [][]p

p -> []<>p

<>p -> []<>p

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

Of course if <>p -> []<>p is valid, <>TRUE -> []<>TRUE is

certainly valid to, and so our "godel second theorem"

<>TRUE -> -[]<>TRUE is certainly NOT valid with Leibniz

semantics. This just means that formal provability cannot

play the role of the leibnizian "necessity".

Kripke generalisation of Leibniz semantics will provide

the necessary tools.

The non logician should note that with a semantics we can

reason on the validity of sentences without having a formal

system in which we could *prove* those formula.

A "difficult" exercice would consist in finding a formal

system which would axiomatize the Leibnizian formula.

(In fact it is axiomatized by the system known as S5 which

has the axioms:

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

[]p->p

<>p -> []<>p

+ the classical tautologies.

with the inferences rules:

p p->q p

------- --- + a substitution rule

q []p

But let us go slowly).

Bruno

Received on Thu Mar 22 2001 - 10:32:25 PST

Date: Thu Mar 22 10:32:25 2001

Hi George,

I make the foolish promise to give you my

proof. Here is Leibniz semantics for modal

logic. It is a preamble.

Don't hesitate to tell me if it is too difficult

or too easy, or too technical ...

I suppose you know a little bit of classical logic.

If you don't, just tell me. As a matter of fact

most physicist and philosopher today does not

know it.

It is necessary for the second part of my thesis.

(At least for a rigorous understanding of it).

It could be fun also, but if you don't like it

I can understand. It's also a matter of taste.

Remeber that my (long term) goal is just to make

you appreciate how big, and well structured, is

the plenitude from "the point of view of the

modest machine"!

Bruno

====================

We have some atomic propositions p, q, r, ...

And connectives &, v, ->, - (intended for "and", "or",

"if...then", "not").

We know what is a semantics for Classical Propositional

Logic (CL). Basicaly it an assignement of truth values,

among {FALSE, TRUE} for the atomic propositions.

The semantics of well formed formula like p & (q v r)

will follow by the usual use of truth table. For exemple:

A v B A -> B

1 1 1 1 1 1

1 1 0 1 0 0

0 1 1 0 1 1

0 0 0 0 1 0

Note that the truth value of a formula is completely

determined by the truth value of its compounds.

The problem is to provide a clean semantics (meaning) for

sentence like []p -> p or <>p -> []q, ... with the intuitive

reading "if necessary p then p","if possible p then

necessary q"...

Like the not "-", the box "[]" and the diamond "<>" are unary

connective and it is obvious that we cannot define them

truth functionaly (unless we define the box by the

identity and the diamond by not, but that would be rather

trivial). The truth value of a formula will no more completely

be determined by the truth value of its compounds!

In "Leibniz semantics" there is a collection W of worlds.

That collection of world is called a frame.

The frame W becomes a model (W,V) when there is given

a valuation V, assigning truth values to the atomic

propositions in each world.

Each world is supposed to "obey" classical logic. This means

that if p is true in world w and if q is true in world w, then

p & q is true in world w, etc.

I will say that the model (W,V) is based on the frame W.

Here is Leibniz semantics for modal propositions.

In any world, []p will be considered true if p is true

in all worlds of W. And in any world, <>p will be considered true,

if there is (at least one) world in W in which p is true.

This captures the intuitive idea that "p is necessary" means

p is true in all possible conceivable situations, worlds, states,

etc. and "p is possible" if there is at least one world (states ...)

where p is true. That's the idea often attributed to Leibniz.

Validity is the key notion (generalising the notion of tautology

in the non modal case).

I will say that a formula is valid in a frame, if the formula

is true in all the worlds of all models based on that frame.

A simple (non modal) tautology is of course valid. For exemple

"p v -p" is true in all world independently of the valuations.

[]p v -[]p is also valid.

Exercices: 1) is []p -> p valid? 2) is p -> []p valid?

Solution: Yes []p -> p is valid. let take an arbitrary world w

in an arbitrary model (W,V) if []p is true in w, it means p

is true in all world of the model (W,V), then it is true

in particular in w, so []p -> p is true in w. This works

for all w (note that if []p is false in w, then []p -> p is

automatically true in w. So []p -> p is valid.

2) no p -> []p is not valid. Take a frame with two worlds

w1 and w2, and take a valuation which makes p true in w1 and

which make p false in w2. Clearly in w1 you have p and -[]p,

so in w1 p -> []p is false.

Exercices. Show that the following sentences are valid:

p -> <>p

[]p -> [][]p

p -> []<>p

<>p -> []<>p

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

Of course if <>p -> []<>p is valid, <>TRUE -> []<>TRUE is

certainly valid to, and so our "godel second theorem"

<>TRUE -> -[]<>TRUE is certainly NOT valid with Leibniz

semantics. This just means that formal provability cannot

play the role of the leibnizian "necessity".

Kripke generalisation of Leibniz semantics will provide

the necessary tools.

The non logician should note that with a semantics we can

reason on the validity of sentences without having a formal

system in which we could *prove* those formula.

A "difficult" exercice would consist in finding a formal

system which would axiomatize the Leibnizian formula.

(In fact it is axiomatized by the system known as S5 which

has the axioms:

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

[]p->p

<>p -> []<>p

+ the classical tautologies.

with the inferences rules:

p p->q p

------- --- + a substitution rule

q []p

But let us go slowly).

Bruno

Received on Thu Mar 22 2001 - 10:32:25 PST

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