Fibers of the morphism from the free Heyting algebra to the free Boolean algebra For $k\in\mathbb{N}$, let $H_k$ be the free Heyting algebra on $k$ variables $p_1,\ldots,p_k$ and $B_k$ be the free Boolean algebra on the same $k$ variables.  Thus, $B_k$ has $2^{2^k}$ elements (corresponding to all possible truth-value tables with $k$ entries), while $H_k$ is infinite as soon as $k\geq 1$.
Since Boolean algebras are, in particular, Heyting algebras, there is a natural morphism $\psi \colon H_k \to B_k$ (taking each $p_i$ to the corresponding Boolean variable).
Example: For $k=1$ (and writing $p:=p_1$), the algebra $H_1$ is the (infinite) Rieger-Nishimura lattice (see here), while $B_1$ has four elements namely $\bot,p,\neg p,\top$.  The morphism $\psi$ takes the single element $\bot$ to $\bot$, the two $p$ and $\neg\neg p$ to $p$, the single $\neg p$ to $\neg p$, and every other element of $H_1$ to $\top$.  So three of its fibers are finite while the last is infinite.

Question: Which elements $u \in B_k$ have finite fiber $\psi^{-1}(u)$, and how can we describe their cardinalities or, better, their elements?

 A: $\let\eq\leftrightarrow$Notice that $\psi(A)=u$ iff $\vdash_\mathrm{CPC}A\eq u$ iff $\vdash_\mathrm{IPC}\neg\neg(A\eq u)$. (I will write just $\vdash$ for $\vdash_\mathrm{IPC}$.) Thus:


*

*$\bot$ has a one-element fiber consisting of $\bot$: if $\vdash\neg\neg(A\eq\bot)$, then $\vdash\neg A$.

*For each $i$, $u_i:=p_i\land\bigwedge_{j\ne i}\neg p_j$ has a two-element fiber consisting of $p_i\land\bigwedge_{j\ne i}\neg p_j$ and $\neg\neg p_i\land\bigwedge_{j\ne i}\neg p_j$: if $\vdash\neg\neg(A\eq u_i)$, then $\vdash A\to\neg p_j$ for all $j\ne i$, thus $A$ is equivalent to $\bigwedge_{j\ne i}\neg p_j\land A(\bot,\dots,\bot,p_i,\bot,\dots)$. The formula $A':=A(\bot,\dots,\bot,p_i,\bot,\dots)$ of one variable also has to imply $\neg\neg p_i$, hence by your analysis of the Rieger–Nishimura lattice, it must be equivalent to $\neg\neg p_i$ or to $p_i$. (It can’t be $\bot$.)

*Likewise, $u=\bigwedge_i\neg p_i$ has a one-element fibre consisting of $\bigwedge_i\neg p_i$.
In the remaining cases, the fiber is infinite:


*

*If $u=\bigwedge_{i\in I}p_i\land\bigwedge_{i\notin I}\neg p_i$ where $|I|\ge2$, fix $j\ne k$ in $I$. Then the fiber of $u$ includes all formulas of the form $$\bigwedge_{\substack{i\in I\\i\ne j,k}}p_i\land\bigwedge_{i\notin I}\neg p_i\land A(p_j,p_k),$$
where $A(p_j,p_k)$ is a formula of two variables implying $\neg\neg(p_j\land p_k)$ and implied by $p_j\land p_k$. That there are infinitely many such formulas follows from the fact that in the universal intuitionistic frame of rank $2$, there are infinitely many points such that the only leaf they see is the one satisfying both variables.

*If $u$ has $\ge2$ satisfying assignments $e,e'$, let $I_{a,b}$, $a,b=0,1$, be the set of indices of variables assigned to $a$ by $e$, and to $b$ by $e'$. Without loss of generality, $I_{0,1}\ne\varnothing$, hence we may fix $j\in I_{0,1}$. Then $\psi^{-1}(u)$ includes all formulas of the form
$$\neg\neg u\land A(p_j)$$
where $A$ is a formula in one variable such that $\vdash\neg\neg A(p_j)$. All these formulas are inequivalent: if
$$\vdash\neg\neg u\land A(p_j)\to A'(p_j),$$
we may substitute $\bot$ for all $p_i$ such that $i\in I_{0,0}$, $\top$ for $i\in I_{1,1}$, $p_j$ for $i\in I_{0,1}$, and $\neg p_j$ for $i\in I_{1,0}$. This substitution turns $\neg\neg u$ into a theorem, and leaves $A$ and $A'$ unaffected, hence
$$\vdash A(p_j)\to A'(p_j).$$
