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](https://en.wikipedia.org/wiki/Kripke_semantics#Semantics_of_intuitionistic_logic). 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?



Possible values of "Kripke rank" for formulae in IPL
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.


