# Possible values of "Kripke rank" for formulae in IPL

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$$.

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?

• My guess is that the Kreisel-Putnam axiom (eg mathoverflow.net/a/160067/44143) and the formulas in the Rieger-Nishimura lattice, or variants of them, will require arbitrarily high ranks. Oct 25 '21 at 15:11

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 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.