I have a question regarding disjunction and necessity.

Is the following theorem provable in any system of modal logic, or is it not generally true?

⊢ A ∨ B → □A ∨ □B

I was thinking about using the truth functional definition of OR to answer the question myself. I think it's true, but I don't know how to prove it.

  • 2
    It is trivially false, take B = ¬A.
    – Conifold
    Commented May 27 at 12:43
  • Necessity and possibility are nothing but a half-baked attempt at something probability theory does better. ("Necessary" = probability of 1, "possible" = nonzero probability)
    – causative
    Commented May 27 at 18:21

2 Answers 2


⊢ (A ∨ B) → (□A ∨ □B) is certainly not generally true, but it is a theorem of a rather weird modal system called Ver. The system Ver consists of the system K together with the axiom

  ⊢ □P

In other words, by substitution, □A is true for any A, including □⊥. It might seem like this system is inconsistent, but it is not. It lacks the reflexive T axiom, so □⊥ does not entail ⊥. Ver includes the necessitation rule, so it is a normal modal logic. Its frame condition is that of a world with no worlds accessible to it, including itself.

Since □A and □B are both theorems, □A ∨ □B is a theorem and hence so is (A ∨ B) → (□A ∨ □B).


Axioms of SQML

The question is, is the following a theorem of any modal logic?

⊢ A ∨ B → □A ∨ □B

To me it seems to be a consequence of the truth functional definition of OR. If 'A or B' is true then A must be true or B must be true.

So suppose it's not a theorem of some modal logic. Then it's antecedent can be true while its consequent is false in that logic.

  1. (A ∨ B) ∧ ~(□A ∨ □B)
  2. (A ∨ B) ∧ (~□A ∧ ~□B) [DM]
  3. (A ∨ B) ∧ (◊~A ∧ ◊~B) [Df]

But from the truth functional definition of OR: the only row in which (◊~A ∧ ◊~B) is true is the row in which A,B are simultaneously false, or equivalently ~A,~B are simultaneously true. That means ~A ∧ ~B, which means ~(A ∨ B). Thus in that modal logic (A ∨ B) ∧ ~(A ∨ B). Thus, any modal logic in which does not have

⊢ A ∨ B → □A ∨ □B

is perforce inconsistent.

So I followed my instinct, and used the truth functional definition of OR to answer the question.

A B ~A ~B ◊~A ◊~B ~◊~A ~◊~B ~◊~A∨~◊~B
0 0 1 1 1 1 0 0 0
0 1 1 0 1 0
1 0 0 1 1 0
1 1 0 0

These were all the table entries I was initially certain of.

B is true in row 2. Then I looked at row 2, column 8, and asked myself, could there be a zero there. If the answer is yes then ◊~B when B is true.

I then constructed the following demonstration.

 1. B ∧ ◊~B                     [OSC1]
 2. B ∧ ~☐B                     [1;Df]
 3. B                           [2;simp1]
 4. ☐B                          [3;NEC]
 5. ~☐B                         [2;simp2]
 6. ☐B ∧ ~☐B                   [4,5;conj]
 7. (B ∧ ◊~B)→ contradiction   [1-6;CSC1]
 8. ~(B ∧ ◊~B)                  [7;RAA]
 9. ~(B ∧ ~~◊~B)                [8;DN]
 10. B → ~◊~B                   [9;Df]
 11. B → ☐B                    [10;Df]
 12. ☐B→ B                     [T]
 13. B ↔ ☐B                   [11,12,conj,Df]

At this point I knew how to fill in all the entries of the table.

A B A∨B ☐A ☐B ☐A∨☐B (A∨B)→(☐A∨☐B)
0 0 0 0 0 0 1
0 1 1 0 1 1 1
1 0 1 1 0 1 1
1 1 1 1 1 1 1

Therefore (A∨B)→(☐A∨☐B) is a tautology in SQML.

EDIT - Suppose B can be true at one accessible world w1, and false at another w0.

World B ~B ◊~B B∧◊~B ~(B∧◊~B)
w0 0 1 1 0 1
w1 1 0 0 0 1


⊢ ~(B∧◊~B)

⊢ ~(B∧~~◊~B)

⊢ ~(B∧~☐B)

⊢ B→☐B

Which is the same result as before, but this time I didn't use NEC.

  • 5
    That sentence is not a theorem of SQML. It has a countermodel as follows: at world w0, A is true, B is false; at world w1, A is false, B is false. As I have explained in detail in my answer to this question the necessitation rule NEC is a rule of proof, not a rule of inference, so it cannot be used in the way you are trying to use it.
    – Bumble
    Commented May 27 at 17:37
  • @leepappas you’re not understanding the definition of ‘☐’. It’s saying that at any accessible world, the formula under its scope is true. That some contingent formula A is true doesn’t mean ☐A is true.
    – PW_246
    Commented May 27 at 19:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .