Preserve validity between the two Kripke frames

Question

The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame.

For $n \geq 1$, let $\mathcal{C}_n$ denote the frame which is shown in Fig.1. It is formed by the set: $$ \left\{(i, j)\in \omega \times \omega \mid (i=0, 0 \leq j \leq 1) \vee (1 \leq i \leq n-2, 0 \leq j \leq 3) \vee (i=n-1, j=0)\right\}, $$ with the accessibility relation described in

.

For $1\leq s\leq n-2$, the frame $\mathcal{C}_n(s)$ denote the frame which is shown in Fig.2. It is formed by the set: $$ \left\{(i, j)\in \omega \times \omega \mid (i=0, 0 \leq j \leq 1) \vee (1 \leq i \leq n-2, i \neq s, 0 \leq j \leq 3)\vee (i=s, j=0) \vee (i=n-1, j=0)\right\}, $$ with the accessibility relation described in

Thus the frame $\mathcal{C}_n(s)$ is obtained by gluing $(s,0)$, $(s,1)$, $(s,2)$, $(s,3)$ together of the frame $\mathcal{C}_n$.

I want to prove the following result:

Assuming $\psi$ is a formula with $m$ variables, $n$ is a sufficiently large number. Then there exists $s \leq n$ such that, if $\mathcal{C}_n \nvDash \psi$ then $\mathcal{C}_n(s)\nvDash \psi$.

My attempt at analysis is: let $\psi(p_1, ... ,p_m)$ be a formula with $m$ varibles. Because $V(p_j)$, the valuation on $\mathcal{C}_n$ of a given variable $p_t$, is an upset, there will be $(i,0)$, $(i,1)$, $(i,2)$, $(i,3)$, $(i-1,0)$, $(i-1,1)$, $(i-1,2)$, $(i-1,3)$ (or similar result for more points) agree on any variable when the height $n$ of $\mathcal{C}_n$ is sufficiently large. Then we have a valuation $V'(p_j):=V(p_j)\setminus \{(i,1), (i,2), (i,3)\}$ on $\mathcal{C}_n(i)$. $f$ is a map from $\langle\mathcal{C}_n, V\rangle$ onto $\langle\mathcal{C}_n(i), V'\rangle$: $f(x)=(i,0)$ if $x \in \{(i,0),(i,1), (i,2), (i,3)\}$ and $f(x)=x$ otherwise. I am in trouble since $f$ is not a $p$-morphism.

Answer 1

The result is actually false, for $m=6$. (One can bring it down to $m=2$ with a bit of effort.)

Let $n$ be arbitrarily large, and $\phi_n(\vec q)$ be a Jankov–De Jongh frame formula of $\def\p#1{\langle#1\rangle}\def\C{\mathcal C}\C_n$, so that for any frame $F$, $$F\nvDash\phi_n\iff\text{$\C_n$ is a p-morphic image of a generated subframe of $F$}.$$ Let $V$ be the valuation in $\C_n$ to the six variables $p_{(i,j)}$, $(i,j)\in\C_n$, $i\le1$, such that $$V(p_x)=\{y\in\C_n:y\nleq x\}.$$ We define a formula $\alpha_x(\vec p)$ for each $x\in\C_n$ by induction on $i$: $$\alpha_{(i,j)}=\begin{cases} p_{(i,j)}&i\le1,\\ \alpha_{(i-1,j)}\to\bigvee_{j'\ne j}\alpha_{(i-1,j')}&2\le i\le n-2,\\ \bigvee_{j'}\alpha_{(i-1,j')}&i=n-1. \end{cases}$$ Then we see by induction on $i$ that for all $x,y\in\C_n$, $$\p{\C_n,V},y\models\alpha_x\iff y\nleq x.$$ It follows that if $U$ is an arbitrary upper subset of $\C_n$, then $$y\in U\iff\p{\C_n,V},y\models\beta_U,$$ where $$\beta_U=\bigwedge_{x\notin U}\alpha_x.$$

Since $\C_n$ is a p-morphic image of itself, there is a valuation $W$ to the variables $\vec q$ such that $\p{\C_n,W}\nvDash\phi_n$. Let $\sigma$ be the substitution $$\sigma(q_i)=\beta_{W(q_i)}.$$ Then $$\p{\C_n,W},x\models\chi\iff\p{\C_n,V},x\models\sigma(\chi)$$ for all $x\in\C_n$ and all formulas $\chi(\vec q)$.

Thus, $\psi_n=\sigma(\phi_n)$ is a formula in the six variables $\vec p$, and by construction, $\C_n\nvDash\psi_n$ under $V$. However, for all $s\le n-2$, we have $\C_n(s)\models\phi_n$, and a fortiori $\C_n(s)\models\psi_n$, as $\C_n$ is not a p-morphic image of a generated subframe of $\C_n(s)$ (or of any other frame of size strictly smaller than $|\C_n|$, for that matter).

To reduce $m$ from $6$ to $3$, replace $V$ with a valuation of $\{p_0,p_1,p_2\}$ such that $V(p_0)=\{(0,0),(0,1),(1,0),(1,1)\}$, $V(p_1)=\{(0,0),(0,1),(1,0),(1,2)\}$, and $V(p_2)=\{(0,0)\}$. Show that you can still define suitable formulas $\alpha_x$.

To reduce it further to $m=2$, drop $p_2$, and show that you can define every upset $U\subseteq\C_n$ that does not differentiate the points $(0,0)$, $(0,1)$, and $(1,0)$. This allows you to carry out the argument above with $\phi_n$ replaced with the frame formula of the frame $\C'_n$ obtained from $\C_n$ by identifying $(0,0)$, $(0,1)$, and $(1,0)$. Note that $\C'_n$ still has strictly larger cardinality than $\C(s)$.

Finally, it is easy to show that the result holds for $m=1$, as there are only a constant number of formulas in one variable (up to equivalence) not valid in any $\C_n$.