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?