I have been trying to do this logic proof for quite some time now, but cannot seem to figure it out.
Specifically, we are working in a stronger system than S4.
We will say this is S4.2, which is defined as all of S4 plus the axiom $\diamond \square \phi \rightarrow \square \diamond \phi$.
I am trying to prove axiomatically that $\neg \forall y \neg \square \forall x (\square Fx \rightarrow \diamond \square Fy)$
I have made numerous attempts to solve this. Specifically, I have tried to utilize the relation $ \forall x (Fx \rightarrow Fy) \rightarrow (Fx \rightarrow Fy)$
But I always run into a problem that cannot seem to be solved by invoking the S4.2 axiom.
In fact, I can't find where the S4.2 axiom could even be used.
I would really appreciate guidance on how to prove this statement.
Edit: As requested, I will provide further clarifications on what proof rules are available.
Specifically, we are defining our axiomatic system by mixing both the same techniques from propositional modal logic and first order predicate logic.
Therefore, when proving in S4, we are able to assume:
$$\forall \alpha \phi \rightarrow \phi (\alpha/\beta)$$ where $(\alpha/\beta)$ is the substitution of $\alpha$ for modal statement $\beta$.
We also have $$\forall \alpha (\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \forall \alpha \psi)$$
and then finally we have all the regular modal axioms:
$$K: \square (\phi \rightarrow \psi) \rightarrow (\square \phi \rightarrow \square \psi)$$
$$S4: \square \phi \rightarrow \square \square \phi$$
$$S4.2: \diamond \square \phi \rightarrow \square \diamond \phi$$
Also, we move deductively between theorems/axioms using the rules:
if $\phi$ is a theorem, then $\forall \alpha \phi$ is a theorem (universal generalization)
if $\phi$ is a theorem, then $\square \phi$ is a theorem (necessitation)
and if $\phi$ and $\phi \rightarrow \psi$ are theorems, then $\psi$ is a theorem (modus ponens)
Best Answer
For future searchability, this is Exercise 13.2(iv) on p. 254 of Hughes and Cresswell A New Introduction to Modal Logic. We are to prove $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ in the first-order modal logic S4.2 with Barcan's formula.
By the law of excluded middle, either $\exists y\lozenge\square F(y)$ or $\lnot \exists y\lozenge\square F(y)$.
Case 1: $\exists y\lozenge\square F(y)$.
By S4, $\square F(y)\rightarrow \square\square F(y)$ is a theorem. By necessitation and K (and taking contrapositives twice), $\lozenge\square F(y)\rightarrow \lozenge \square\square F(y)$ is a theorem. As an instance of S4.2, $\lozenge \square\square F(y)\rightarrow \square \lozenge \square F(y)$, so $\lozenge\square F(y)\rightarrow \square \lozenge \square F(y)$ is a theorem.
Now by first-order logic, $\lozenge\square F(y)\rightarrow \forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem, so by necessitation and K, $\square\lozenge\square F(y)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem. Combining with the result of the previous paragraph, $\lozenge\square F(y)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem.
By our Case 1 assumption and first-order logic, we obtain $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$, as desired.
Case 2: $\lnot \exists y\lozenge\square F(y)$. This is equivalent to $\forall x\square\lnot \square F(x)$.
By first-order logic, $\forall x\lnot\square F(x)\rightarrow \forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem, so by necessitation and K, $\square\forall x\lnot\square F(x)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem. As an instance of Barcan's formula, $\forall x\square\lnot \square F(x)\rightarrow \square\forall x\lnot\square F(x)$. So $\forall x\square\lnot \square F(x)\rightarrow \square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ is a theorem.
By our Case 2 assumption, we get $\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$. Adding the existential quantifier, $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$, as desired.
[Note that this last step assumes that our underlying first-order logic has existential import (i.e. is sound and complete for non-empty structures). I haven't checked that the system described in Hughes and Cresswell has existential import, but I assume it does - otherwise no sentence beginning with an existential quantifier is provable, since such a sentence is false on empty domains.]
Let me add something about the semantic motivation for this proof. I believe the the system in question (S4.2+Barcan's formula) is sound and complete for first-order non-empty constant domain Kripke frames which are directed preorders.
The desired sentence $\exists y\square\forall x(\square F(x)\rightarrow \lozenge\square F(y))$ says that there is some $y$ in world $w_1$ such that for every world $w_2\geq w_1$ and every $x$ in $w_2$, either (1) there is some world $w_3\geq w_2$ such that $F(x)$ is false at $w_3$, or (2) there is some world $w_3'\geq w_2$ such that $F(y)$ is true "on the cone above $w_3'$" (at every world $w_4\geq w_3'$).
Well, the easiest way to make (2) hold is if there is some $y$ in $w_1$ such that $F(y)$ is true on some cone above $w_1$. Indeed, if there is some world $v\geq w_1$ so that $F(y)$ is true on the cone above $v$, then for every world $w_2\geq w_1$ (and any $x$, but the choice of $x$ is irrelevant), since the frame is directed, we can pick some $w_3'$ such that $w_3'\geq v$ and $w_3'\geq w_2$. And since $F(y)$ is true on the cone above $v$, it is true on the cone above $w_3'$, so (2) holds. This semantic argument is formalized by the proof of Case 1 above.
On the other hand, suppose that there is no $y$ in $w_1$ such that $F(y)$ is true on some cone above $w_1$. Note that for every $w_2\geq w_1$ and every $x$ in $w_2$, it is not the case that $F(x)$ is true on the cone above $w_2$. Indeed, since our domains our constant, $x$ is also in $w_1$, and picking $y = x$ would contradict our assumption. This exactly means that there is some $w_3\geq w_2$ such that $F(x)$ is false at $w_3$. So picking any $y$ in $w_1$ (the choice is irrelevant), we have seen that (1) holds. This semantic argument is formalized by the proof of Case 2 above.