In system K, ◇A is defined to mean ~◻~A. Therefore, it is very tempting to conclude ◇◇A means ~◻~~◻~A. But I am not certain whether this is valid conclusion to make, because in ◇◇A, the main operator is ◇ on the left: ◇(◇A) means ~◻~(◇A) or simply ~◻~◇A. Now here the main operator is the negation ~, and I cannot seem to access the ◇ operator to conclude ~◻~~◻~A. I was wondering if a proof can be given that ◇◇A is equivalent to ~◻~~◻~A or is it enough to say that ◇◇A is equivalent to ~◻~~◻~A by the definition?
1
-
When an operator is defined in some way you can "access" it anywhere in the formula to substitute its definition there, so ◇◇A≡~◻~~◻~A≡~◻◻~A is a theorem of K, and the first ≡ is by definition. Whether the definition itself is justified based on pre-existent intuitive concepts of possibility and necessity is a different question, some modal logics introduce ◇ and ◻ independently and do not reduce one to the other.– ConifoldOct 18, 2021 at 7:17
Add a comment
|
2 Answers
There's an interesting subtlety here. The statement
(1): ◇A is defined to mean ~◻~A,
is extremely strong. For example, thinking in terms of a sequent calculus with both ◇ and ◻ included as primitives, this corresponds to having available the following (hypothesis-free) inference rule:
(A): For every sentence p, if q is a sentence gotten from p by replacing some instances of "◇" with "~◻~" or vice versa, then {p} ⊢ q is a valid sequent.
This is much much stronger than the following rule:
(B): For every sentence a, both {~◻~a} ⊢ ◇a and {◇a} ⊢ ~◻~a are valid sequents.
(If you prefer a Hilbert-style system, think of (A) as saying "if p is a sentence and q is a sentence gotten from p by replacing some instances of "◇" with "~◻~" or vice versa, then p↔q is a tautology" and think of (B) as saying "for every sentence a, ~◻~a ↔ ◇a is a tautology.")
The rule (B) does not in fact allow you to apply the "~◻~/◇"-translation "inside" a sentence, and the difficulty you're seeing in your OP essentially amounts to your interpretation of (1) as (B) rather than (A).
In general, a lot of care must be taken around phrasing and using substitution rules!
answered Oct 18, 2021 at 4:58
-
Interesting point. One could say the same about the rule of double negation elimination in propositional logic, but presumably the difference there is that we can always manipulate the DN into prime position by using the rule of conditional proof, or something equivalent. Does it follow then that your A and B rules are equivalent if the deduction theorem applies, or would we need something stronger?– BumbleOct 18, 2021 at 16:25
First of all, you can just define things it were a game, because you can Esasy create a inconsistent system of axioms, you had to justify and if possible just prove the stament form the other axioms.
Proof:
◇(◇A) = ~◻~(◇A) By application of the definition of ◇x
~◻~(◇A) = ~◻~~◻~A By a second application of the definition of ◇x
Hence has been proved that ◇◇A is logically equivalent to ~◻~~◻~A.
