Possible values of "Kripke rank" for formulae in IPL

Question

Fix a (countable) set $\mathcal{P}$ of atomic propositional variables. Recall a Kripke model $\mathcal{K}$ for intuitionistic propositional logic (IPL) consists of:

• A preorder $(W,\leq)$
• For each $w \in W$, a (classical) valuation $\varphi_w\colon \mathcal{P} \to 2$

such that for all $w \leq v$ and $x \in \mathcal{P}$, having $\varphi_w(x) = 1$ implies $\varphi_v(x)=1$.

We can extend the valuations $\varphi_w$ to a forcing relation $w \Vdash F$ between states $w \in W$ and arbitrary formulae $F$, using the schema here. We then say $W \Vdash F$ if $w \Vdash F$ for all $w \in W$.

These semantics are sound and complete for IPL, so we can show a formula $F$ is not a tautology of IPL by exhibiting a Kripke model where it doesn't hold. For example, let $\mathcal{P} = \{ P \}$ and let $\mathcal{K}$ be: $$ (P = \mathsf{true}) \\ \uparrow \\ (P = \mathsf{false}) $$

Then $\mathcal{K} \nVdash P \lor \neg P$ and $\mathcal{K} \nVdash \lnot\lnot P \to P$, showing both are not theorems of IPL.

---

I find it interesting that perhaps the two most famous classical tautologies which fail in IPL ($P \lor \neg P$ and $\lnot\lnot P \to P$) are both disprovable in such a small Kripke model. This leads to the following definition.

Given a formula $F$ which is not a theorem of IPL, let the Kripke rank of $F$, $\mathrm{krk}(F)$ be the size of the smallest Kripke model $\mathcal{K} \nVdash F$. Some simple observations:

• $\mathrm{krk}(F) = 1$ iff $F$ is not a theorem of classical logic.
• $\mathrm{krk}(P \lor \neg P) = \mathrm{krk}(\lnot\lnot P \to P) = 2$.

My (very broad) question is:

What are the possible values for $\mathrm{krk}(F)$?

I know a complete answer to this question is probably too much to expect, but here are some particularly relevant subquestions:

• Are finite values $> 2$ possible?
• Are arbitrarily large finite values possible?
• Is every finite value possible?
• Is there any possible infinite value (e.g. $\omega$)?
• What about any/arbitrarily large cardinal values?

---

Aside: you can also do this all for intuitionistic first-order logic (IFOL), by defining a Kripke model for IFOL as a functor from a preorder $(W,\leq)$ to the category of $\mathcal{L}$-structures and model-theoretic embeddings. I'm also interested in answers to the general question in this setting: is it any different from the IPL case?

Answer 1

The finite model property of intuitionistic logic implies that every unprovable formula has finite rank. On the other hand, all positive integers are ranks of some formulas; there are many families of formulas one could use to show this, but for example, the formulas $$\bigvee_{i=0}^n\Bigl(\bigwedge_{j<i}p_j\to p_i\Bigr)$$ have rank $n+1$ (any countermodel has size at least $n+1$ as nodes witnessing the failure of each of the disjuncts have to be pairwise distinct).

For first-order logic, infinite rank is also possible (e.g., take the double-negation shift formula $\forall x\,\neg\neg P(x)\to\neg\neg\forall x\,P(x)$). Uncountable ranks are impossible, as any unprovable formula has a countable countermodel.