Logic Trees and Modal Indexicals

In logic class the other day, we were learning how to do "semantic trees" for the modal system KTS5, and I suggested that indexing modal statements to particular worlds (as we were told must be done) was redundant. My professor wasn't convinced, however, so I'll use this post to set out and clarify my argument.

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 non-modal 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 tree-based 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 (non-modal) rules are left untouched; and of the modal rules, we simply drop the index from all modal statements, and add one new 'de-indexifying' 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 de-index 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.