Marchal wrote:

> Hi George,
>
> I make the foolish promise to give you my
> proof.

We're even. I made the foolish promise to ask for your proof. :-)

With my background in electronic engineering, I am moderately versed in
logic, in particular Boolean logic. I am sorry for my long hmmmm. The
going got rough when you  started talking about knowability and
believability. But I realize that if we are to investigate consciousness
these are ideas that have to be talked about.

So let's go with it.. I promise I'll give it a shot. It will be very
instructive.... However it would help if together with the string of
symbols there was an English translation.

> 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.

I'll tell you!

>
>
> ====================
>
> 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

hmmm.... do you mean?

                  A v B     A -> B
                  1 1 1     1 1 1
                  1 0 1     1 0 0
                  0 1 1     0 1 x
                  0 0 0     0 1 x

> 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"...
>

OK


>
> 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.
>

OK


>
> 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.
>

OK

>
> 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.
>

OK

>
> 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
>

This string of symbols does not mean anything to me... Is there a real
life  model to which it applies, a story, a game, anything to give it
meaning?


>
> But let us go slowly).
>
> Bruno

So far so good

Thanks for making this effort.


George

Reply via email to