Argthtjtr

For $kinmathbb{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 $kgeq 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 $negneg 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?

$leteqleftrightarrow$Notice that $psi(A)=u$ iff $vdash_mathrm{CPC}Aeq u$ iff $vdash_mathrm{IPC}negneg(Aeq u)$. (I will write just $vdash$ for $vdash_mathrm{IPC}$.) Thus:

• $bot$ has a one-element fiber consisting of $bot$: if $vdashnegneg(Aeqbot)$, then $vdashneg A$.




• For each $i$, $u_i:=p_ilandbigwedge_{jne i}neg p_j$ has a two-element fiber consisting of $p_ilandbigwedge_{jne i}neg p_j$ and $negneg p_ilandbigwedge_{jne i}neg p_j$: if $vdashnegneg(Aeq u_i)$, then $vdash Atoneg p_j$ for all $jne i$, thus $A$ is equivalent to $bigwedge_{jne i}neg p_jland 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 $negneg p_i$, hence by your analysis of the Rieger–Nishimura lattice, it must be equivalent to $negneg p_i$ or to $p_i$. (It can’t be $bot$.)




• Likewise, $u=bigwedge_ineg p_i$ has a one-element fibre consisting of $bigwedge_ineg p_i$.

In the remaining cases, the fiber is infinite:

• If $u=bigwedge_{iin I}p_ilandbigwedge_{inotin I}neg p_i$ where $|I|ge2$, fix $jne k$ in $I$. Then the fiber of $u$ includes all formulas of the form $$bigwedge_{substack{iin I\ine j,k}}p_ilandbigwedge_{inotin I}neg p_iland A(p_j,p_k),$$
  where $A(p_j,p_k)$ is a formula of two variables implying $negneg(p_jland p_k)$ and implied by $p_jland 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}nevarnothing$, hence we may fix $jin I_{0,1}$. Then $psi^{-1}(u)$ includes all formulas of the form
  $$negneg uland A(p_j)$$
  where $A$ is a formula in one variable such that $vdashnegneg A(p_j)$. All these formulas are inequivalent: if
  $$vdashnegneg uland A(p_j)to A'(p_j),$$
  we may substitute $bot$ for all $p_i$ such that $iin I_{0,0}$, $top$ for $iin I_{1,1}$, $p_j$ for $iin I_{0,1}$, and $neg p_j$ for $iin I_{1,0}$. This substitution turns $negneg u$ into a theorem, and leaves $A$ and $A'$ unaffected, hence
  $$vdash A(p_j)to A'(p_j).$$