# How to prove rigorously that " necessarily ( A OR ~A) " does not imply " necessarily A OR necessarily ~A"?

In De Interpretatione , Aristotle criticizes logical fatalism ( a metaphysical doctrine professed in the Megarian School, in particular by Diodorus Cronus).

Aristotle reconstructs the reasoning of logical fatalists as follow :

(1) Necessarily ( there will be a sea battle tomorrow or there will not be a sea battle tomorrow).

(2) Therefore, necessarily a sea battle will happen tomorrow or necessarily it will not happen.

One can say informally that the logical mistake consists in the fact that " the necessity of the disjunction does not imply the disjunction of the necessities".

However, how to prove rigorously using the tools of modal logic that the reasoning is not valid?

• Use "standard" Kripke semantics to manufacture a counter-example. Nov 12, 2019 at 21:09
• But A's example suffices : we have the "actual" world W1 were (e.g.) there will be a sea battle tomorrow and an "alternative" world W2 were there will be no sea battle tomorrow. This means that in both W1 and W2 the disjunction "there will be a sea battle tomorrow or there will not be a sea battle tomorrow" holds and this it holds in every possible world, i.e. it is necessarily true. But neither the first alternative nor the second one hol in every world, and thus no one of them is necessarily true. Nov 12, 2019 at 21:12
• With more technical terms, could also word this observation as "The necessity operator does not distribute over disjunction". Nov 12, 2019 at 21:21

As pointed out in the comments, a counterexample suffices to prove the invalidity of the argument, and the one cited by Aristotle is precisely one such counterexample.

Before we go about carrying out such a proof more precisely, here is a very quick introduction to the semantics of modal logic:

Models of modal logic are triples <W,R,h>, where

• W is a set of possible worlds (think of possible worlds as alternate universes if you like),
• R is a binary relation on W, the accessibility relation, which defines which worlds can access which other worlds (think of "w can access w'" (written wRw') as something like "w can imagine w'")
• h is a function that assigns to each combination of possible world and atomic proposition a truth value -- that is, h defines what is true at which world.

Thus in modal logic, truth is defined relative to worlds; truth in a model means truth in all worlds of the model.
In addition to the connectives of standard propositional logic, modal propositional logic has the modal operators ◻ and ◇, where ◻A is intended to mean "it is necessary that A" and ◇A is supposed to mean "it is possible that A".
Intuitively, a world w considers A necessary (◻A is true at w) iff A is true in every world accessible to w (or conversely, w can imagine no world where A is not the case), and w deems A possible (◇A is true at w) iff there is at least one world within the reach of w where A is true.
Note that a world only has access to those worlds for which we explicitly defined this -- in particular, R is not by default reflexive, that is, worlds don't automatically see themselves unless the tuple <w,w> is in R.

Formally, the semantics of the modal operators is defined as

[[◻A]]w = 1 ("◻A is true at w") iff for all w' ∈ W: if wRw' then [[A]]w = 1
[[◇A]]w = 1 ("◇A is true at w") iff there exists a w'∈ W: wRw' and [[A]]w = 1

and truth in a model is defined as

[[A]]M = 1 ("A is true in M, where M=<W,R,h>") iff for all w ∈ W, [[A]]w = 1

The modal translation of the two sentences is

◻(A∨¬A): "necessarily (there will be a sea battle tomorrow or there will not be a sea battle tomorrow)"
◻A∨◻¬A: "(necessarily there will be a sea battle tomorrow) or (necessarily there will not be a sea battle tomorrow)
where A = "there will be a sea battle tomorrow".

If we want to prove that the first doesn't imply the second, we need to find a model that satisfies the first but the second formula.¹
Let's construct a model with two worlds, w1 and w2, which can access themselves (depicted by the loop arrow below the worlds) and each other (depicted by the double arrow betewen w1 and w2) -- that is, each world can "imagaine" all possible worlds -- and h defined such that A is true in w1 (depicted by A written on top of w1) and no other proposition is true anywhere else. In this model, the tautology Av¬A will be true in both worlds and therefore necessary in both worlds, but from no world's perspective is it the case that A must be necessary or ¬A must be necessary, since they can each imagine both scenarios A and ¬A.

``````  A
----            ----
| w1 |  <---->  | w2 |
----            ----
^----'          ^----'
``````

Let M = <W,R,h> with
W = {w1, w2}
R = {<w1,w1>, <w1,w2>, <w2,w1>, <w2,w2>}
h : <w1,A> ↦ 1, and <w,B> ↦ 0 for all other worlds w and propositions B.

In this model, the following holds:

• [[A]]w1 = 1, by definition of h
• [[A∨¬A]]w1 = 1, since [[A]]w1 = 1
• [[A]]w2 = 0, by deifnition of h
• [[¬A]]w2 = 1, since [[A]]w2 = 0
• [[A∨¬A]]w2 = 1, since [[¬A]]w2 = 1
• [[◻(A∨¬A)]]w1 = 1, since [[(A∨¬A)]]w = 1 for every w such that w1Rw (= namely, w1 and w2)
• [[◻(A∨¬A)]]w2 = 1, since [[(A∨¬A)]]w = 1 for every w such that w2Rw (= namely, w1 and w2)
• [[◻(A∨¬A)]]M = 1, since [[◻(A∨¬A)]]w = 1 for every w ∈ W

We have thus shown that the first formula holds in our model; now it remains to show that the second one doesn't:

• [[A]]w2 = 0, by definition of h
• [[◻A]]w1 = 0, since not for every world w such that w1Rw, [[A]]w = 1 (namely, not in w2)
• [[A]]w1 = 1, by definition of h
• [[¬A]]w1 = 0, since [[A]]w1 = 1
• [[◻¬A]]w1 = 0, since not for every world w such that w1Rw, [[¬A]]w = 1 (namely, not in w1)
• [[◻A∨◻¬A]]w1 = 0, since neither [[◻A]]w1 = 1 nor [[◻¬A]]w1 = 1
• [[◻A∨◻¬A]]M = 0, since not for every w ∈ W, [[◻A∨◻¬A]]w = 1 (namely, not in w1)

So ◻A∨◻¬A is false in model M.

Since ◻(A∨¬A) is true in M but ◻A∨◻¬A is false in M, it is not the case for all models M' that if ◻(A∨¬A) is true in M', then ◻A∨◻¬A is true in M', hence ◻(A∨¬A) does not imply ◻A∨◻¬A.

And finally, since with the proposition A (= "There will be a sea battle tomorrow") we found a concrete instance of formulas φ for which the inference does not hold, we have that in general ◻(φ∨¬φ) ⊭ ◻φ∨◻¬φ, that is, the necessity operator does not distribute over disjunction.

Q.E.D.

¹ In modal logic, there actually are two competing notions of validity of an inference A1, ..., An ⊨ B:

1) Global validity:
A1, ..., An ⊨ B
⇔ For any model M, if A1, ..., An are true in M (= true in all worlds of M), then B is true in M (= all worlds of M)

2) Local validity:
A1, ..., An ⊨ B
⇔ For any model M, if A1, ..., An are true in M at a world w, then B is true in M at that world w

Global validity considers only the propositions that are true throughout all worlds of a model, while local validity cheks the inference world-wise. These two notions of logical implication are not equivalent (there are inferences which hold globally but fail locally; though if an inference holds locally, then it also holds globally). The inference in Aristotele's example is invalid under both interpretations of validity; I will be using the global version throughout my post.