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)](https://commons.wikimedia.org/wiki/File:Rieger-Nishimura.svg), 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?
> 
> 
> 



Fibers of the morphism from the free Heyting algebra to the free Boolean algebra
$\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).$$


