Summary: We study embeddings of Heyting algebras \((Ha\)’s). It is pointed out that such embeddings are naturally connected with Derived Rules and with propositional theories. We consider the \(Ha\)’s embeddable in the \(Ha\) of the Intuitionistic Propositional Calculus (IPC), i.e. the free \(Ha\) on \(\aleph_0\) generators, those embeddable in the \(Ha\) of Heyting Arithmetic (HA) and those embeddable in the \(Ha\) of \(\text{HA}^*\), a ‘natural’ extension of HA. We prove the following theorems. The same \(Ha\)’s on finitely many generators are embeddable in the \(Ha\) of IPC and in the \(Ha\) of Boolean (or: Brouwerian) combinations of \(\Sigma\)-sentences of HA. The \(Ha\)’s on finitely many generators embeddable in the \(Ha\) of IPC are finitely presented. There is a non-recursive \(Ha\) on three generators that can be embedded in the \(Ha\) of HA. Every recursively enumerable prime \(Ha\) is embeddable in the \(Ha\) of \(\text{HA}^*\).
For the entire collection see [Zbl 0851.00045].