Logic is meaningless

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.

  1. A -> ~~A
  2. (A -> ~~A)
  3. A -> ~~A
  4. A -> ~~~~A
  5. A -> ~<>~A
    :confused: 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.)