If $S5 \vdash \alpha$ then $S4 \vdash \diamond \alpha$

Question

I would like to prove that if S5 proves $\alpha$ then S4 proves $\diamond \alpha$. Here S4 is K plus axioms for reflexivity ($\square \alpha \to \alpha$) and transitivity ($\square \alpha \to \square \square \alpha$), and S5 is S4 plus the axiom $\diamond \alpha \to \square \diamond \alpha$.

My attempts:

I tried to prove it semantically, i.e. that if $\alpha$ is true in every reflexive, transitive, symmetric model then $\diamond \alpha$ is true in every reflexive, transitive model (and then use completeness), by using something like a "symmetric closure" of the relation, but I got stuck ($\alpha$ may be "complicated", I'm not sure how to handle all of the cases...).

I also tried to prove it by induction on the proof of $\alpha$ from S5. I think I was able to prove $S4 \vdash \diamond \alpha$ in case that $\alpha$ is an axiom of S5, but that is not enough, I need to take care of MP and NEC ($\vdash \alpha \Rightarrow \vdash \square \alpha$). For example for NEC I would like to prove that if $S4 \vdash \diamond \alpha$ then $S4 \vdash \diamond \square \alpha$, but I am not sure it is even true (if a model satisfies $\diamond \alpha$ it does not have to satisfy $\diamond \square \alpha$, right?).

I even tried by induction on the structure of $\alpha$ but got stuck (the induction step does not really work).

I do not think it is supposed to be a difficult question so I guess I am missing something.

Thanks in advance!

Answer 1

Here is a proof which relies in the fact that S4 has the finite model property.

If $S4 \nvdash \Diamond \alpha$, then you have a finite Kripke model $M$ where the accessibility relation is a preorder and a world $w$ in $M$ where $\Diamond \alpha$ fails. If $\Diamond \alpha$ fails in $w$, then $\alpha$ fails in every world $w'$ accessible from $w$. In particular, $\alpha$ fails in a maximal world $w'$ in the accessibility preorder, i.e. in a world $w'$ such that $w' R v$ implies $v R w'$. The submodel $M'$ generated by $w'$, i.e. the submodel consisting of the worlds which are equivalent to $w'$ in the equivalence relation induced by the accessibility preorder, is then an S5 model which falsifies $\alpha$.

Answer 2

We can use the truth of the lozenge-ified version of the axiom $(\lozenge \beta \to \square \lozenge \beta)$ to grab ourselves a new model on the same Kripke frame where all of the $\mathsf{S5}$ axioms hold. This model does not necessarily have a symmetric accessibility relation, even if we prune away now-unreachable worlds; I'm only promising that its set of tautologies is a superset of the set of $\mathsf{S5}$-tautologies.

Lemma 101: $\lozenge (\lozenge \beta \to \square \lozenge \beta)$ is an $\mathsf{S4}$-tautology.

We can prove this using a tableau with a single branch.

My worlds are $0, 1, 2$. It holds that $0R1$, $0R2$, $2R3$. $0R3$ holds implicitly by transitivity of the accessibility relation.

1. $0 : \square(\lozenge \beta \land \lozenge \square \lnot \beta)$ is our negated goal.
2. $0 : \lozenge \beta \land \lozenge \square \lnot \beta$ follows by necessitation.
3. $0: \lozenge \beta$
4. $0 : \lozenge \square \lnot \beta$
5. $1 : \beta$ holds at a fresh world $1$.
6. $2 : \square \lnot \beta$ holds at a fresh world $2$.
7. $2 : \lozenge \beta \land \lozenge \square \lnot \beta$ follows by necessitation.
8. $2 : \lozenge \beta$
9. $2 : \lozenge \square \lnot \beta$
10. $3 : \beta$ holds at a fresh world $3$.
11. $3: \lnot \beta$ follows by necessitation.
12. Contradiction

We can also prove it using the topological semantics for $\mathsf{S4}$. Let $c$ be the complement, $i$ be the interior, $e$ be the exterior, and $k$ be the closure.

Note $\lozenge (\lozenge \beta \to \square \lozenge \beta)$ is equivalent to $((B^k)^c \cup (B^k)^i)^c$, with the modal symbols being replaced with their topological equivalents.

1. $((B^k)^c \cup (B^k)^i)^k$
2. $(B^e \cup B^i)^k$
3. $B$

Since this holds in an arbitrary topological space, we are done.

Proof

Let $\alpha$ be an arbitrary well-formed formula such that $\mathsf{S5} \vdash \alpha$.

Consider an arbitrary $\mathsf{S4}$-model $(W, R, w)$. By Lemma 101 and the truth conditions of $\lozenge$, there exists a model $(W, R, u)$ such that $\lozenge \beta \to \square \lozenge \beta$ holds at that model and $wRu$

$(W, R, u)$ thus has all of the tautologies of $\mathsf{S5}$.

Therefore $(W, R, u) \models \alpha$.

Therefore $(W, R, w) \models \lozenge \alpha$ as desired.

Since our model was chosen arbitrarily, it holds that $\mathsf{S4} \vdash \lozenge \alpha$.

Answer 3

Following @GregNisbet's answer and @AlexKruckman's comment (and a great help from a friend), here is an answer (sketch; not using fmp):

Lemma 1: $S4\models\lozenge M4$ for every $\varphi$. (M4 is the axiom scheme $\lozenge\varphi\to\square\lozenge\varphi$).

Lemma 2: Let M be a model with a reflexive and transitive relation $R$ (preorder). If $M,u\models\lozenge\varphi\to\square\lozenge\varphi$ for some given $\varphi$, then $M,v\models\lozenge\varphi\to\square\lozenge\varphi$ for every $v$ such that $R(u,v)$.

Both lemmas can be proved (semantically) quite easily.

Now let $\{\alpha_i\}_{i=1}^n$ be the instances of M4 that are used in the proof of $\alpha$ from S5. So we observe $S4,\{\alpha_i\}_{i=1}^n\models\alpha$.

Let M be a preordered model and $w_0$ in M. For $i\in\{1...n\}$, let $w_i$ be a world that satisfies $\alpha_i$ such that $R(w_{i-1}, w_i)$ (exists because of Lemma 1). From Lemma 2, the model $M^{w_n}$ (which is M reduced to the worlds that are seen from $w_n$) satisfies $\{\alpha_i\}_{i=1}^n$ so from the observation above it satisfies $\alpha$, which leads to $M,w_0\models\lozenge\alpha$. $w_0$ was arbitrary and M was an arbitrary preordered model so from the completeness of S4 w.r.t such models we get the result.

Any corrections or improvements? :)