That’s what I love most about Spiritus. He makes people think.
Spiritus, I am looking over your step 2, A->A with necessitation as a justification, but I don’t think it applies there as you’ve written it. Necessitation only shows that what we prove a priori is necessary (and when you think about it, one would hope so). That A is the case doesn’t make it necessary.
But, I admit, I cannot think of how else to do it without asserting
A -> <>A in the first place, after which (as we have shown) it is trivial.
- A -> ~~A
- (A -> ~~A)
- A -> ~~A
- A -> ~~~~A
-
A -> ~<>~A
I have been trying this off and on all day and I can get all kinds of possibles, but there’s always a stupid negation I can’t eliminate.
5 is interesting though. It seems that, just like <> can be defined as ~~, can be defined as ~<>~. The symmetry surprised me, though I don’t know why.
erl
Hmmmm . . . you might be right. I would have to include classical quantifiers to get that application of necessity. Actually, I might be able to since we start with “the principles of propositional logic”, but that strikes me as a bit dodgy since I know there is great disagreement over how to apply and read the classical quantifiers in modal contexts. Hmmmm . . . I might be right.
Damn, I told you I was no expert. It really should be trivially derivable in just T. Maybe including an existential quntifier is the right way to go, but I get the feeling I am overlooking something else: something outrageously obvious.
Yes, the symmetry is implicit in the definitional relationship. You can start with either or <> as the primitive. (Well, except for some modal forms designed to model actualism, which require both to be primitive: no symmetry, no elegance, no implication of necessary existence.)
Eris wrote:
That is the exact definition of , if I recall.
Well, either one can be defined in terms of the other. Usually, I believe, is taken as the primitive with <> = ~~ by definition. But the of th relationship is easily demonstrated:
<>A = ~~A
<>~A = ~~~A
<>~A = ~A
~<>~A = ~~A
~<>~A = A
(Of course, erl had already given a derivation above, but I wanted to actually solve a trivial derivation for once.)