Notation:
I'll use 'A' to refer to an arbitrary proposition; '~' as the negation operator; 'Nec' as the necessity (box) operator; 'Pos' as the possibility (diamond) operator; '>' as material implication; and '/i' as the index denoting which possible world the entire preceeding statement is true of.
(For example, "PosA > NecPosA /w" means that the proposition "If A is possible then A is necessarily possible" is true in the possible world w.)
Let 'Gen' be used as a generic modal operator (i.e. it could be filled in by either 'Pos' or 'Nec', or the negation of either).
Also, I will use '=>' to represent a tree rule. Indexing does not extend across the arrow. So "X => Y /w" means that given 'X' in some branch, you can extend that branch by one level and write 'Y /w'.
Overview:
To motivate my view, note that modal statements don't say anything about the specific world they are indexed to. Rather, they make claims about the entire collection of possible worlds. ('NecA' means A is true in all possible worlds; 'PosA' means A is true in some possible world.) So the truth value of "GenA /i" should be constant across all possible indices i.
More formally, we can see that this ties in with axioms S4 and S5. Recall that S4 says: "NecA > NecNecA"; and S5 says "PosA > NecPosA". The combined effect of these axioms is to claim that if GenA is true, then GenA is necessarily true. That is, if GenA is true in the actual world, then GenA is true in all possible worlds.
My Proposal:
It simply doesn't matter what world we index a modal statement GenA to. It's either true of all of them, or false of all of them. So why bother indexing modal statements at all?
I propose that we stop indexing modal statements to possible worlds. (Though of course we must retain indexing for all nonmodal propositions in the proof!) This move would have both conceptual and formal benefits. Conceptually, it encourages us to recognise the nature of modal statements as being about the entire collection of possible worlds, rather than any one specific world. Formally, it can save us a few tedious steps when constructing a treebased proof, since we could close a branch the moment it contains both GenA and ~GenA (for the same modal operator 'Gen', of course!), whereas at present this contradiction might be (momentarily) hidden due to different indices being assigned to the respective modal statements.
The Formalities:
Converting the rules is really quite a simple process. The usual (nonmodal) rules are left untouched; and of the modal rules, we simply drop the index from all modal statements, and add one new 'deindexifying' rule.
Recall that the original modal rules are:
 PosA /w => A /i (for some new i)
 NecA /w => A /i (for any i) [Do not check off original statement]
 ~PosA /w => Nec~A /w
 ~NecA /w => Pos~A /w
My new rules would instead be:
 PosA => A /i (for some new i)
 NecA => A /i (for any i) [Do not check off original statement]
 ~PosA => Nec~A
 ~NecA => Pos~A
 GenA /w => GenA
That last rule (or some equivalent) needs to be added so that we can deindex any modal statements derived from the first two rules. See the sample proof below.
Either set of rules (if correctly applied) will give identical results when testing statements for logical consistency within the KTS5 modal system. But the latter set is tidier, faster, and conceptually clearer. So why not use it instead?
Sample Proof: Proving the S5 axiom
The Old Way:
[check] ~(PosA > NecPosA) /w

[check] PosA /w
[check] ~NecPosA /w

[check] Pos~PosA /w

[check] ~PosA /i

Nec~A /i

A /k (from 2)
~A /k (from 6)
X
The New Way:
[check] ~(PosA > NecPosA)

PosA
[check] ~NecPosA

[check] Pos~PosA

[check] ~PosA /i

~PosA
X
Quicker, tidier... better.
Yeah, you're right. If you're working in S5, then there is no need whatsoever for indexing statements to particular worlds. Best I can tell, indexing worlds with the tree rules is basically a hold over from working in more primitive systems (such as S4) where it is not always the case that a modal statement holds true at every world in the universe.
ReplyDeleteIn S4, where you can't do:
Gen(A) / w1
w1 R w2
=>
Gen(A) / w2
It is necessary to have the indexing rules, otherwise you would get incorrect results.
So the tree system (with indexing) is motivated, I think, so that the same system can be used for all logical systems, whether they are S4, S5, or something even more primitive. Yeah it would be cleaner to do away with indexing for S5 as much as possible, but then your system of proof falls out of step with proofs for other systems.
Make sense?
Yeah, I had been wondering how one would go about converting the tree rules to apply to more primitive systems. I don't suppose you'd happen to have a handy reference (or, better still, a URL) to some place where I could learn more about this matter?
ReplyDeleteMelvin Fitting has a few books about this, e.g., "Proof Methods for Modal and Intuitionistic Logics" and the (newer) Fitting and Mendelsohn, "Firstorder Modal Logic". Rajeev GorĂ© wrote a thesis on this which is available (in PostScript) at
ReplyDeletehttp://rsise.anu.edu.au/~rpg/publications.html
From the point of view of a logician, S5 is the most primitive modal logic in the sense that it has practically no structure. As pointed out by Andrew, the reason you index the modal formulas even in S5 is that the indexing is necessary once you pass to more interesting logics.
Posted by Richard Zach
Wow, a fellow philosogeek! BTW I've had Mendelsohn as a professor. You can access some of his papers and material from his recent book on his website, or you could last spring anyway. Here it is:
ReplyDeletehttp://comet.lehman.cuny.edu/mendel
Posted by JL
Thanks for the links!
ReplyDeletePosted by Richard
I can't make the claim to have had Mendelsohn as a prof, but I did use one of his books for a class. I learned most of the modal stuff with the help of a book called Possibilites and Paradox (the author escapes me at the moment and I'm too lazy to Amazon it :P) which was pretty well written and covers the basics of both modal and multivalued logics. I love this stuff. :)
ReplyDeleteI'll have to check out the links yall posted, and I'm checking out your blogs right now. It's always a pleasure to find someone else who knows something about symbolic logics. I absolutely want to learn much more.
Posted by Andrew
_Possibilities and Paradox: An Introduction to Modal and ManyValued Logics_ is by J.C. Beall and Bas van Fraassen. It is a good book.
ReplyDeletePosted by Mark
This is an interesting idea, but I think there are some mistakes in how you've presented it. All nonmodal formulas need to be indexed. Your argument should be:
ReplyDelete1 ~(PosA > NecPosA), i
2 PosA, i
3 ~NecPosA, i
4 Pos~PosA, i
5 ~PosA, j
6 Pos A
7 ~PosA
X
with the last two lines applying the deindexing rule to (2) and (5).
What's wrong with not indexing all the nonmodal formulas? Consider the tree for (NecA > A):
1 ~(NecA > A)
2 NecA
3 ~A
Now what? There's nothing more we can do. The problem is that the rule for Nec is "NecA => A /i (for any i)". In the above argument, we don't have an i, so we can't apply Nec.
It should be:
1 ~(NecA > A), i
2 NecA, i
3 ~A, i
4 NecA
5 A, i
X
So I'm not sure just how much your rules do simplify things. After all, the original rules would give us:
1 ~(NecA > A), i
2 NecA, i
3 ~A, i
4 A, i
X
Which seems to be simpler... applying your rules to the same argument, we have to add the superfluous step of deindexing Nec before we can use it. My guess is that your rules probably are simpler, but I'd have to work with them a little more to be sure.
Actually, re my previous comment, I don't my correction of your argument was quite right. It should be:
ReplyDelete1 ~(PosA > NecPosA), i
2 PosA, i
3 ~NecPosA , i
4 Pos~PosA, i
5 Pos~PosA
6 ~PosA, j
7 PosA
8 ~PosA
X
Per your rules, we need to deindex "Pos~PosA, i" before we can derive "~PosA, i", requiring an extra step. That gives us 8 steps, same as the original rules. So of the two arguments in my post, on your rules, one requires more steps than the original rules, and the other requires the same.