The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame.
For $1\leq s\leq n-2$, the frame $\mathcal{C}_n(s)$ denotes 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, 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
Assuming $\psi$ is a formula with $m$ variables and $n$ is a sufficiently large number. I want to construct a class of frames $\{\mathcal{A}_n(x)\}$ with index $x$, which satisfies:
- For any $x$, every point $u$ in $\mathcal{A}_n(x)$ with a depth of $u$ equal to 2 has a branching degree of 2, and every point $u$ with a depth greater than 2 has a branching degree greater than or equal to 3.
- If for every $x$, we have $\mathcal{A}_n(x) \nvDash \psi$, then there exists $s\leq n$ such that $\mathcal{C}_n(s) \nvDash \psi$.
Thus every formula $\phi(p_1, ... , p_t)$ which is valid in all $\{\mathcal{C}_{n'}(s)\}$, must be valid in some $\mathcal{A}_{n'}(x)$.
I posted a related question on MO which was solved by Emil Jeřábek. One could look at Emil Jeřábek's solution to find out that the frame $\mathcal{C}_n$ can not realize it.
My attempt to build $\{\mathcal{A}_n(x)\}$ is:
For $2\leq x\leq n-2$, the frame $\{\mathcal{A}_n(x)\}$ denotes 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, 0 \leq j \leq 3)\vee (i=n-1, j=0)\right\}, $$ with the accessibility relation described in
where $(x,0)$, $(x,1)$, $(x,2)$, $(x,3)$ can see every nodes $(i, j)$ with $i \leq x-1$.
For the given formula $\psi(p_1, ..., p_m)$, there will be some levels, e.g. $(i,0)$, $(i,1)$, $(i,2)$, $(i,3)$, that agree on any variable for each valuation $V$ on $\mathcal{A}_n(x)$ since the height $n$ is a sufficiently large number.
If $(x_0,0)$, $(x_0,1)$, $(x_0,2)$, $(x_0,3)$ agree on every variable for some valuation $V$ and $(\mathcal{A}_n(x_0), V) \nvDash \psi$, then we have a valuation $V'(p_t)=V(p_t) \setminus \{(x_0,1),(x_0,2),(x_0,3)\}$ on $\mathcal{C}_n(x_0)$, and $p$-morphism prove the result.
If for every valuation $V$ on $\mathcal{A}_n(x_0)$, we have $(x_0,0)$, $(x_0,1)$, $(x_0,2)$, $(x_0,3)$ don't agree on some variable, then there is a $x_1$ such that $(x_1,0)$, $(x_1,1)$, $(x_1,2)$, $(x_1,3)$ agree on every variable for valuation $V$. We turn to discuss $(\mathcal{A}_n(x_1), V)$ and so on. I am in trouble since I am not sure that this would form proof.
Does the $\{\mathcal{A}_n(x)\}$ I've constructed satisfy the requirements?
If not, do you have any suggestions on the construction of $\{\mathcal{A}_n(x)\}$?
