4
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ Can you settle case $n=1$? Is one direction easier than the other? $\endgroup$
    – hardmath
    Commented Aug 25, 2021 at 16:42
  • $\begingroup$ 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 $\endgroup$
    – cinch
    Commented Oct 7, 2021 at 22:23

1 Answer 1

Reset to default
1
$\begingroup$

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$.

$\endgroup$
4
  • $\begingroup$ 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... $\endgroup$
    – cinch
    Commented Aug 25, 2021 at 17:46
  • $\begingroup$ @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). $\endgroup$
    – Caleb Stanford
    Commented Aug 25, 2021 at 17:54
  • $\begingroup$ 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... $\endgroup$
    – cinch
    Commented Aug 25, 2021 at 18:55
  • $\begingroup$ @mohottnad Just construct it! The construct Kripke structure is the union of all the structures $\mathcal{S}_i$, together with one additional world $w$. $\endgroup$
    – Caleb Stanford
    Commented Aug 25, 2021 at 22:57

You must log in to answer this question.

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