Modal Logic: proof or refute

Question

I have the following statement:

$(A \land B) \rightarrow \square\lozenge(A \lor B)$ characterizes symmetry.

I am pretty sure there exists a proof for that statement since I am unable to find some counterexample.

But I am really struggling with a formal proof.

What I have done until now:

We need to prove two directions:

1. For all symmetric frames $\mathcal{F}$ we have $\mathcal{F} \vDash (A \land B) \rightarrow \square\lozenge(A \lor B)$

2. $\mathcal{F} \vDash (A \land B) \rightarrow \square\lozenge(A \lor B)$ implies that $\mathcal{F}$ is symmetric

But how do I correctly prove those?

Answer 1

1. Suppose $\mathcal{F}$ is a symmetric frame. Let $\mathcal{M}$ be a model based on $\mathcal{F}$. We would like to show that $(A\land B)\to \square\lozenge (A\lor B)$ is true at every world. So let $w$ be a world, and assume $A\land B$ is true at $w$. Let $v$ be a world such that $wRv$. Since $\mathcal{F}$ is symmetric, $vRw$. Since $A\land B$ is true at $w$, $A\lor B$ is true at $w$, so $\lozenge (A\lor B)$ is true at $v$. Since $v$ was arbitrary, $\square \lozenge (A\lor B)$ is true at $w$.
2. Suppose $\mathcal{F}$ is a frame validating $(A\land B)\to \square\lozenge (A\lor B)$. Assume for contradiction that $\mathcal{F}$ is not symmetric. Then there exist worlds $w$ and $v$ such that $wRv$ but $\lnot v R w$. Consider the model $\mathcal{M}$ based on $\mathcal{F}$ where $A$ and $B$ are both true at $w$ and $A$ and $B$ are both false at all other worlds. Then $(A\land B)$ is true at $w$. Since $(A\land B)\to \square\lozenge (A\lor B)$ is true at every world, $\square \lozenge (A\lor B)$ is true at $w$. Since $wRv$, $\lozenge (A\lor B)$ is true at $v$. So there is some world $u$ such that $vRu$ and $(A\lor B)$ is true at $u$. Since $\lnot vRw$, $u\neq w$. But by our definition of the model, $A$ and $B$ are both false at $u$, so $\lnot (A\lor B)$ is true at $u$, contradiction.

Answer 2

We can formulate the contention for the basic modal language as

$$(A\wedge B)\rightarrow\Box\Diamond(A\vee B)\text{ is a valid formula in a frame }F\iff F\text{ is a symmetric frame}$$

We shall consider a frame $F=\langle W, R\rangle$ and an associated model $\mathcal{M}=\langle W, R, V\rangle$, where $W$ is a nonempty set of worlds, $R$ is a binary accessibility relation on $W$, and $V$ is a valuation function assigning to each propositional variable $p$ a set $V(p)$ of possible worlds. The following equivalences will get employed:

$(i)\qquad wRw'\text{ holds}\iff w'\text{ is accessible from }w$

$(ii)\qquad w\in V(p)\iff p\text{ is true at }w$

$(iii)\qquad p\text{ is true at }w\iff\mathcal{M}, w\vDash p$

Let us begin with the left-to-right direction:

$$(A\wedge B)\rightarrow\Box\Diamond(A\vee B)\text{ is a valid formula in }F\implies F\text{ is symmetric}$$

So, we suppose $(A\wedge B)\rightarrow\Box\Diamond(A\vee B)$ is a valid formula in a frame $F$ and a world $w_{0}$ such that $w_{0}Rw_{i}$ if there exists an accessible world $w_{i}$. Then, we have

$$\mathcal{M}, w_{0}\nvDash A\wedge B\text{ or }\mathcal{M}, w_{0}\vDash\Box\Diamond(A\vee B)\implies F\text{ is symmetric}$$

which fits into the schema $((\neg\phi\vee\psi)\rightarrow\theta)\leftrightarrow((\neg\phi\rightarrow\theta)\wedge(\psi\rightarrow\theta))$. Hence, a common valuation for $A$ and $B$ is required to be used for both disjuncts in the antecedent; we shall not examine each valuation, but it should not be difficult to see that the combinations of the following arguments work for all valuations.

In the first disjunct of the antecedent, $\mathcal{M}, w_{0}\nvDash A$ or $\mathcal{M}, w_{0}\nvDash B$. Therefore, that $w_{0}\notin V(A)$ or $w_{0}\notin V(B)$ suffices (because of non-modality) for the consequent vacuously to hold, i.e., that $F$ is symmetric can be assigned true.

In the second disjunct of the antecedent, $\mathcal{M}, w_{0}\vDash\Box\Diamond(A\vee B)$. Then, that $w_{0}\in V(A)$ or $w_{0}\in V(B)$ must hold. For the sake of simplicity, let us choose $w_{0}\in V(A)$ and set $V(A)=\{w_{0}\}$ and $V(B)=\emptyset$ without loss of generality. Thus, $\mathcal{M}, w_{0}\vDash A$ and $\mathcal{M}, w_{0}\vDash A\vee B$. We have

$$\mathcal{M}, w_{0}\vDash\Box\Diamond(A\vee B)\iff\mathcal{M}, w_{i}\vDash\Diamond (A\vee B)\text{ for all }w_{i}\text{ such that }w_{0}Rw_{i}$$

and for some $w_{i}$

$$\mathcal{M}, w_{i}\vDash\Diamond(A\vee B)\iff\mathcal{M}, w_{j}\vDash A\vee B\text{ such that }w_{i}Rw_{j}$$

By our assumptions, $w_{j}\in V(A)$, thus $w_{j}=w_{0}$, hence, $w_{i}Rw_{0}$. Therefore, $F$ is symmetric.

Let us examine the right-to-left direction; so, we assume $F$ a symmetric frame:

$$F\text{ is symmetric}\implies (A\wedge B)\rightarrow\Box\Diamond(A\vee B)\text{ is a valid formula in }F$$

A shortcut for this case is to show that supposing the consequent to be false leads to a contradiction. So, we take $\mathcal{M}, w_{0}\vDash A\wedge B$ and $\mathcal{M}, w_{0}\nvDash\Box\Diamond (A\vee B)$. We have

$$\mathcal{M}, w_{0}\nvDash\Box\Diamond (A\vee B)\iff\mathcal{M}, w_{i}\nvDash\Diamond (A\vee B)\text{ for some }w_{i}\text{ such that }w_{0}Rw_{i}$$

$$\mathcal{M}, w_{i}\nvDash\Diamond (A\vee B)\text{ for some }w_{i}\text{ such that }w_{0}Rw_{i}\iff\mathcal{M}, w_{j}\nvDash A\vee B\text{ for all }w_{j}\text{ such that }w_{i}Rw_{j}$$

But one of the $w_{j}$ must be $w_{0}$ by our assumption that $R$ is symmetric, hence, $\mathcal{M}, w_{0}\nvDash A\vee B$, which contradicts our supposition that $\mathcal{M}, w_{0}\vDash A\wedge B$. Therefore, the consequent cannot be false, given the antecedent.