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