Leibniz Semantics

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