Proving this is a theorem of $\mathbf{S4.4}$: modal logic

299 Views Asked by At

Problem: The system $\mathbf{S4.4}$ of modal logic adds to the system $\mathbf{S4}$ the axiom $(A \wedge \Diamond \Box A) \rightarrow \Box A$. Show that $$ (\Diamond A \wedge \Diamond B) \rightarrow (\Diamond (A \wedge \Diamond B) \vee \Diamond (B \wedge \Diamond A))$$ is a theorem of $\mathbf{S4.4}$.

Attempt: In $\mathbf{S4}$ I have the following additional axioms:

(i) $\Box A \rightarrow A$

(ii) $\Box A \rightarrow \Box \Box A$ and their duals.

Furthermore, axioms of minimal temporal logic include axioms like $\Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)$ and stuff like $(\Box A_1 \wedge \ldots \wedge \Box A_n) \leftrightarrow \Box (A_1 \wedge \ldots \wedge A_n)$.

To prove the statement, it is enough to prove $(\Diamond A \wedge \Diamond B) \rightarrow \Diamond (A \wedge \Diamond B)$. It is enough to prove the dual, which is $ \Box (A \vee \Box B) \rightarrow \Box A \vee \Box B$.

Now, the axiom $\Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)$ is equivalent to $$ \Box (A \vee B) \rightarrow (\Diamond A \vee \Box B). $$ Performing a substitution, I get $$ \Box (A \vee \Box B) \rightarrow (\Diamond A \vee \Box \Box B). $$ Now, taking the dual of the additional axiom of $\mathbf{S4.4}$, I see that $$ \Diamond A \rightarrow A \vee \Box \Diamond A.$$

Furthermore, using axiom (i), I see that $\Box \Box B \rightarrow \Box B$ where I also used substitution. Therefore, I know that $$ \Box (A \vee \Box B) \rightarrow A \vee \Box \Diamond A \vee \Box B. $$ This is almost what I need, except that I need to prove somehow that $$ A \vee \Box \Diamond A \rightarrow \Box A $$ and this is where I'm stuck.

Any help is appreciated.

1

There are 1 best solutions below

0
On BEST ANSWER

Your proof is not erroneous, though the desired final implication $$A\vee\Box\Diamond A\rightarrow \Box A$$ is not a theorem of S4.4. It is easy to build a two-state Kripke model of S4.4 in which the first state sees the second but not vice versa, and a proposition $A$ which holds for the first state, but not the second. In this model, this implication fails.

Unfortunatly, the first step already doomed you,S4.4 does not prove $$\Diamond A\wedge\Diamond B\rightarrow\Diamond( A\wedge\Diamond B)$$ The counterexample form above is a counterexample here as well.

So let us assume $$\Diamond A\wedge\Diamond B \wedge \neg \Diamond( A\wedge\Diamond B)$$ which is equivalent to $$\Diamond A\wedge\Diamond B \wedge \Box (\neg A\vee\Box \neg B)$$ and recall that we want to show $$\Diamond(\Diamond A\wedge B)$$ from the above. From T we get $\neg A\vee\Box\neg B$ and as $\Diamond B$ holds, $\neg A$. I claim $$\Box\Diamond A$$ If this fails, $$\Diamond\Box\neg A$$ and from S4.4 and $\neg A$ we conclude $$\Box\neg A$$ which contradicts $\Diamond A$. Thus we have $$\Diamond B\wedge\Box\Diamond A$$ and hence $$\Diamond(B\wedge \Diamond A)$$ as desired.