# Prove or disprove statement for the smallest normal modal logic

I've come to the following problem:

Let n $$\geq$$ 1 and $$\phi_1 \dots \phi_n$$ are modal formulas:

Prove or disprove that the following are equivalent:

$$\bullet$$ At least one of the $$\phi_1 \dots \phi_n$$ is from the smallest normal modal logic (K)

$$\bullet$$ $$\square \phi_1 \lor \square \phi_1 \dots \lor \square \phi_n$$ is from the smallest normal modal logic (K).

I've come that the statement is true, but I can't seem to proove it formaly (in terms of modal logic). Any tips?

• Can you settle case $n=1$? Is one direction easier than the other? Commented Aug 25, 2021 at 16:42
• Here's a more explicit proof sketch for the backward direction using the common tableaux tree method. Say we want to prove $\vdash \square \phi_1 \implies \vdash \phi_1$, we can contradict its negation in the object language expressed as $\square \phi_1 \land \lozenge \lnot \phi_1$. And we know from Kripke relational model semantics, we can arrive at an accessible possible world at which $\lnot \phi_1$, but then we must derive $\phi_1$ at this world due to first conjunct, a contradiction. Same method for your forward direction $\vdash \phi_1 \implies \vdash \square \phi_1$ if you like ND style Commented Oct 7, 2021 at 22:23

I agree that it's true. The forward direction is easy (if $$\phi_i$$ is a theorem of K, then so is $$\square \phi_i$$ by necessitation, which implies the disjunction).
For the backward direction it is useful to consider the contrapositive statement: suppose that for all $$i$$, $$\phi_i$$ is not a theorem of K, and we want to show that $$\square \phi_1 \lor \cdots \lor \square \phi_n$$ is not a theorem of K. Here it is useful to think in terms of Kripke structures. For each $$i$$ because $$\phi_i$$ is not a theorem, there must be a Kripke structure $$\mathcal{S}_i$$ in which world $$w_i$$ is a counterexample. Then we can use this to construct a counterexample to $$\square \phi_1 \lor \cdots \lor \square \phi_n$$: just combine all the Kripke structures and add a new world $$w$$ which has arrows to $$w_i$$ for each $$i$$. The statement $$\square \phi_i$$ is false at $$w$$ because $$\phi_i$$ is false at $$w_i$$ and $$w_i$$ is a possible world from $$w$$.
P.S.: It is important to understand what we are showing here: that if $$\square \phi_1 \lor \cdots$$ is a theorem of K, then $$\phi_i$$ is a theorem of K for some $$i$$. Taking the case $$n = 1$$, what we showed is that if $$\square \phi_1$$ is a theorem, then $$\phi_i$$ is a theorem. This is not the same as saying that $$\square \phi_1 \to \phi_1$$ for any $$\phi_1$$, which is not a valid reasoning principle in K. In other words, what we showed was only for theorems, not for an arbitrary choice of $$\phi_1$$.
• A question here. Say $n=1$, then your conclusion for the 2nd direction shows $\square \phi_1 \rightarrow \phi_1$, which is just the reflexivity axiom T. But T is not an axiom in K... Commented Aug 25, 2021 at 17:46
• @mohottnad On the contrary! It doesn't show $\square \phi_1 \to \phi_1$, but rather that if $\square \phi_1$ is a theorem of K, then $\phi_1$ is a theorem of K. For example, we showed that if $\square (p \lor \lnot p)$ is a theorem of K, then so is $p \lor \lnot p$. But we did not argue that $\square p \to p$ is a theorem of K (that would not be true). Commented Aug 25, 2021 at 17:54
• Glad now you further pointed out the theorem semantic of the equivalence here. Also can you clarify why we can be assured there must be such a new world w which has arrows to every world $w_i$ at which $\phi_i$ is not a theorem per Kripke relational structure... Commented Aug 25, 2021 at 18:55
• @mohottnad Just construct it! The construct Kripke structure is the union of all the structures $\mathcal{S}_i$, together with one additional world $w$. Commented Aug 25, 2021 at 22:57