On page 230 of An abstract notion of realizability ..., Lauchli writes the following:

If we drop the restrictions put on $\Theta$, then we get classical logic in one case and an intermediate thing in the other: [...] the condition $\exists\Theta\forall p$ holds for some intuitionistically valid formulas, e.g. for $$\forall v(R(v)\vee Q)\rightarrow (\forall vR(v)\vee Q),$$ but not for all classically valid ones, e.g. not for $Q\vee\neg Q$.

I'm curious whether this "intermediate thing" - the set of formulas $A$ such that the intersection of all possible "proof assignment sets" $p[A]$ is nonempty (but not requiring that intersection to have an easily-definable or substitution-invariant member) - is more completely understood. Since Lauchli's paper is hard to get a copy of, I've given a sketch of the definition below.

---

Fix countable disjoint sets $\Pi,\Gamma$; we'll think of these as consisting of possible proofs of atomic facts and names of possible elements of the universe, respectively. To each formula $A$ (not necessarilyl closed) we associate a set $S(A)$ of "possible proofs" of $A$ as follows:

• $S(A)=\Pi$ if $A$ is atomic.

• $\wedge$ and $\vee$ correspond to product and disjoint union respectively.

• $S(A\rightarrow B)=S(B)^{S(A)}$.

• $S(\forall vA)=S(A)^\Gamma$ and $S(\exists vA)=\Gamma\times S(A)$.

Next, a proof assignment is a function $p$ assigning to each closed formula $A$ a set $p[A]\subseteq S(A)$ satisfying a few rules, namely:

• $p[\perp]\subseteq p[A]\subseteq\Pi$ if $A$ is atomic,

• $\wedge$ and $\vee$ correspond to product and disjoint union as before,

• $p[A\rightarrow B]=\{f\in S(A\rightarrow B): \forall g\in p[A](f(g)\in p[B])\}$ as expected, and

• $p[\forall vA]=\{f\in S(\forall v A): \forall c\in \Gamma(f(c)\in p[A^v_c])\}$ and similarly $p[\exists v A]=\{\langle c,x\rangle: c\in\Gamma\wedge x\in p[A^v_c]\}$.