On page 230 of An abstract notion of realizability ..., Läuchli 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 Läuchli'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]\}$.
By "proof assignment for $A$," I mean a set of the form $p[A]$ for some proof assignment $p$. Let $\mathbb{P}(A)$ be the set of proof assignments for $A$; Lauchli's intermediate logic, then, is $\{A: \bigcap \mathbb{P}(A)\not=\emptyset\}$.
