---
abstract: 'The paper is devoted to an algebraic interpretation of Kuznetsov’s theorem which establishes the assertoric equipollence of intuitionistic and proof-intuitionistic propositional calculi.  Given a Heyting algebra, we define an enrichable Heyting algebra, in which the former algebra is embedded.  Moreover, we show that both algebras generate one and the same variety of Heyting algebras.  This algebraic result is equivalent to the Kuznetsov theorem.  The proposed construction of the enrichable “counterpart” of a given Heyting algebra allows one to observe that some properties of the original algebra are preserved by this embedding in the counterpart algebra.' 
address: |
    Louisiana Scholars’ College\
    Northwestern State University\
    Natchitoches, U.S.A.
author:
- Alexei Muravitsky
title: On one embedding of Heyting algebras
---

The history of one question
===========================

The present paper is about an algebraic interpretation of the main theorem of [@kuz85b] by Alexander Kuznetsov.  This theorem reads: $${\mbox{\textbf{Int}}}+ A\vdash B ~\Longleftrightarrow ~{\mbox{\textbf{KM}}}+ A\vdash
B, \tag{\emph{Kuznetsov's Theorem}}$$ where ${\mbox{\textbf{Int}}}$ and ${\mbox{\textbf{KM}}}$ are intuitionistic propositional calculus and proof-intuitionistic calculus, respectively, and $A$ and $B$ are assertoric (i.e. modality-free) propositional formulas.  This might seem not very impressive, if we would not know that Kuznetsov’s Theorem was one of the two key properties which helped establish [@km86] that the lattices of the normal extensions of ${\mbox{\textbf{Grz}}}$ (Grzegorczyk logic), of ${\mbox{\textbf{GL}}}$ (provability logic) and of the aforementioned logics ${\mbox{\textbf{Int}}}$ and ${\mbox{\textbf{KM}}}$ are connected by the following commutative diagram: $$\xymatrix{
    \text{NE}{\mbox{\textbf{KM}}}\ar@<1ex>[r]^\tau \ar@<1ex>[r];[]^\rho
    \ar[d]_{\lambda} &\text{NE}{\mbox{\textbf{GL}}}\ar[d]^{\mu}\\
    \text{NE}{\mbox{\textbf{Int}}}\ar@<1ex>[r]^\sigma  \ar@<1ex>[r];[]^{\sigma^{-1}} &\text{NE}{\mbox{\textbf{Grz}}}}$$ where $\tau$ and $\rho$ are lattice isomorphisms and inverses of one another,[^1] $\lambda$ and $\mu$ are meet epimorphisms[^2] and $\sigma$ denotes the Blok-Esakia isomorphism.  Kuznetsov’s Theorem is responsible for $\lambda$ to be a meet epimorphism which makes the above diagram commute.  If one seeks to find a relationship between modal propositional systems on classical and intuitionistic bases, a diagram like that, we believe, gives a right view.[^3]

Syntactic background {#S:syntactic}
--------------------

We will, at first, be dealing with *formulas* (alias *terms*) of two propositional languages, ${\mbox{$\mathcal{L}_{a}$}}$ and ${\mbox{$\mathcal{L}$}}_{\square}$. The language ${\mbox{$\mathcal{L}_{a}$}}$ is grounded on a denumerable set ${\textbf{\textit{Var}}}$ of propositional variables and the logical constants: $\wedge,\vee,{\rightarrow}$ and $\neg$. Unspecified ${\mbox{$\mathcal{L}_{a}$}}$-formulas will be denoted by $A,~B,\ldots$ We obtain ${\mbox{$\mathcal{L}$}}_{\square}$ by adding modality $\square$ to the logical constants of ${\mbox{$\mathcal{L}_{a}$}}$. Regarding the sets of ${\mbox{$\mathcal{L}_{a}$}}$- and ${\mbox{$\mathcal{L}$}}_{\square}$-formulas as algebras, we obtain the formula algebras ${\mathfrak{F}}_a$ and ${\mathfrak{F}}_{\square}$, respectively.  In Section \[S:localization-proof-theoretic\], we will introduce two more extensions of ${\mbox{$\mathcal{L}_{a}$}}$. Let ${\mbox{$\mathcal{L}$}}$ be a propositional language which is an extension (not necessarily proper) of ${\mbox{$\mathcal{L}_{a}$}}$. A homomorphism of a formula algebra ${\mathfrak{F}}_{\mathcal{L}}$ into ${\mathfrak{F}}_{\mathcal{L}}$ is called a *substitution*.  Metavariables for ${\mbox{$\mathcal{L}$}}$-formulas (or ${\mbox{$\mathcal{L}$}}$-terms) are $\alpha, \beta,\ldots$. As usual, we denote: $$\alpha\leftrightarrow\beta:=(\alpha\rightarrow\beta)\wedge(\beta\rightarrow\alpha).$$

Now ${\mbox{\textbf{Int}}}$ can be defined as an ${\mbox{$\mathcal{L}_{a}$}}$-system given by any suitable axioms for intuitionistic propositional logic (see, e.g., [@church1956], [§]{} 26) and two inference rules, (uniform) substitution and modus ponens.  ${\mbox{\textbf{KM}}}$ is defined as an ${\mbox{$\mathcal{L}$}}_{\square}$-system by the axioms and inference rules of ${\mbox{\textbf{Int}}}$ plus the following three formulas: $$\label{E:KM-axioms}
p{\rightarrow}\square p, ~~~(\square p{\rightarrow}p){\rightarrow}p, ~~~\square p{\rightarrow}(q\vee(q{\rightarrow}p)),$$ where $p$ and $q$ are two distinct variables of ${\textbf{\textit{Var}}}$.[^4]

Semantic background
-------------------

We assume that the reader is familiar with the notion of Heyting algebra and with the basic properties of those algebras. ( See, e.g., [@rs70], where those algebras are call pseudo-Boolean.) 

\[D:KM-algebra\] An algebra ${\mbox{$\mathfrak{A}$}}=\langle{\mbox{$\mathcal{A}$}},\wedge,\vee,{\rightarrow},\square,{\boldsymbol{0}},{\boldsymbol{1}}\rangle$ is said to be a [*${\mbox{\textbf{KM}}}$*]{}-algebra if $\langle{\mbox{$\mathcal{A}$}},\wedge,\vee,{\rightarrow},{\boldsymbol{0}},{\boldsymbol{1}}\rangle$ is a Heyting algebra (the **Heyting reduct** of ${\mbox{$\mathfrak{A}$}}$), with a least and greatest elements ${\boldsymbol{0}}$ (the zero) and ${\boldsymbol{1}}$ (the unit), respectively, and the unary operation $\square$ satisfies the following conditions: [*$$\begin{array}{cl}
    (\text{a}) & x\le \square x,\\
    (\text{b}) & \square x{\rightarrow}x\le x,\\
    (\text{c}) & \square x\le y\vee(y{\rightarrow}x). 
    \end{array}$$*]{} The universe ${\mbox{$\mathcal{A}$}}$ will often be denoted by $|{\mbox{$\mathfrak{A}$}}|$.

As was noted in [@mur90], if ${\mbox{$\mathfrak{A}$}}$ is a ${\mbox{\textbf{KM}}}$-algebra, the operation $\square$ is defined in ${\mbox{$\mathfrak{A}$}}$ uniquely.  This gives rise to the following definition. 

\[D:enrichable\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra and $a,b\in|{\mbox{$\mathfrak{A}$}}|$. We say that $b$ enriches $a$ or $a$ is enriched with $b$ if the following conditions are satisfied in ${\mbox{$\mathfrak{A}$}}$: [*$$\begin{array}{cl}
    (\text{a}) & a\le b,\\
    (\text{b}) & b{\rightarrow}a=a,\\
    (\text{c}) & b\le x\vee(x{\rightarrow}a),~\textit{for any $x\in|{\mbox{$\mathfrak{A}$}}|$}. 
    \end{array}$$*]{} A Heyting algebra is called enrichable if every element of this algebra is enrichable. 

\[P:unique\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra and $a\in|{\mbox{$\mathfrak{A}$}}|$. If $a$ is enrichable in ${\mbox{$\mathfrak{A}$}}$, it can be enriched with only one element. 

For contradiction, we suppose that elements $b$ and $b^\prime$ enrich $a$, that is the properties ()–() of Definition \[D:enrichable\] are true for $b$ and $b^\prime$. Then we obtain: $$b\leq b^{\prime}{\vee}(b^{\prime}{\rightarrow}a)=b^{\prime}{\vee}a=b^{\prime}.$$

Similarly, we get $b^{\prime}\leq b$.

The next observation uses the notion of a dense element of Heyting algebra; see definition, e.g., in [@rs70], chapter IV, [§]{} 5. 

\[P:negation\] If $a$ is enriched in with $b$, then the latter is dense; that is $\neg b={\boldsymbol{0}}$.

Indeed, $$\begin{array}{rl}
    \neg b\leq b{\rightarrow}a & \Leftrightarrow \neg b\leq a\\
    & \Rightarrow \neg b\leq b\\
    & \Leftrightarrow \neg b\leq{\boldsymbol{0}}. 
    \end{array}$$

We note that not all Heyting algebras are enrichable.  For instance, the least element of a chain of type $1+\omega^{\ast}$ is not enrichable.  However, every finite Heyting algebra is enrichable; cf.  [@mur14a], Proposition 15.  Thus any variety of Heyting algebras contains enrichable members. 

It follows directly from Kuznetsov’s Theorem that any variety of Heyting algebras is generated by those algebras in it that are enrichable. ( Cf.  [@kuz85b], Corollary 1.)  In fact, the last statement is equivalent to Kuznetsov’s Theorem.[^5] However, Kuznetsov states another equivalent of his Theorem:

> Every Heyting algebra ${\mbox{$\mathfrak{A}$}}$ is a subalgebra (up to isomorphism) of some enrichable Heyting algebra in the variety generated by ${\mbox{$\mathfrak{A}$}}$.\
> (Cf.  [@kuz85b], Corollary 2.\[Kuznetsov’s-Corollary-2\])

The last observation was pointed out to Kuznetsov by the author and its proof can be found, e.g., in [@mur08], Remark 3.  Thus, according to this observation, for any Heyting algebra ${\mbox{$\mathfrak{A}$}}$, there is an enrichable Heyting algebra ${\mbox{$\mathfrak{B}$}}$ such that

  ----- --------------------------------------------------------------------------------------------
   (A)  ${\mbox{$\mathfrak{A}$}}$ is embedded into ${\mbox{$\mathfrak{B}$}}$ and
   (B)  ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ generate one and the same variety. 
  ----- --------------------------------------------------------------------------------------------

What do we know about ${\mbox{$\mathfrak{B}$}}$, besides its existence?  According to Remark 3 of [@mur08], if $K$ is the class of all enrichable algebras of the variety generated by ${\mbox{$\mathfrak{A}$}}$, then ${\mbox{$\mathfrak{A}$}}\in{\mathbf{S}}{\mathbf{H}}{\mathbf{P}}(K)$. Grounding only on the last membership, that is, not having any transparent algebraic construction of ${\mbox{$\mathfrak{B}$}}$, it is hardly possible to answer some natural questions about properties which can be preserved in ${\mbox{$\mathfrak{B}$}}$. For instance, grounding only on this membership, we do not know whether ${\mbox{$\mathfrak{B}$}}$ can be countable, providing that ${\mbox{$\mathfrak{A}$}}$ is; or whether ${\mbox{$\mathfrak{B}$}}$ can be subdirectly irreducible, if ${\mbox{$\mathfrak{A}$}}$ is. 

In the remaining part of the paper, we show, given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, how to define such ${\mbox{$\mathfrak{B}$}}$ that the properties ()–() are fulfilled.  In fact, one possible candidate for ${\mbox{$\mathfrak{B}$}}$ has already been proposed in [@mur86], where we constructed algebra ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ (see definition in Section \[S:algebraLimitA\]) which possesses the property (A).[^6]\
Let ${\mbox{$\mathcal{L}$}}$ be an extension of ${\mbox{$\mathcal{L}_{a}$}}$. Given ${\mbox{$\mathcal{L}$}}$-algebras and , we write $${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$$ if is a subalgebra (up to isomorphism) of . 

We conclude this section with the following definition. 

Let ${\mbox{$\mathcal{L}$}}$ be a propositional language which is an extension of ${\mbox{$\mathcal{L}_{a}$}}$ and ${\mbox{$\mathfrak{A}$}}$ be an ${\mbox{$\mathcal{L}$}}$-expansion of Heyting algebra.  Any homomorphism $v:{\mathfrak{F}}_{\mathcal{L}}{\rightarrow}{\mbox{$\mathfrak{A}$}}$ is called a valuation (in ${\mbox{$\mathfrak{A}$}}$).  The logic of algebra ${\mbox{$\mathfrak{A}$}}$ is the set $$L({\mbox{$\mathfrak{A}$}})={\{A\in{\mathfrak{F}}_{\mathcal{L}} ~|~v(A)={\boldsymbol{1}},~\text{for any valuation $v$ in ${\mbox{$\mathfrak{A}$}}$}\}}.$$

Given a language ${\mbox{$\mathcal{L}$}}$, an ${\mbox{$\mathcal{L}$}}$-algebra ${\mbox{$\mathfrak{A}$}}$ and any nonempty set $\Gamma$ of ${\mbox{$\mathcal{L}$}}$-formulas, we denote $${\mbox{$\mathfrak{A}$}}\models\Gamma$$ if $\Gamma{\subseteq}L({\mbox{$\mathfrak{A}$}})$. And if $A$ is an ${\mbox{$\mathcal{L}$}}$-formula, we write $$\Gamma\not\models A,$$ if there is an ${\mbox{$\mathcal{L}$}}$-algebra ${\mbox{$\mathfrak{A}$}}$ such that ${\mbox{$\mathfrak{A}$}}\models\Gamma$ and ${\mbox{$\mathfrak{A}$}}\not\models A$.  Finally, we use $$\Gamma\models A$$ in the usual sense: $${\mbox{$\mathfrak{A}$}}\models\Gamma\Longrightarrow{\mbox{$\mathfrak{A}$}}\models A.$$

The structure of the present paper
----------------------------------

In Section \[S:algebraLimitA\], given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, we define an algebra ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ which will play in the sequel the role of ${\mbox{$\mathfrak{B}$}}$ in the above conditions (A) and (B).  We show (referring chiefly to [@mur86]) that ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ satisfies (A).  Also, we demonstrate some preservation properties over transition from ${\mbox{$\mathfrak{A}$}}$ to ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ and state the main theorem (Theorem \[T:main-theorem\]).  In Section \[S:reducibility\], we find a sufficient condition (Corollary \[C:reducibility-4\]) for the main theorem.  This leads us to the idea of *one-element enrichment*.  In Section \[S:localization-algebraic\] we develop an algebraic view on one-element enrichment and in Section \[S:localization-proof-theoretic-0\] a proof-theoretic view on it.  In Section \[S:connecting-viewpoints\] we connect these viewpoints; in the end of that section we explain what remains to be done to complete the proof of the main theorem.  We are taking a decisive step in our proof in Section \[S:Stone-embedding-properties-main\].  In Section \[S:completing-proof\] we make a final effort to complete the proof of Theorem \[T:main-theorem\].  Thus, as the reader can see, this paper is devoted to the proof of one theorem.  In Section \[S:conclusion\] we formulate open questions about properties which ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ may have, providing that ${\mbox{$\mathfrak{A}$}}$ possesses them. 

Algebra ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ {#S:algebraLimitA}
=====================================================================

In this paper we deal mostly with Heyting algebras or algebras whose assertoric reduct is a Heyting algebra.  When confusion is unlikely, the word “Heyting” will often be omitted.  The following algebraic notions and facts will be presupposed.  The main references in this section are [@rs70], [@gra79], [@gor98], and [@mur86].  We start with the following notions and notations. 

-   Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$ and $X\subseteq|{\mbox{$\mathfrak{A}$}}|$, we denote by $[X)_{\mathfrak{A}}$ the filter of ${\mbox{$\mathfrak{A}$}}$ generated by the set $X$; it is well know that $[X)_{\mathfrak{A}}={\{x ~|~y\le x,~\text{for some $y\in X$}\}}$.

-   Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, ${\mathcal{S}_{\mathfrak{A}}}$ denotes both the set of all prime filters of ${\mbox{$\mathfrak{A}$}}$ and the poset $({\mathcal{S}_{\mathfrak{A}}},{\subseteq})$.[^7] The filters of an algebra ${\mbox{$\mathfrak{A}$}}$ are called ${\mbox{$\mathfrak{A}$}}$-***filters***. 

-   Given an algebra ${\mbox{$\mathfrak{A}$}}$, ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ is the (Heyting) algebra of all upward sets of ${\mathcal{S}_{\mathfrak{A}}}$. It is well known that the signature operations of ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ are defined as follows: $$\begin{array}{l}
        X{\wedge}Y=X\cap Y,\\
        X{\vee}Y=X\cup Y,\\
        X{\rightarrow}Y={\{F\in{\mathcal{S}_{\mathfrak{A}}}~|~\forall F^{\prime}\in{\mathcal{S}_{\mathfrak{A}}}.~(F{\subseteq}F^{\prime}\&F^{\prime}\in X){\Rightarrow}F^{\prime}\in Y\}},\\
        \neg X=X{\rightarrow}\emptyset,\\
        {\boldsymbol{0}}=\emptyset~\text{and}~{\boldsymbol{1}}={\mathcal{S}_{\mathfrak{A}}}. 
        \end{array}$$

-   Given an algebra ${\mbox{$\mathfrak{A}$}}$, the Stone embedding $h_{\mathfrak{A}}: {\mbox{$\mathfrak{A}$}}{\rightarrow}{\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ is defined as follows: $h_{\mathfrak{A}}(x)={\{F\in{\mathcal{S}_{\mathfrak{A}}}~|~x\in F\}}$. The isomorphic image of ${\mbox{$\mathfrak{A}$}}$ w.r.t.  $h_{\mathfrak{A}}$ is denoted by $h_{\mathfrak{A}}[{\mbox{$\mathfrak{A}$}}]$. Thus $h_{\mathfrak{A}}[{\mbox{$\mathfrak{A}$}}]{\preccurlyeq}{\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$. Also, we denote $$h_{\mathfrak{A}}(\overline{x})={\{F\in{\mathcal{S}_{\mathfrak{A}}}~|~x\not\in F\}},$$ for any $x\in|{\mbox{$\mathfrak{A}$}}|$. Further, we will find the usefulness of the set $$\max{h_{\mathfrak{A}}(\overline{x})},$$ which consists of the maximal elements, if any, of the set ${h_{\mathfrak{A}}(\overline{x})}$.\

Now we will outline an algebraic construction defined in [@mur86], §1. 

We start with the definition of operation $\de$  in ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$: $${\deltaX}={\{F\in{\mathcal{S}_{\mathfrak{A}}}~|~(\forall F^{\prime}\in{\mathcal{S}_{\mathfrak{A}}})(F\subset
    F^{\prime}{\Rightarrow}F^{\prime}\in X)\}}.$$ In particular, for any particular $a\in{\mbox{$\mathfrak{A}$}}$, $$\label{E:delta-for-element}
{\delta{h_{\mathfrak{A}}(a)}}={\{F\in{\mathcal{S}_{\mathfrak{A}}}~|~(\forall F^{\prime}\in{\mathcal{S}_{\mathfrak{A}}})(F\subset
    F^{\prime}{\Rightarrow}a\in F^{\prime})\}}.$$

In the sequel, we will need the following two observations. 

\[P:delta-h(x)-1\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra.  For any $x\in|{\mbox{$\mathfrak{A}$}}|$, ${\delta{h_{\mathfrak{A}}(x)}}={h_{\mathfrak{A}}(x)}\cup\max{h_{\mathfrak{A}}(\overline{x})}$.

\[P:delta-h(x)-2\] For any $x\in|{\mbox{$\mathfrak{A}$}}|$, the element $h_{\mathfrak{A}}(x)$ is enriched in [*${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$*]{} with the element ${\deltah_{\mathfrak{A}}(x)}$. Moreover, if an element $a\in|{\mbox{$\mathfrak{A}$}}|$ is enriched in with an element ${\mbox{$a^{\ast}$}}$, then ${\deltah_{\mathfrak{A}}(a)}=h({\mbox{$a^{\ast}$}})$.

We will be using the following notation: $$h_{\mathfrak{A}}({\mbox{$\mathfrak{A}$}})={\{h_{\mathfrak{A}}(x) ~|~x\in|{\mbox{$\mathfrak{A}$}}|\}}
~\text{and}~\Delta_{\mathfrak{A}}={\{{\deltah_{\mathfrak{A}}(x)} ~|~x\in|{\mbox{$\mathfrak{A}$}}|\}}.$$ Then, we denote by ${\mbox{$\delta[{\mbox{$\mathfrak{A}$}}]$}}$ the subalgebra of ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ generated by $h_{\mathfrak{A}}({\mbox{$\mathfrak{A}$}})\cup\Delta_{\mathfrak{A}}$.\
Next, given an algebra , we define a denumerable sequence of algebras as follows: $$\begin{array}{l}
{\mbox{$\mathfrak{A}$}}_{0}={\mbox{$\mathfrak{A}$}},\\
{\mbox{$\mathfrak{A}$}}_{i+1}={\mbox{$\delta[{\mbox{$\mathfrak{A}$}}_{i}]$}}\quad (i<{\mbox{$\omega$}}).\\
\end{array}$$

Along with the sequence $\{{\mbox{$\mathfrak{A}$}}_{i}\}_{i<{\mbox{$\omega$}}}$, we also have the embeddings: $$\begin{array}{l}
\varphi_{ii}:{\mbox{$\mathfrak{A}$}}_{i}{\rightarrow}{\mbox{$\mathfrak{A}$}}_{i}, i<{\mbox{$\omega$}},\quad\text{(the identity
    embedding
    on ${\mbox{$\mathfrak{A}$}}_{i}$)}\\
\varphi_{i(i+1)}:{\mbox{$\mathfrak{A}$}}_{i}{\rightarrow}{\mbox{$\mathfrak{A}$}}_{i+1},i<{\mbox{$\omega$}},\quad\text{(Stone
    embedding
    $h_{\mathfrak{A}_i}:{\mbox{$\mathfrak{A}$}}_{i}{\rightarrow}{\mbox{$\delta[{\mbox{$\mathfrak{A}$}}_{i}]$}}$)}\\
\varphi_{ij}=\varphi_{i(i+1)}\circ\varphi_{(i+1)(i+2)}\circ\ldots\circ\varphi_{(j-1)j},
\text{ where $i<j$}. 
\end{array}$$

Thus the sequence $\{{\mbox{$\mathfrak{A}$}}_{i}\}_{i<{\mbox{$\omega$}}}$ along with the embeddings $\varphi_{ij}$, $i\leq j$, form a direct family [@gra79].  Let be the direct limit of this family. 

We remind the reader that the carrier of consists of the equivalence classes on $\bigcup{\{{\mbox{$\mathcal{A}$}}_i ~|~i<{\mbox{$\omega$}}\}}$: $$|x|={\{y ~|~y\equiv x\}},$$ for any $x\in\bigcup{\{{\mbox{$\mathcal{A}$}}_i ~|~i<{\mbox{$\omega$}}\}}$. Here the equivalence $x\equiv y$, where $x\in{\mbox{$\mathcal{A}$}}_i$ and $y\in{\mbox{$\mathcal{A}$}}_j$, means that either $i\leq j$ and $\varphi_{ij}(x)=y$, or $i\geq j$ and $\varphi_{ji}(y)=x$.

Obviously, for any $x,y\in{\mbox{$\mathcal{A}$}}_i$, $$\label{E:equality}
|x|=|y|~\Longleftrightarrow~x=y.$$

Next we define: $$|x|\odot|y|=|\varphi_{ij}(x)\odot y|,$$ where $\odot\in\{{\wedge},{\vee},{\rightarrow}\}$, $x\in{\mbox{$\mathfrak{A}$}}_i$, $y\in{\mbox{$\mathfrak{A}$}}_j$, and $i\leq j$. (In case $j\leq i$, we define $|x|\odot|y|=|x\odot\varphi_{ji}(y)|$.)

Naturally, we also define: $$\neg|x|=|\neg x|.$$ (Cf.  [@gra79] or [@gor98].) 

Further, we define: For $x\in{\mbox{$\mathcal{A}$}}_i$ and $y\in{\mbox{$\mathcal{A}$}}_j$, $$|x|\leq|y|~\Longleftrightarrow~\text{either $i\le j$
and $\varphi_{ij}(x)\leq_j y$, or $j\le i$ and $x\le_i\varphi_{ji}(y)$},$$ where $\le_i$ and $\le_J$ are the lattice partial orderings in the algebras ${\mbox{$\mathfrak{A}$}}_i$ and ${\mbox{$\mathfrak{A}$}}_j$, respectively. 

It is easy to see that

$|x|\leq|y|$ *is the lattice partial order in* . 

If we denote the unit and zero of ${\mbox{$\mathfrak{A}$}}_i$ by ${\boldsymbol{1}}_i$ and ${\boldsymbol{0}}_i$, respectively, then

${\{{\boldsymbol{1}}_i ~|~i<{\mbox{$\omega$}}\}}$ *is the unit of*

and

${\{{\boldsymbol{0}}_i ~|~i<{\mbox{$\omega$}}\}}$ *is the zero of*

Indeed, it is obvious that ${\boldsymbol{1}}_i\equiv{\boldsymbol{1}}_j$ and ${\boldsymbol{0}}_i\equiv{\boldsymbol{0}}_j$. Thus $|{\boldsymbol{0}}_0|\leq|x|\leq|{\boldsymbol{1}}_0|$.

Since each ${\mbox{$\mathfrak{A}$}}_i$ is a Heyting algebra, we arrive at the first observation. 

is a Heyting algebra. 

*Proof* follows from the definition of and the fact that each $\varphi_{ij}$ is an embedding.  Also, we have to use (\[E:equality\]).[^8]\

\[P:A\_i-embedding\] Each ${\mbox{$\mathfrak{A}$}}_i$ is embedded into . 

It is clear that the map $$\varphi_i:x\mapsto|x|,$$ where $x\in{\mbox{$\mathfrak{A}$}}_i$ and $i<{\mbox{$\omega$}}$, is an embedding of ${\mbox{$\mathfrak{A}$}}_i$ into .  Indeed, $\varphi_i(x)=|{\boldsymbol{1}}_i|$ means $|x|=|{\boldsymbol{1}}_i|$. Then we apply (\[E:equality\]). 

Also, we observe the following. 

\[P:countable\] If  is countable, then is countable as well. 

Since each ${\mbox{$\mathfrak{A}$}}_i$ is countable, is also countable. 

\[P:sub-irr\] If is subdirectly irreducible, so are each ${\mbox{$\mathfrak{A}$}}_i$ and . 

Let ${\mbox{$\omega$}}$ be the pre-top element of .  Algebra ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ is subdirectly irreducible, for $h({\mbox{$\omega$}})$ is a pre-top element in it.  Therefore, ${\mbox{$\delta[{\mbox{$\mathfrak{A}$}}]$}}$ is subdirectly irreducible.  By induction, we conclude that each ${\mbox{$\mathfrak{A}$}}_i$ is subdirectly irreducible as well. 

To continue, we first observe that $\varphi_{0i}({\mbox{$\omega$}})$ is the pre-top element of ${\mbox{$\mathfrak{A}$}}_i$. We denote the latter element by ${\mbox{$\omega$}}_i$.

Next assume that $|{\mbox{$\omega$}}|\leq|x|$ and $x\in{\mbox{$\mathfrak{A}$}}_i$. Then $\varphi_{0i}({\mbox{$\omega$}})\leq x$, which implies that either $x=\varphi_{0i}({\mbox{$\omega$}})$ or $x={\boldsymbol{1}}_i$. Therefore, ${\{{\mbox{$\omega$}}_i ~|~i<{\mbox{$\omega$}}\}}$ is a pre-top element of . 

We want to show that is enrichable.  We will do it by employing the following lemma. 

\[L:1\] If an element $x\in|{\mbox{$\mathfrak{A}$}}_i|$ is enriched with an element $y\in|{\mbox{$\mathfrak{A}$}}_i|$, then $|x|$ is enriched with $|y|$ in . 

\[P:directA-enrichable\] Algebra is enrichable. 

Let $x\in|{\mbox{$\mathfrak{A}$}}_i|$. Then $h_{\mathfrak{A}_i}(x)$ is enriched with ${\deltah}_{\mathfrak{A}_i}(x)$ in ${\mbox{$\mathfrak{A}$}}_{i+1}$. It remains to apply Lemma \[L:1\]. 

In this paper we aim to prove the following theorem. 

\[T:main-theorem\] Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, the algebras ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ generate one and the same variety.  In other words, ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ determine one and the same equational theory, that is $L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}})$.

Reduction to one-element enrichment {#S:reducibility}
===================================

The sense of the term *one-element enrichment* should become clear at the end of this section. 

\[P:reducibility-1\] Given an algebra ${\mbox{$\mathfrak{A}$}}$, the following conditions are equivalent$:$ $$\begin{array}{cl}
(\emph{a}) &L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}});\\
(\emph{b}) &L({\mbox{$\mathfrak{A}$}}_i)=L({\mbox{$\mathfrak{A}$}}_{i+1}),~\text{for all $i\ge 0$}. 
\end{array}$$

Suppose (a) is true.  Since ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{A}$}}_i{\preccurlyeq}{\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$, we get (b).  Now assume that (b).  Then each ${\mbox{$\mathfrak{A}$}}_i$ generates one and the same variety.  By virtue of [@gor98], Theorem 1.2.9, ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ is a subalgebra of ultraproduct of some of ${\mbox{$\mathfrak{A}$}}_i$’s and hence generates the same variety. 

\[C:reducibility-2\] A sufficient condition for Theorem \[T:main-theorem\] is that for any Heyting algebra ${\mbox{$\mathfrak{A}$}}$, $L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\delta[{\mbox{$\mathfrak{A}$}}]$}})$.

Indeed, if $L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\delta[{\mbox{$\mathfrak{A}$}}]$}})$, for any algebra ${\mbox{$\mathfrak{A}$}}$, then starting from an algebra ${\mbox{$\mathfrak{A}$}}={\mbox{$\mathfrak{A}$}}_0$, we obtain the condition (b) of Proposition \[P:reducibility-1\]. 

In the sequel, we will be using the following notation. 

-   Given two sets $X$ and $Y$, $$X{\Subset}Y$$ denotes that $X$ is a finite subset of $Y$.

-   Let ${\mbox{$\mathfrak{A}$}}$ be an algebra and $X{\Subset}|{\mbox{$\mathfrak{A}$}}|$. We denote by ${\delta[{\mbox{$\mathfrak{A}$}}_X]}$ and by ${\delta[{\mbox{$\mathfrak{A}$}}_a]}$, if $X=\lbrace a\rbrace$, the subalgebra of ${\delta[{\mbox{$\mathfrak{A}$}}]}$ generated by $|h_{\mathfrak{A}}({\mbox{$\mathfrak{A}$}})|\cup{\{{\deltah_{\mathfrak{A}}(x)} ~|~x\in X\}}$.

\[P:reducubility-3\] Given an algebra ${\mbox{$\mathfrak{A}$}}$, if for any $X,Y{\Subset}|{\mbox{$\mathfrak{A}$}}|$, $L({\delta[{\mbox{$\mathfrak{A}$}}_X]})=L({\delta[{\mbox{$\mathfrak{A}$}}_Y]})$, then $L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\delta[{\mbox{$\mathfrak{A}$}}]$}})$ and, hence, $L({\mbox{$\mathfrak{A}$}})=L({\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}})$.

We notice that $\left({\delta[{\mbox{$\mathfrak{A}$}}_X]}\right)_{X\Subset|\mathfrak{A}|}$ along with identity maps is a directed family, the direct limit of which is ${\delta[{\mbox{$\mathfrak{A}$}}]}$.[^9] Thus, by virtue of [@gor98], Theorem 1.2.9, $L({\delta[{\mbox{$\mathfrak{A}$}}]})=L({\mbox{$\mathfrak{A}$}})$ (since ${\mbox{$\mathfrak{A}$}}={\delta[{\mbox{$\mathfrak{A}$}}_\emptyset]}$).  Then, we apply Corollary \[C:reducibility-2\]. 

\[C:reducibility-4\] A sufficient condition for Theorem \[T:main-theorem\] is that, given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, for any $a\in|{\mbox{$\mathfrak{A}$}}|$, $L({\mbox{$\mathfrak{A}$}})=L({\delta[{\mbox{$\mathfrak{A}$}}_a]})$.

Suppose for any algebra ${\mbox{$\mathfrak{A}$}}$ and any $a\in|{\mbox{$\mathfrak{A}$}}|$, $L({\mbox{$\mathfrak{A}$}})=L({\delta[{\mbox{$\mathfrak{A}$}}_a]})$. Let $a,b\in|{\mbox{$\mathfrak{A}$}}|$. By virtue of [@mur90], Lemma 5, the algebras ${\delta[{\mbox{$\mathfrak{A}$}}_{\lbrace a,b\rbrace}]}$ and ${\delta[{\delta[{\mbox{$\mathfrak{A}$}}_a]}_{h(b)}]}$ are isomorphic.  This implies that $L({\delta[{\mbox{$\mathfrak{A}$}}_a]})=L({\delta[{\mbox{$\mathfrak{A}$}}_{\lbrace a,b\rbrace}]})$. By induction, we conclude that for any $X{\Subset}|{\mbox{$\mathfrak{A}$}}|$, $L({\mbox{$\mathfrak{A}$}})=L({\delta[{\mbox{$\mathfrak{A}$}}_X]})$. It remains to apply Proposition \[P:reducubility-3\]. 

In the next section, we show that the enrichabilty of an element $a$ of an algebra ${\mbox{$\mathfrak{A}$}}$ is equivalent to the existence of a unary operation associated with $a$. Unlike the unary operation $\square$ of Definition \[D:KM-algebra\] which ensures the enrichabilty of all elements of algebra ${\mbox{$\mathfrak{A}$}}$, the new operation associated with $a$ guarantees the enrichabilty of just $a$. We call this treatment of one-element enrichment *algebraic*. 

One-element enrichment from an algebraic viewpoint {#S:localization-algebraic}
==================================================

In this section, we will treat each pair $(a,{\mbox{$a^{\ast}$}})$, where ${\mbox{$a^{\ast}$}}$ enriches $a$, as an element of a binary relation.  The main reference in this section is [@gra79], [§]{}13 and [§]{}28. 

Given an algebra and $a,{\mbox{$a^{\ast}$}}\in|{\mbox{$\mathfrak{A}$}}|$, $(a,{\mbox{$a^{\ast}$}})$ is an -pair $($in $)$ if $a$ is enriched with ${\mbox{$a^{\ast}$}}$ in .  Then, we define*:* $${\mbox{$\mathcal{E}$}}_{\mathfrak{A}}={\{(a,{\mbox{$a^{\ast}$}}) ~|~(a,{\mbox{$a^{\ast}$}})\mbox{ is an {\mbox{$\mathcal{E}$}}-pair in {\mbox{$\mathfrak{A}$}}}\}}.$$ We will drop the subscript ‘${\mbox{$\mathfrak{A}$}}$’ and write simply ‘${\mbox{$\mathcal{E}$}}$’ when confusion is unlikely. 

We note that for any Heyting algebra, its relation is never empty, for $({\boldsymbol{1}},{\boldsymbol{1}})$ is an -pair.  Also, if ${\mbox{$\omega$}}$ is the pre-top element of a subdirectly irreducible algebra, then $({\mbox{$\omega$}},{\boldsymbol{1}})$ is an -pair in this algebra. 

\[D:bn-negation\] A unary operation ${\mbox{$\sim$}}x$ in a Heyting algebra is called tilde-negation $($or $\sim$-negation for short$)$ if the following identities hold: [*$$\begin{array}{cl}
    (\text{a}) &x{\rightarrow}y\le {\mbox{$\sim$}}y{\rightarrow}{\mbox{$\sim$}}x;\\
    (\text{b}) &x{\wedge}{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{1}};\\
    (\text{c}) &{\mbox{$\sim$}}{\boldsymbol{0}}\le x{\vee}{\mbox{$\sim$}}x;\\
    (\text{d}) &{\mbox{$\sim$}}{\boldsymbol{0}}{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{1}},~\textit{or equivalently}~{\mbox{$\sim$}}{\boldsymbol{0}}{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}={\mbox{$\sim$}}{\boldsymbol{1}}. 
    \end{array}$$*]{} Sometimes, it will be convenient, instead of ${\mbox{$\sim$}}x$, to write $t(x)$ (perhaps with a subscript at ‘${\mbox{$\sim$}}$’ and ‘$t$’). 

It is obvious that in any Heyting algebra with ${\mbox{$\sim$}}$-negation, the following quasi-identity holds: $$\label{E:tilde-quasi-idenity}
x\le y \Longrightarrow {\mbox{$\sim$}}y\le{\mbox{$\sim$}}x.$$

Before we show how a -negation can be defined in a Heyting algebra, we will prove some properties of this operation. 

\[P:bn-properties\] The following properties hold in any Heyting algebra with -negation.  $$\begin{array}{cl}
    (\emph{a}) & {\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{0}};\\
    (\emph{b}) & {\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{1}};\\
    (\emph{c}) & {\mbox{$\sim$}}x{\vee}{\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{0}};\\
    (\emph{d}) & {\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}{\boldsymbol{1}};\\
    (\emph{e}) & {\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{1}}={\mbox{$\sim$}}{\boldsymbol{0}};\\
    (\emph{f}) & {\mbox{$\sim$}}x\leftrightarrow
    {\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{1}};\\
    (\emph{g}) & x{\wedge}{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\mbox{$\sim$}}x\le x{\vee}{\mbox{$\sim$}}x;\\
    (\emph{h}) &{\mbox{$\sim$}}{\boldsymbol{0}}\le x\Longrightarrow{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{1}};\\
    (\emph{i}) & {\mbox{$\sim$}}x=(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\boldsymbol{0}};\\
    (\emph{j}) & {\mbox{$\sim$}}(x{\vee}y)={\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}y;\\
    (\emph{k}) & ([{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}],{\wedge},{\vee},{\mbox{$\sim$}})~\text{is
        a Boolean algebra with complementation {\mbox{$\sim$}}};\\
    (\emph{l}) & {\mbox{$\sim$}}{\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}x. 
    \end{array}$$

(): Since $x{\rightarrow}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{1}}{\rightarrow}{\mbox{$\sim$}}x$, we derive ${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x$. On the other hand, beginning with ${\boldsymbol{0}}{\rightarrow}{\mbox{$\sim$}}x\le {\mbox{$\sim$}}x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{0}}$, we obtain ${\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{0}}$.

(b): From (a) just proved we have: ${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x$ and ${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\mbox{$\sim$}}x$ and hence ${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x$. And by virtue of Definition \[D:bn-negation\].b, we get ${\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{1}}$.

(c): According to (a) above, ${\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{0}}$ and ${\mbox{$\sim$}}{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{0}}$ and hence ${\mbox{$\sim$}}x{\vee}{\mbox{$\sim$}}{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\boldsymbol{0}}$. Then, with help of Definition \[D:bn-negation\].c, we get ${\mbox{$\sim$}}x{\vee}{\mbox{$\sim$}}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{0}}$.

(d): Using (a) above twice and, then, (b), we obtain: $${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}{\boldsymbol{0}}{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}{\boldsymbol{1}}.$$

(e): We use (c) and (a) twice to obtain: $${\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}{\boldsymbol{1}}{\vee}{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{0}}.$$

(f): Using (c) and (b) above and Definition \[D:bn-negation\].d, we get: $$\begin{array}{rl}
    {\mbox{$\sim$}}x\leftrightarrow{\mbox{$\sim$}}{\mbox{$\sim$}}x
    &=({\mbox{$\sim$}}x\rightarrow{\mbox{$\sim$}}{\mbox{$\sim$}}x){\wedge}({\mbox{$\sim$}}{\mbox{$\sim$}}x\rightarrow{\mbox{$\sim$}}x)\\
    &=({\mbox{$\sim$}}x\rightarrow{\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x)
    {\wedge}({\mbox{$\sim$}}{\mbox{$\sim$}}x\rightarrow{\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x)\\
    &=({\mbox{$\sim$}}x{\vee}{\mbox{$\sim$}}{\mbox{$\sim$}}x)\rightarrow
    ({\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}x)\\
    &={\mbox{$\sim$}}{\boldsymbol{0}}\rightarrow{\mbox{$\sim$}}{\boldsymbol{1}}~~~[\text{(c) and (b)}]\\
    &={\mbox{$\sim$}}{\boldsymbol{1}}.~~~[\text{Definition~\ref{D:bn-negation}.d}]
    \end{array}$$

(g): We obtain: $$\begin{array}{rl}
        x{\wedge}{\mbox{$\sim$}}x &\le{\mbox{$\sim$}}{\boldsymbol{1}}={\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{0}}~~~[\text{Definition~\ref{D:bn-negation}.b and (d)}]\\
        &\le{\mbox{$\sim$}}{\mbox{$\sim$}}x~~~[\text{\eqref{E:tilde-quasi-idenity} twice}]\\
        &\le{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{1}}={\mbox{$\sim$}}{\boldsymbol{0}}\le x{\vee}{\mbox{$\sim$}}x.~~~[\text{\eqref{E:tilde-quasi-idenity} twice, (e) and Definition~\ref{D:bn-negation}.c}]
    \end{array}$$

(h): Using , (a) and (d), we receive: $${\mbox{$\sim$}}{\boldsymbol{0}}\le x\Longrightarrow
    {\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x\le{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}{\boldsymbol{1}}.$$

(i): In virtue of Definition \[D:bn-negation\].b and (a), we have: ${\mbox{$\sim$}}x\le(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\boldsymbol{0}}$.

In virtue of Definition \[D:bn-negation\].a, we have: $(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}x$. Then, we use (e) to get $(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\boldsymbol{0}}\le{\mbox{$\sim$}}x$.

(j): With help of (i), we get: $$\begin{array}{rl}
    {\mbox{$\sim$}}(x{\vee}y) &=
    (x{\vee}y{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\boldsymbol{0}}\\
    &=(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}(y{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}){\wedge}{\mbox{$\sim$}}{\boldsymbol{0}}\\
    &={\mbox{$\sim$}}x{\wedge}{\mbox{$\sim$}}y. 
    \end{array}$$

(k): First of all, we note that $[{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}]$ is a distributive bounded lattice.  Let us take any $x\in[{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}]$. According to (a), ${\mbox{$\sim$}}x\in[{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}]$. According to Definition \[D:bn-negation\].b and \[D:bn-negation\].c, $x{\wedge}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{1}}$ and $x{\vee}{\mbox{$\sim$}}x={\mbox{$\sim$}}{\boldsymbol{0}}$. Therefore, ${\mbox{$\sim$}}x$ is a complement of $x$ in $[{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}]$.

\(l) From , we derive that ${\mbox{$\sim$}}x\in[{\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}}]$. Then, we apply (k). 

\[C:bn-gives-pair\] Given a -negation, $({\mbox{$\sim$}}{\boldsymbol{1}},{\mbox{$\sim$}}{\boldsymbol{0}})$ is an ${\mbox{$\mathcal{E}$}}$-pair.  Hence $\neg{\mbox{$\sim$}}{\boldsymbol{0}}={\boldsymbol{0}}$.

Indeed, from Proposition \[P:bn-properties\].a, we derive that ${\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{0}}$. And Definition \[D:bn-negation\].d gives us ${\mbox{$\sim$}}{\boldsymbol{0}}{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{1}}$. Further, in virtue of Definitions \[D:bn-negation\].c and \[D:bn-negation\].b, we obtain that ${\mbox{$\sim$}}{\boldsymbol{0}}\le x{\vee}(x{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}})$.

The equality $\neg{\mbox{$\sim$}}{\boldsymbol{0}}={\boldsymbol{0}}$ follows from Proposition \[P:negation\]

Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, two -negations ${\mbox{$\sim$}}_{1}$ and ${\mbox{$\sim$}}_{2}$ are equal in ${\mbox{$\mathfrak{A}$}}$ if and only if ${\mbox{$\sim$}}_{1}{\boldsymbol{1}}={\mbox{$\sim$}}_{2}{\boldsymbol{1}}$.

Assume that ${\mbox{$\sim$}}_{1}{\boldsymbol{1}}={\mbox{$\sim$}}_{2}{\boldsymbol{1}}$. In view of Proposition \[P:bn-properties\].i, we need to show that ${\mbox{$\sim$}}_{1}{\boldsymbol{0}}={\mbox{$\sim$}}_{2}{\boldsymbol{0}}$. According to Corollary \[C:bn-gives-pair\], both pairs $({\mbox{$\sim$}}_{1}{\boldsymbol{1}},{\mbox{$\sim$}}_{1}{\boldsymbol{0}})$ and $({\mbox{$\sim$}}_{2}{\boldsymbol{1}},{\mbox{$\sim$}}_{2}{\boldsymbol{0}})$ belong to ${\mbox{$\mathcal{E}$}}_{\mathfrak{A}}$. In virtue of Proposition \[P:unique\], ${\mbox{$\sim$}}_{1}{\boldsymbol{0}}={\mbox{$\sim$}}_{2}{\boldsymbol{0}}$. The converse is obvious. 

Now we give an example of how a -negation can be defined in a Heyting algebra. 

\[P:bn-negation-1\] Given a Heyting algebra , if $(a,{\mbox{$a^{\ast}$}})$ is an -pair, then the operation $${\mbox{$\sim$}}x=(x{\rightarrow}a){\wedge}{\mbox{$a^{\ast}$}}$$ is a -negation in so that $a={\mbox{$\sim$}}{\boldsymbol{1}}$ and ${\mbox{$a^{\ast}$}}={\mbox{$\sim$}}{\boldsymbol{0}}$.

We have to check that the definition of ${\mbox{$\sim$}}x$ above satisfies the properties ()–() of Definition \[D:bn-negation\]. 

(a): In any Heyting algebra, the following holds: $$x{\rightarrow}y\le (y{\rightarrow}a){\rightarrow}(x{\rightarrow}a)\le
    (y{\rightarrow}a){\wedge}a^{\ast}{\rightarrow}(x{\rightarrow}a){\wedge}a^{\ast}.$$

(b): We also have: $$x{\wedge}(x{\rightarrow}a){\wedge}a^{\ast}=
    x{\wedge}a{\wedge}a^{\ast}\le a{\wedge}a^{\ast}=
    {\boldsymbol{1}}{\wedge}({\boldsymbol{1}}{\rightarrow}a){\wedge}a^{\ast}.$$

(c): We first note that $a^{\ast}=({\boldsymbol{0}}{\rightarrow}a){\wedge}a^{\ast}$. Also, since $a^{\ast}\le x{\vee}(x{\rightarrow}a)$, we have: $a^{\ast}\le x{\vee}(x{\rightarrow}a){\wedge}a^{\ast}$. Thus $({\boldsymbol{0}}{\rightarrow}a){\wedge}a^{\ast}
    \le x{\vee}(x{\rightarrow}a){\wedge}a^{\ast}$.

(d): We notice that $a^{\ast}=({\boldsymbol{0}}{\rightarrow}a){\wedge}a^{\ast}$ and $a=({\boldsymbol{1}}{\rightarrow}a){\wedge}a^{\ast}$. Thus the true inequality $a^{\ast}{\rightarrow}a\le a$ implies $({\boldsymbol{0}}{\rightarrow}a){\wedge}a^{\ast}{\rightarrow}({\boldsymbol{1}}{\rightarrow}a){\wedge}a^{\ast}\le
    ({\boldsymbol{1}}{\rightarrow}a){\wedge}a^{\ast}$, that is ${\mbox{$\sim$}}{\boldsymbol{0}}{\rightarrow}{\mbox{$\sim$}}{\boldsymbol{1}}\le{\mbox{$\sim$}}{\boldsymbol{1}}$.

The last proposition inspires the next definition. 

\[D:t-negation\] Given an ${\mbox{$\mathcal{E}$}}$-pair $\varepsilon=(a,a^{\ast})$ in a Heyting algebra, we define a -negation as follows: $$t_{\varepsilon}(x)=(x{\rightarrow}a){\wedge}a^{\ast}.$$ On the other hand, given a -negation $t(x)$, we denote $\varepsilon_{t}=(t({\boldsymbol{1}}),t({\boldsymbol{0}}))$.

\[P:t(x)\] If $t(x)$ is a -negation, then $$t_{\varepsilon_{t}}(x)=t(x).$$ If $\varepsilon=(a,a^{\ast})$ is an ${\mbox{$\mathcal{E}$}}$-pair, then $$\varepsilon_{t_{\varepsilon}}=\varepsilon.$$

According to Definition \[D:t-negation\] and Proposition \[P:bn-properties\].i, $$t_{\varepsilon_{t}}(x)=(x{\rightarrow}t({\boldsymbol{1}})){\wedge}t({\boldsymbol{0}})=t(x).$$

Further, according to Definition \[D:t-negation\] and Proposition \[P:bn-negation-1\], $$\varepsilon_{t_{\varepsilon}}=(t_{\varepsilon}({\boldsymbol{1}}),t_{\varepsilon}({\boldsymbol{0}}))=(a,a^{\ast}).$$

\[C:bn-pair-isomorphism\] Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, there is a one-one correspondence between ${\mbox{$\mathcal{E}$}}_{\mathfrak{A}}$ and -negations in ${\mbox{$\mathfrak{A}$}}$.

\[D:expansion\] An algebra $({\mbox{$\mathfrak{A}$}},{\mbox{$\sim$}})$, where ${\mbox{$\mathfrak{A}$}}$ is a Heyting algebra with a -negation, is called a -expansion $($a tilde-expansion of $)$.  Also, we will call the Heyting reduct $($or simply reduct$)$ of the -expansion $({\mbox{$\mathfrak{A}$}},{\mbox{$\sim$}})$. The abstract class of all -expansions is denoted by $K$.

\[P:variety\] Class $K$ is a variety. 

*Proof* follows immediately from Definition \[D:bn-negation\].\

\[P:congruences=filters\] Given a -expansion ${\mbox{$\mathfrak{B}$}}=({\mbox{$\mathfrak{A}$}},{\mbox{$\sim$}})$, there is a one-one correspondence between the congruences on ${\mbox{$\mathfrak{B}$}}$ and the filters of the Heyting reduct ${\mbox{$\mathfrak{A}$}}$.

*Proof* follows straightforwardly from Definition \[D:bn-negation\].a.\
In the sequel, we will use the last proposition without reference. 

So far, talking about one-element enrichment in this section, we introduced ${\mbox{$\sim$}}$-negation as a tool to “materialize” the enrichabilty of an unspecified element of a Heyting algebra.  Now we will be dealing with a particular element of the algebra, which is intended to be enriched. 

\[D:tau-tilde-expasion\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra.  We enrich the signature of ${\mbox{$\mathfrak{A}$}}$ with a nullary operation $\tau$ and call ${\mbox{$\mathfrak{A}$}}_{\tau}=({\mbox{$\mathfrak{A}$}},\tau)$ a $\tau$-expansion of ${\mbox{$\mathfrak{A}$}}$. If we know that $\tau$ in the latter is interpreted by $a\in|{\mbox{$\mathfrak{A}$}}|$, we will denote this expansion by ${\mbox{$\mathfrak{A}$}}_{\tau_{a}}$. The -expansion of ${\mbox{$\mathfrak{A}$}}_{\tau}$ that satisfies the identity ${\mbox{$\sim$}}{\boldsymbol{1}}=\tau$ is called a $\tau{\mbox{$\sim$}}$-expansion $($of ${\mbox{$\mathfrak{A}$}}$$)$, in symbols $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$. In ${\mbox{$\mathfrak{A}$}}_{\tau}$ and $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$, ${\mbox{$\mathfrak{A}$}}$ is called the **Heyting reduct** $($or simply **reduct**$)$ of the former and latter and ${\mbox{$\mathfrak{A}$}}_{\tau}$ is the $\tau$-**Heyting reduct** $($or simply $\tau$-**reduct**$)$ of the latter.  The equational class of all $\tau{\mbox{$\sim$}}$-expansions is denoted by $K_{\tau}$. The class of $\tau$-Heyting reducts of the algebras of $K_{\tau}$ is denoted by $K^{\ast}_{\tau}$.

The following observation is obvious. 

The class $K_{\tau}$ is a variety. 

In Section \[S:localization-proof-theoretic-0\], we will see that not only the class $K^{\ast}_{\tau}$ is a variety, but one can prove that the class of all $\tau$-Heyting reducts of any subvariety of $K_{\tau}$ whose equational theory is defined by ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas is a subvariety of $K^{\ast}_{\tau}$.

\[D:packing\] Suppose ${\mbox{$\mathfrak{A}$}}_{\tau}\!\!{\preccurlyeq}\!\!{\mbox{$\mathfrak{B}$}}_{\tau}$ and $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ is a $\tau{\mbox{$\sim$}}$-expansion generated by $|{\mbox{$\mathfrak{A}$}}|$. Then, we say that ${\mbox{$\mathfrak{A}$}}_{\tau}$ is packed in ${\mbox{$\mathfrak{B}$}}_{\tau}$$;$ symbolically ${\mbox{$\mathfrak{A}$}}_{\tau}{\mbox{$\vartriangleleft$}}{\mbox{$\mathfrak{B}$}}_{\tau}$. If ${\mbox{$\mathfrak{A}$}}_{\tau}$ is packed in ${\mbox{$\mathfrak{B}$}}_{\tau}$, then $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ can be regarded as a partial algebra w.r.t.  ${\mbox{$\sim$}}$ and as such is a relative subalgebra of a $($full$)$ algebra $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ $($in the sense of [@gra79], §13$)$; in this case, we also say that $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ is packed in $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$, denoting this by $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}}){\mbox{$\vartriangleleft$}}({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$.

\[P:generating\] If $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}}){\mbox{$\vartriangleleft$}}({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$, then ${\mbox{$\mathfrak{B}$}}_{\tau}$ is generated as a $\tau$-expansion by $|{\mbox{$\mathfrak{A}$}}|\cup\lbrace{\mbox{$\sim$}}{\boldsymbol{0}}\rbrace$. Conversely, if $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ is a relative subalgebra of a $\tau{\mbox{$\sim$}}$-expansion $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ and the latter is generated as a $\tau$-expansion by $|{\mbox{$\mathfrak{A}$}}|\cup\lbrace{\mbox{$\sim$}}{\boldsymbol{0}}\rbrace$, then $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})\vartriangleleft({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$.

The first part follows straightforwardly by the property Proposition \[P:bn-properties\].i.  The second part is obvious. 

\[P:bn-closeness\] Let $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ be a $\tau{\mbox{$\sim$}}$-expansion and let $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ be a relative subalgebra of $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$. Then the following conditions are equivalent$:$ [*$$\begin{array}{rl}
    (\text{a}) & {\mbox{$\mathfrak{A}$}}_{\tau}\mbox{ is closed under {\mbox{$\sim$}}};\\
    (\text{b}) & {\mbox{$\sim$}}a\in{\mbox{$\mathfrak{A}$}}_{\tau}\mbox{ and }{\mbox{$\sim$}}{\mbox{$\sim$}}a\in{\mbox{$\mathfrak{A}$}}_{\tau},\mbox{ for some
        $a\in|{\mbox{$\mathfrak{A}$}}|$};\\
    (\text{c}) & {\mbox{$\sim$}}{\boldsymbol{0}}\in{\mbox{$\mathfrak{A}$}}_{\tau}. 
    \end{array}$$*]{}

The implication $(\text{a}){\Rightarrow}(\text{b})$ is obvious. 

Then, $(\text{b}){\Rightarrow}(\text{c})$ follows straightforward from Proposition \[P:bn-properties\].c. 

Now we prove $(\text{c}){\Rightarrow}(\text{a})$. Since, by premise, ${\mbox{$\sim$}}{\boldsymbol{1}}\in{\mbox{$\mathfrak{A}$}}_{\tau}$, we use Proposition \[P:bn-properties\].i. 

Let ${\mbox{$\mathfrak{A}$}}_{\tau}\preccurlyeq{\mbox{$\mathfrak{B}$}}_{\tau}$ and let $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}}_{1})$ and $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}}_{2})$ be $\tau{\mbox{$\sim$}}$-expansions.  Then the following properties are equivalent: $$\begin{array}{cl}
    (\emph{a}) &({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}}_{1})\preccurlyeq({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}}_{2});\\
    (\emph{b}) &{\mbox{$\sim$}}_{1}{\boldsymbol{0}}={\mbox{$\sim$}}_{2}{\boldsymbol{0}};\\
    (\emph{c}) &{\mbox{$\sim$}}_{1}\tau={\mbox{$\sim$}}_{2}\tau. 
    \end{array}$$

The conditional $(\text{a})\Rightarrow(\text{b})$ is obvious.  Next, assume that (b) is true.  Then, by virtue of Proposition \[P:bn-properties\].e, $${\mbox{$\sim$}}_{1}\tau={\mbox{$\sim$}}_{1}{\mbox{$\sim$}}_{1}{\boldsymbol{1}}={\mbox{$\sim$}}_{1}{\boldsymbol{0}}={\mbox{$\sim$}}_{2}{\boldsymbol{0}}={\mbox{$\sim$}}_{2}{\mbox{$\sim$}}_{2}{\boldsymbol{1}}={\mbox{$\sim$}}_{2}\tau;$$ thus (c) is true.  Finally, suppose that ${\mbox{$\sim$}}_{1}\tau={\mbox{$\sim$}}_{2}\tau$. The latter,as above, implies that $${\mbox{$\sim$}}_{1}{\boldsymbol{0}}={\mbox{$\sim$}}_{1}{\mbox{$\sim$}}_{1}{\boldsymbol{1}}={\mbox{$\sim$}}_{1}\tau={\mbox{$\sim$}}_{2}\tau={\mbox{$\sim$}}_{2}{\mbox{$\sim$}}_{2}{\boldsymbol{1}}={\mbox{$\sim$}}_{2}{\boldsymbol{0}}.$$ Then, we apply Proposition \[P:bn-properties\]

Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra and $a\in|{\mbox{$\mathfrak{A}$}}|$. Interpreting a constant $\tau$ as $a$, we get a $\tau$-expansion ${\mbox{$\mathfrak{A}$}}_{\tau_{a}}$. Then, we obtain algebra ${\delta[{\mbox{$\mathfrak{A}$}}_{\tau_{a}}]}$. It is clear that in the latter algebra $(h(\tau_{a}),{\deltah(\tau_{a})})$ is an ${\mbox{$\mathcal{E}$}}$-pair (Proposition \[P:delta-h(x)-2\]).  Thus, by adding of the ${\mbox{$\sim$}}$-negation to ${\delta[{\mbox{$\mathfrak{A}$}}_{\tau_{a}}]}$, corresponding to this ${\mbox{$\mathcal{E}$}}$-pair, in the way provisioned in Proposition \[P:bn-negation-1\], we obtain a $\tau{\mbox{$\sim$}}$-expansion.  Moreover, by virtue of Proposition \[P:generating\], $({\mbox{$\mathfrak{A}$}}_{\tau_{a}},{\mbox{$\sim$}}){\mbox{$\vartriangleleft$}}({\delta[{\mbox{$\mathfrak{A}$}}_{\tau_{a}}]},{\mbox{$\sim$}})$. We state this conclusion by the following proposition. 

\[P:packing\] Given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$ and $a\in|{\mbox{$\mathfrak{A}$}}|$, $({\mbox{$\mathfrak{A}$}}_{\tau_{a}},{\mbox{$\sim$}}){\mbox{$\vartriangleleft$}}({\delta[{\mbox{$\mathfrak{A}$}}_{\tau_{a}}]},{\mbox{$\sim$}})$; in other words, ${\mbox{$\mathfrak{A}$}}_{\tau_{a}}{\mbox{$\vartriangleleft$}}{\delta[{\mbox{$\mathfrak{A}$}}_{\tau_{a}}]}$ (in the sense of Definition \[D:packing\]). 

One-element enrichment from a proof-theoretic viewpoint {#S:localization-proof-theoretic-0}
=======================================================

In this section we prove an analog of Kuznetsov’s Theorem (Proposition \[P:equipollence\]), where in place of $\square$ the connective ${\mbox{$\sim$}}$ is used.[^10] We need it to derive an analog of Kuznetsov’s Corollary 2 mentioned on p. , which is obtained as Corollary \[C:L(A\_tau)=L(B\_tau)\]. 

The ${\mbox{$\mathcal{L}_{\tau}$}}$-equipollence of two calculi {#S:localization-proof-theoretic}
---------------------------------------------------------------

In this subsection we discus logical systems formulated in languages ${\mbox{$\mathcal{L}_{\tau}$}}$ and ${\mbox{$\mathcal{L}_{\tau\sim}$}}$. These languages are extensions of the language ${\mbox{$\mathcal{L}_{a}$}}$ introduced in Section \[S:syntactic\].  We obtain ${\mbox{$\mathcal{L}_{\tau}$}}$ by adding a nullary connective $\tau$. Then, ${\mbox{$\mathcal{L}_{\tau\sim}$}}$ is the extension of ${\mbox{$\mathcal{L}_{\tau}$}}$ by enriching the latter with another unary connective $\sim$. Unspecified formulas of ${\mbox{$\mathcal{L}_{\tau}$}}$ will be denoted by symbols $A^{\ast}, B^{\ast},\ldots$ (with or without subscripts) and those of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$ by letters $\alpha,\beta, \gamma$, and $\lambda$ (also with or without subscripts).  The formulas of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$ of the form $\sim\!\alpha$ are called $\sim$-***formulas***.  We refer to those ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formulas which do not contain $\sim$ (i.e. are ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas) as $\sim$-***free***.  The ***degree*** of an ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formula is the number of occurrences of the connective $\sim$ in the formula.  Thus all ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas have the degree 0.  Also, we will be using the following notation: $${\bm{\top}}:= p{\rightarrow}p.$$

Calculus ${\textbf{Int}_{\tau}}$ is defined in the language ${\mbox{$\mathcal{L}_{\tau}$}}$, while the calculi ${\textbf{Int}_{\tau\sim}}$ and ${\textbf{KM}_{\tau}}$ are defined in the language ${\mbox{$\mathcal{L}_{\tau\sim}$}}$. The calculus ${\textbf{Int}_{\tau}}$ is ${\mbox{\textbf{Int}}}$ in the language ${\mbox{$\mathcal{L}_{\tau}$}}$. The calculus ${\textbf{Int}_{\tau\sim}}$ is defined by the axioms of ${\mbox{\textbf{Int}}}$ in the language ${\mbox{$\mathcal{L}_{\tau\sim}$}}$. The calculus ${\textbf{KM}_{\tau}}$ is ${\textbf{Int}_{\tau\sim}}$ plus the following formulas: $$\begin{array}{rl}
(\text{a}) &\sim p\leftrightarrow(p\rightarrow\tau)\wedge\sim\tau,\\
(\text{b}) & (\sim\tau\rightarrow\tau)\rightarrow\tau,\\
(\text{c}) &\sim\tau\rightarrow(p\vee(p\rightarrow\tau)),\\
(\text{d}) &\tau\rightarrow\sim\tau. 
\end{array}$$ The postulated inference rules of all calculi under consideration are (uniform) substitution and modus ponens.[^11]

Below we will deal with several types of derivation.  We distinguish these types as follows. 

-   ${\textbf{Int}_{\tau}}+A^{\ast}\vdash B^{\ast}$ means that there is a derivation in ${\mbox{$\mathcal{L}_{\tau}$}}$ of a formula $B^{\ast}$ from axioms of ${\mbox{\textbf{Int}}}$ and a formula $A^{\ast}$ as a premise by using substitution of ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas and modus ponens..

-   ${\textbf{Int}_{\tau\sim}}+\alpha\vdash\beta$ denotes the fact that there is a derivation in ${\mbox{$\mathcal{L}_{\tau\sim}$}}$ of a formula $\beta$ from axioms of ${\mbox{\textbf{Int}}}$ and a formula $\alpha$ by using substitution of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formulas and modus ponens. 

-   ${\textbf{KM}_{\tau}}+\alpha \vdash\beta$ is to denote that there is a derivation in ${\mbox{$\mathcal{L}_{\tau\sim}$}}$ of $\beta$ from axioms of ${\mbox{\textbf{Int}}}$, formulas of the list $\text{(a)}-\text{(d)}$, and $\alpha$.

If a derivation ${\mbox{$\mathcal{D}$}}$ supports, say, the claim ${\textbf{KM}_{\tau}}+\alpha \vdash\beta$, we will write ${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+\alpha \vdash\beta$ and call ${\mbox{$\mathcal{D}$}}$ a ${\textbf{KM}_{\tau}}$-***derivation***.  This notation and terminology apply also to the types of derivation which have been introduced above, as well as to those which will be defined below. 

A derivation is called refined if all substitutions, if any, apply only to the axioms occurring in the derivation or to a premise. 

It is a well-known fact that if the only postulated inference rules of a calculus are substitution and modus ponens, then any derivation can be transformed to a refined derivation of the same last formula. ( Cf.  [@sob74; @lam79].) 

Suppose $S=\lbrace\alpha_{1},\ldots,\alpha_{n}\rbrace$ is a finite set of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formulas.  A formula $\sim\!\!\alpha$ is called ***maximal in*** $S$ if it is a subformula of at least one of the formulas $\alpha_{i}$ and it does not occur in the scope of any occurrence of the connective $\sim$ in any of the formulas $\alpha_{i}$. The set of all maximal formulas of $S$ is denoted by $M(S)$. We also apply this definition, when $S$ is a finite list of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formulas. 

\[D:pure-derivation\] A refined [*${\textbf{KM}_{\tau}}$*]{}-derivation [*${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+\alpha\vdash\beta$*]{} is called pure if [*$M({\mbox{$\mathcal{D}$}})\subseteq M(\alpha,\beta)$*]{}.  The notation [*${\mbox{$\mathcal{D}$}}: {\textbf{KM}_{\tau}}+\alpha\Vdash\beta$*]{} reads that ${\mbox{$\mathcal{D}$}}$ is a pure [*${\textbf{KM}_{\tau}}$*]{}-derivation.  These definition and notation apply to [*${\textbf{Int}_{\tau\sim}}$*]{}-derivations as well. 

Thus, ${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+ A^{\ast}\Vdash B^{\ast}$ if and only if ${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+ A^{\ast}\vdash B^{\ast}$ and $M({\mbox{$\mathcal{D}$}})=\emptyset$. Hence, if the first statement is true, then ${\textbf{Int}_{\tau}}+A^{\ast}\vdash B^{\ast}$. In this section we aim to prove Proposition \[P:equipollence\] and Corollary \[C:general-equipollence\].  We will reach this goal through the following key, though auxiliary, notion. 

\[D:set-I\] Let $\mathbb{N}$ be the set of nonnegative numbers.  Then we arrange the pairs of $\mathbb{N}^{2}$ by the following relation: $$(x_{1},x_{2})\ll(y_{1},y_{2})\Longleftrightarrow  x_{1}<y_{1},~\text{or}~x_{1}=y_{1}~\text{and}~x_{2}\le y_{2}.$$ We denote $\mathcal{I}=\langle\mathbb{N}^{2},\ll\rangle$. It is clear that $r_{0}=(0,0)$ is the least element of $\mathcal{I}$. We call $r_{0}$ the root of $\mathcal{I}$.

A routine check shows that $\mathcal{I}$ is a poset. 

The poset $\mathcal{I}$ satisfies the descending chain condition [*[@gra78]*]{}. 

First we notice that $$\label{E:<<-relation}
(x_{1},x_{2})\ll(y_{1},y_{2})\Longrightarrow x_1\le y_1.$$

Given a pair $s=(x_1,x_2)\in\mathcal{I}$, we call $x_1$, the *level* of $s$. It is obvious that, given a pair $s$, there are only finitely many pairs $t$ with $t\ll s$ such that the levels of $s$ and $t$ coincide.  Also, according to (\[E:&lt;&lt;-relation\]), given a pair $s$, each pair $t$ with $t\ll s$ is of a level that is less than or equal to the level of $s$.

A descending chain in $\mathcal{I}$ is called down-complete if its least element is $r_{0}$.

\[D:rank\] We say that a refined derivation ${\mbox{$\mathcal{D}$}}$ is of rank $s\in\mathcal{I}$, where $s=(m,n)$, denoting this fact by [*${\mbox{$\mathcal{D}$}}: {\textbf{KM}_{\tau}}+\alpha\vdash_{s}\beta$*]{} $($or by [*${\mbox{$\mathcal{D}$}}: {\textbf{Int}_{\tau\sim}}+\alpha\vdash_{s}\beta$ $)$*]{}, if $M({\mbox{$\mathcal{D}$}})\neq\emptyset$, $m$ is the highest degree among the formulas of $M({\mbox{$\mathcal{D}$}})$ and $n$ is the number of the formulas of $M({\mbox{$\mathcal{D}$}})$ of the degree $m$. If $M({\mbox{$\mathcal{D}$}})=\emptyset$ then $s=r_{0}$.

It is obvious that $${\textbf{KM}_{\tau}}+A^{\ast}\vdash_{r_{0}} B^{\ast} \Longleftrightarrow {\textbf{KM}_{\tau}}+A^{\ast}\Vdash B^{\ast}.$$

Given formulas $\alpha$, $\beta$ and $\gamma$, we denote by $$\alpha[\beta:\gamma]$$ the result of replacement of all occurrences of $\beta$ in $\alpha$ with $\gamma$.

\[P:key-lemma-one\] Let [*${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+\alpha\vdash_{s} \beta$*]{} be a refined derivation of rank $s\neq r_{0}$. Also, suppose a formula $\sim\!\gamma\in M({\mbox{$\mathcal{D}$}})$, $\gamma\neq\tau$, $\sim\!\gamma$ is not a subformula of $\alpha$ and $\sim\!\gamma$ is of the highest degree among the formulas of $M({\mbox{$\mathcal{D}$}})$ .  Then there are a formula $\delta$ and a refined derivation [*${\mbox{$\mathcal{D}$}}^{\ast}:{\textbf{KM}_{\tau}}+\alpha\vdash_{t} \beta[\sim\!\gamma:\delta]$*]{} such that$:$

-   if $M({\mbox{$\mathcal{D}$}})=\lbrace\sim\!  A^{\ast}_{1},\ldots,\sim\!  A^{\ast}_{n}\rbrace$, for some formulas $A^{\ast}_{1},\ldots,A^{\ast}_{n}$, and $\gamma=A^{\ast}_{i}$, then $M({\mbox{$\mathcal{D}$}}^{\ast})=\lbrace \sim\!  A^{\ast}_{1},\ldots,\sim\!  A^{\ast}_{i-1},\sim\!  A^{\ast}_{i+1},\sim\!\tau\rbrace$, in which case $s=t=(1,n)$$;$

-   otherwise, $t\ll s$ and $t\neq s$.

Let us denote by $${\mbox{$\mathcal{D}$}}: \gamma_{1},\ldots,\gamma_{n}$$ the given derivation.  Obviously, $\gamma_{n}=\beta$. Then, we define: $$\delta=(\gamma\rightarrow\tau)\wedge\sim\!\tau.$$ We notice that $\delta$ does not contain $\sim\!\gamma$. Further, we define: $$\gamma_{i}^{\ast}=\gamma_{i}[\sim\!\gamma:\delta].$$

We note that $\gamma_{i}^{\ast}$ does not contain $\sim\!\gamma$. If $\gamma\neq A^{\ast}$, for some $A^{\ast}$, then the degree of $\gamma_{i}^{\ast}$ is less than that of $\gamma_{i}$ but greater than or equal to 1; otherwise, the degree of $\gamma_{i}^{\ast}$ equals that of $\gamma_{i}$ and both are equal to $1$. Now we have to consider in more detail what happens in conversion of $\gamma_{i}$ to $\gamma_{i}^{\ast}$. For this we examine the following cases. 

Case 1: $\gamma_{i}$ is an instance of an ${\mbox{\textbf{Int}}}$-axiom.  Then $\gamma_{i}^{\ast}$ is also an instance of the same ${\mbox{\textbf{Int}}}$-axiom. 

Case 2: $\gamma_{i}$ is an instance of the axiom (a), that is a formula $\sim\!\lambda\leftrightarrow(\lambda\rightarrow\tau)\wedge\sim\!\tau$. In this case, assume that $\lambda\neq\gamma$. Then $\gamma_{i}$ does not contain $\sim\!\gamma$ at all and hence $\gamma_{i}^{\ast}=\gamma_{i}$.

Case 3: $\gamma_{i}=\sim\!\gamma\leftrightarrow(\gamma\rightarrow\tau)\wedge\sim\!\tau$. Then $\gamma_{i}^{\ast}=\delta\leftrightarrow\delta$. It is obvious that ${\textbf{Int}_{\tau\sim}}\Vdash\gamma_{i}^{\ast}$. Let us denote a derivation that supports the last claim by ${\mbox{$\mathcal{D}$}}_{1}$.

Case 4: $\gamma_{i}=\sim\!\tau\rightarrow(\lambda\vee(\lambda\rightarrow\tau))$. Then $\gamma_{i}^{\ast}=\sim\!\tau\rightarrow(\lambda[\sim\!\gamma:\delta]\vee(\lambda[\sim\!\gamma:\delta]\rightarrow\tau))$, that is, $\gamma_{i}^{\ast}$ is an instance of the axiom (c) and does not contain $\sim\!\gamma$.

Case 5: $\gamma_{i}$ is an instance of $\alpha$. Then, since $\sim\!\gamma$ is not a subformula of $\alpha$ and $\sim\!\gamma$ is maximal in ${\mbox{$\mathcal{D}$}}$, $\gamma_{i}^{\ast}$ remains to be an instance of $\alpha$.

Case 6: $\gamma_{i}$ is obtained by modus ponens from $\gamma_{k}$ and $\gamma_{l}=\gamma_{k}\rightarrow\gamma_{i}$ for some $k,l<i$. Then $\gamma_{i}^{\ast}$ can be derived from $\gamma_{k}^{\ast}$ and $\gamma_{l}^{\ast}=\gamma_{k}^{\ast}\rightarrow\gamma_{i}^{\ast}$.

Further, we define $$[\gamma_{i}^{\ast}]=
    \begin{cases}
    \begin{array}{cl}
    \gamma_{i}^{\ast} &\text{if $\gamma_{i}^{\ast}$ is obtained in one of the cases 1,2, 4, 5 or 6}\\
    {\mbox{$\mathcal{D}$}}_{1} &\text{if $\gamma_{i}^{\ast}$ is obtained according to case 3.} 
    \end{array}
    \end{cases}$$

Now we denote: $${\mbox{$\mathcal{D}$}}^{\ast}: [\gamma_{1}^{\ast}],\ldots,[\gamma_{n}^{\ast}].$$

It is clear that ${\mbox{$\mathcal{D}$}}^{\ast}$ is a refined derivation which supports ${\textbf{KM}_{\tau}}+\alpha\vdash\beta[\sim\!\gamma:\delta]$. Assume that $s=(m,n)$. In the case of the first alternative in the conclusion of the lemma, that is when $s=(1,n)$, $\delta$ contains only one $\sim$-formula – $\sim\!\tau$. Regardless of whether $M({\mbox{$\mathcal{D}$}})$ contains $\sim\!\tau$ or not, $M({\mbox{$\mathcal{D}$}}^{\ast})$ will have it.  Thus the conclusion of the first alternative is true.  Otherwise, $m>1$ and, then, either $t=(m,n-1)$ or $t=(m_{1},n_{1})$ with $1\le m_{1}<m$ and some $n_{1}\ge 1$. We observe that in both cases $t\ll s$ and $t\neq s$.

\[P:key-lemma-two\] Let [*${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+\alpha\vdash\beta$*]{} be a refined derivation such that $M({\mbox{$\mathcal{D}$}})=\lbrace\sim\!\tau\rbrace$. Also, assume that $\sim\!\tau$ is not a subformula of $\alpha$. Then there is a $\sim$-free formula $A^{\ast}$ such that [*${\textbf{KM}_{\tau}}+\alpha\Vdash\beta[\sim\!\tau:A^{\ast}]$*]{}. 

Assume that the formulas $$\label{E:c-axiom-instances}
    \sim\!\tau\rightarrow(\lambda_{1}\vee(\lambda_{1}\rightarrow\tau)),\ldots,
    \sim\!\tau\rightarrow(\lambda_{k}\vee(\lambda_{k}\rightarrow\tau))$$ are all the instances of the axiom (c) in the refined derivation ${\mbox{$\mathcal{D}$}}$. Then, we define: $$A^{\ast}=\begin{cases}
    \begin{array}{cl}
    \bigwedge_{1\le j\le k}(\lambda_{j}\vee(\lambda_{j}\rightarrow\tau))[\sim\!\tau:{\bm{\top}}]
    &\text{if the list (\ref{E:c-axiom-instances}) is not empty}\\
    {\bm{\top}}&\text{if the list (\ref{E:c-axiom-instances}) is empty}. 
    \end{array}
    \end{cases}$$ Thus, if the list (\[E:c-axiom-instances\]) is nonempty, then we denote: $$A^{\ast}=\bigwedge_{1\le j\le k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)),$$ for some $\sim$-free formulas $B^{\ast}_{1},\ldots, B^{\ast}_{k}$.

Further, we denote: $$\gamma_{i}^{\ast}=\gamma_{i}[\sim\!\tau:A^{\ast}].$$ Now we consider the following cases. 

Case 1: $\gamma_{i}$ is an instance of an ${\mbox{\textbf{Int}}}$-axiom.  Then $\gamma_{i}^{\ast}$ is also an instance of the same ${\mbox{\textbf{Int}}}$-axiom. 

Case 2: $\gamma_{i}=\sim\!\tau\leftrightarrow(\tau\rightarrow\tau)\wedge\sim\!\tau$. Then $\gamma_{i}^{\ast}=A^{\ast}\leftrightarrow(\tau{\rightarrow}\tau)\wedge A^{\ast}$. It is obvious that there is a derivation ${\mbox{$\mathcal{D}$}}_{1}:{\textbf{Int}_{\tau}}\Vdash\delta\leftrightarrow(\tau{\rightarrow}\tau)\wedge A$. 

Case 3: $\gamma_{i}=(\sim\!\tau{\rightarrow}\tau){\rightarrow}\tau$. If (\[E:c-axiom-instances\]) is empty, then $\gamma_{i}^{\ast}=({\bm{\top}}{\rightarrow}\tau){\rightarrow}\tau$ and hence ${\textbf{Int}_{\tau}}\Vdash \gamma_{i}^{\ast}$. Let us denote a pure derivation that supports the last claim by ${\mbox{$\mathcal{D}$}}_{2}$.

If (\[E:c-axiom-instances\]) is nonempty, then $\gamma_{i}^{\ast}=
    (\bigwedge_{1\le j\le k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}\tau){\rightarrow}\tau$. Then we observe: $$\begin{array}{l}
    {\textbf{Int}_{\tau}}\Vdash ((B^{\ast}_{j}{\rightarrow}\tau)\wedge((B^{\ast}_{j}{\rightarrow}\tau){\rightarrow}\tau)){\rightarrow}\tau, ~\text{that is}\\
    {\textbf{Int}_{\tau}}\Vdash ((B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}\tau){\rightarrow}\tau~\text{and hence}\\
    {\textbf{Int}_{\tau}}\Vdash ((B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}\tau)\leftrightarrow\tau;~\text{the latter in turn implies that}\\
    {\textbf{Int}_{\tau}}\Vdash ((B^{\ast}_{1}\vee(B^{\ast}_{1}\rightarrow\tau)){\rightarrow}((B^{\ast}_{2}\vee(B^{\ast}_{2}\rightarrow\tau)){\rightarrow}\tau)){\rightarrow}\tau,~\text{that is}\\
    {\textbf{Int}_{\tau}}\Vdash(\bigwedge_{1\le j\le 2}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}\tau){\rightarrow}\tau;~\text{thus, repeating this, we obtain}\\
    {\textbf{Int}_{\tau}}\Vdash(\bigwedge_{1\le j\le k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}\tau){\rightarrow}\tau. 
    \end{array}$$ We denote by ${\mbox{$\mathcal{D}$}}_{3}$ a pure derivation supporting the last claim. 

Case 4: $\gamma^{i}$ is an instance of the axiom (c), that is $\gamma_{i}=\sim\!\tau{\rightarrow}(\lambda_{j}{\rightarrow}(\lambda_{j}{\rightarrow}\tau))$. Consequently, $\gamma_{i}^{\ast}=A^{\ast}
    {\rightarrow}(\lambda_{j}[\sim\!\tau:A^{\ast}]\vee(\lambda_{j}[\sim\!\tau:A^{\ast}]{\rightarrow}\tau))$. As it is well-known, (see, e.g., [@kle52], [§]{} 26) $$\begin{array}{l}
    {\textbf{Int}_{\tau}}\Vdash A^{\ast}
    {\rightarrow}(\lambda_{j}[\sim\!\tau:{\bm{\top}}]\vee(\lambda_{j}[\sim\!\tau:{\bm{\top}}]{\rightarrow}\tau)),~\text{that is}\\
    {\textbf{Int}_{\tau}}\Vdash \bigwedge_{1\le j\le k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)){\rightarrow}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau)). 
    \end{array}$$ Therefore, ${\textbf{Int}_{\tau}}\Vdash\gamma_{i}^{\ast}$. We denote a pure derivation supporting the last claim by ${\mbox{$\mathcal{D}$}}_{4}$.

Case 5: $\gamma_{i}=\tau{\rightarrow}\sim\!\tau$. Then either $\gamma_{i}^{\ast}=
    \tau{\rightarrow}{\bm{\top}}$ or $\gamma_{i}^{\ast}=\tau{\rightarrow}\bigwedge_{1\le j\le k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau))$. Obviously, in both cases ${\textbf{Int}_{\tau}}\Vdash\gamma_{i}^{\ast}$. We denote a pure derivation supporting the last claim by ${\mbox{$\mathcal{D}$}}_{5}$.

Case 6: $\gamma_{i}$ is obtained by modus ponens from $\gamma_{l}$ and $\gamma_{l}{\rightarrow}\gamma_{i}$. Obviously, then $\gamma_{i}^{\ast}$ is obtained by modus ponens from $\gamma_{l}^{\ast}$ and $\gamma_{l}^{\ast}{\rightarrow}\gamma_{i}^{\ast}$.

Now we define: $$[\gamma_{i}^{\ast}]=\begin{cases}
    \begin{array}{cl}
    \gamma_{i}^{\ast} &\text{if $\gamma_{i}$ falls in Case 1};\\
    {\mbox{$\mathcal{D}$}}_{1 } &\text{if $\gamma_{i}$ falls in Case 2};\\
    {\mbox{$\mathcal{D}$}}_{2} &\text{if $\gamma_{i}$ falls in the first subcase of Case 3};\\
    {\mbox{$\mathcal{D}$}}_{3} &\text{if $\gamma_{i}$ falls in the second subcase of Case 3};\\
    {\mbox{$\mathcal{D}$}}_{4} &\text{if $\gamma_{i}$ falls in Case 4};\\
    {\mbox{$\mathcal{D}$}}_{5} &\text{if $\gamma_{i}$ falls in Case 5}. 
    \end{array}
    \end{cases}$$

Further, we denote: $${\mbox{$\mathcal{D}$}}^{\ast}: [\gamma_{1}^{\ast}],\ldots,[\gamma_{n}^{\ast}].$$

It should be clear that ${\mbox{$\mathcal{D}$}}^{\ast}:{\textbf{KM}_{\tau}}+\alpha\Vdash\beta[\sim\!\tau:A^{\ast}]$.

\[P:equipollence\] The calculi [*${\textbf{KM}_{\tau}}$*]{} and [*${\textbf{Int}_{\tau}}$*]{} are ${\mbox{$\mathcal{L}_{\tau}$}}$-equipollent*;* that is, for any ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas $A^{\ast}$ and $B^{\ast}$, [ *$${\textbf{KM}_{\tau}}+A^{\ast}\vdash B^{\ast}\Longleftrightarrow {\textbf{Int}_{\tau}}+ A^{\ast}\vdash B^{\ast}.$$*]{}

Let ${\mbox{$\mathcal{D}$}}:{\textbf{KM}_{\tau}}+A^{\ast}\vdash_{s} B^{\ast}$ be a refined derivation of rank $s=(m,n)$, where $m,n\ge 1$. Using Lemma \[P:key-lemma-one\], maybe more than one time, we obtain a refine derivation ${\mbox{$\mathcal{D}$}}^{\prime}:{\textbf{KM}_{\tau}}+A^{\ast}\vdash_{t} B^{\ast}$ with $M({\mbox{$\mathcal{D}$}}^{\prime})=\lbrace{\mbox{$\sim$}}\tau\rbrace$. Then, we apply Lemma \[P:key-lemma-two\], to get ${\textbf{KM}_{\tau}}+A^{\ast}\Vdash B^{\ast}$. The latter means that ${\textbf{Int}_{\tau}}+ A^{\ast}\vdash B^{\ast}$.

\[C:general-equipollence\] For any set $\Gamma$ of ${\mbox{$\mathcal{L}_{\tau}$}}$-formulas and any ${\mbox{$\mathcal{L}_{\tau}$}}$-formula $A^{\ast}$, the following equivalence holds*:* [ *$${\textbf{KM}_{\tau}}+\Gamma\vdash A^{\ast}\Longleftrightarrow {\textbf{Int}_{\tau}}+ \Gamma\vdash A^{\ast}.$$*]{}

*Proof* follows immediately from Proposition \[P:equipollence\].\

Completeness of [*${\textbf{KM}_{\tau}}$*]{}
--------------------------------------------

We intend to prove the following. 

\[P:KMt-completeness\] For any ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formula $\alpha$, [*${\textbf{KM}_{\tau}}\vdash\alpha$*]{} if, and only if, any $\tau{\mbox{$\sim$}}$-expansion validates $\alpha$.

It suffices to show that all proper axioms $(\text{a})-(\text{d})$ of ${\textbf{KM}_{\tau}}$ are valid in any $\tau{\mbox{$\sim$}}$-expansion and, conversely, if a $\tau$-expansion with a unary operation ${\mbox{$\sim$}}x$ satisfies $(\text{a})-(\text{d})$ of ${\textbf{KM}_{\tau}}$, then it is a $\tau{\mbox{$\sim$}}$-expansion. 

First we rewrite the proper axioms of ${\textbf{KM}_{\tau}}$ as identities: $$\begin{array}{cl}
(\text{a}^{\prime}) &{\mbox{$\sim$}}x=(x{\rightarrow}\tau)\wedge{\mbox{$\sim$}}\tau,\\
(\text{b}^{\prime}) &({\mbox{$\sim$}}\tau{\rightarrow}\tau)\le\tau,\\
(\text{c}^{\prime}) &{\mbox{$\sim$}}\tau\le(x\vee(x{\rightarrow}\tau)),\\
(\text{d}^{\prime}) &\tau\le{\mbox{$\sim$}}\tau. 
\end{array}$$

Now let $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ be a $\tau{\mbox{$\sim$}}$-expansion.  Then, we recall, not only the identities $(\text{a})$–$(\text{d})$ of Definition \[D:bn-negation\] are true but also ${\mbox{$\sim$}}{\boldsymbol{1}}=\tau$ (Definition \[D:tau-tilde-expasion\]).  The latter and Proposition \[P:bn-properties\].e imply that ${\mbox{$\sim$}}{\boldsymbol{0}}={\mbox{$\sim$}}\tau$. And, by virtue of Corollary \[C:bn-gives-pair\], we conclude that $(\tau,{\mbox{$\sim$}}\tau)$ is an ${\mbox{$\mathcal{E}$}}$-pair in ${\mbox{$\mathfrak{A}$}}_{\tau}$. This immediately implies that the identities $(\text{b}^{\prime})$–$(\text{d}^{\prime})$ are valid in $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$. By virtue of Proposition \[P:t(x)\], $(\text{a}^{\prime})$ is also valid. 

Next assume that the identities $(\text{a}^{\prime})$–$(\text{d}^{\prime})$ are valid in a $\tau$-expansion ${\mbox{$\mathfrak{A}$}}_{\tau}$ with a unary operation ${\mbox{$\sim$}}x$. From $(\text{b}^{\prime})$–$(\text{d}^{\prime})$ we derive that $(\tau,{\mbox{$\sim$}}\tau)$ is an ${\mbox{$\mathcal{E}$}}$-pair in ${\mbox{$\mathfrak{A}$}}_{\tau}$. According to Proposition \[P:bn-negation-1\], ${\mbox{$\sim$}}x$ is a ${\mbox{$\sim$}}$-negation in ${\mbox{$\mathfrak{A}$}}_{\tau}$ and $\tau={\mbox{$\sim$}}{\boldsymbol{1}}$; that is $({\mbox{$\mathfrak{A}$}}_{\tau},{\mbox{$\sim$}})$ is a $\tau{\mbox{$\sim$}}$-expansion. 

It is clear that the last proposition admits the following generalization. 

\[C:KM-completeness\] Let $\Lambda\cup\lbrace\alpha\rbrace$ be a set of ${\mbox{$\mathcal{L}_{\tau\sim}$}}$-formulas.  Then [*$${\textbf{KM}_{\tau}}+\Lambda\vdash \alpha\Longleftrightarrow\Lambda\models\alpha~(\textit{for all $\tau{\mbox{$\sim$}}$-expansions}).$$*]{}

Also, we obtain the following. 

\[K\^\*\_tau-variety\] The class $K_{\tau}^{\ast}$ is a variety.  Moreover, for any ${\mbox{$\mathcal{L}_{\tau}$}}$-formula $A^{\ast}$, [*$$K_{\tau}^{\ast}\models A^{\ast}\Longleftrightarrow{\textbf{Int}_{\tau}}\vdash A^{\ast}.$$*]{}

It should be clear that $K_{\tau}^{\ast}$ is closed under formation of direct products, of subalgebras and of homomorphic images. 

Now, using Corollary \[C:general-equipollence\] with $\Gamma=\emptyset$ and Proposition \[P:KMt-completeness\], we receive the equivalence above. 

Connecting the two viewpoints on one-element enrichment {#S:connecting-viewpoints}
=======================================================

We connect the two viewpoints discussed above in Sections \[S:localization-algebraic\] and \[S:localization-proof-theoretic-0\] via the following two propositions and corollary.  Namely, in this section we aim to show that any ${\tau}$-expansion can be embedded into such a ${\tau}$-expansion, where the element corresponding to the constant ${\tau}$ is enrichable, and both ${\tau}$-expansions generation one and the same variety, or, equivalently, have the same logic in ${\mbox{$\mathcal{L}_{\tau}$}}$.

\[P:generated-by-tau-expansions\] Any variety ${\mbox{$\mathcal{V}$}}$ of $\tau$-expansions is generated by the class ${\mbox{$\mathcal{V}$}}\cap K^{\ast}_{\tau}$.

Let $$\Gamma={\{B^{\ast} ~|~(\forall~{\mbox{$\mathfrak{A}$}}_{\tau}^{\prime}\in{\mbox{$\mathcal{V}$}})
    ({\mbox{$\mathfrak{A}$}}_{\tau}^{\prime}\models B^{\ast})\}}.$$

Suppose, for some ${\mbox{$\mathfrak{A}$}}_{\tau}\in{\mbox{$\mathcal{V}$}}$, ${\mbox{$\mathfrak{A}$}}_{\tau}\not\models A^{\ast}$. Then ${\textbf{Int}_{\tau}}+\Gamma\not\vdash A^{\ast}$. By virtue of Corollary \[C:KM-completeness\], ${\textbf{KM}_{\tau}}+\Gamma\not\vdash A^{\ast}$. This implies that there is a $\tau{\mbox{$\sim$}}$-expansion $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ such that ${\mbox{$\mathfrak{B}$}}_{\tau}\models\Gamma$ and ${\mbox{$\mathfrak{B}$}}_{\tau}\not\models A^{\ast}$. It remains to notice that ${\mbox{$\mathfrak{B}$}}_{\tau}\in{\mbox{$\mathcal{V}$}}$.

\[P:L(A\_tau)=L(C\_tau)\] For any $\tau$-expansion ${\mbox{$\mathfrak{A}$}}_{\tau}$, there is a $\tau{\mbox{$\sim$}}$-expansion $({\mbox{$\mathfrak{C}$}}_{\tau},{\mbox{$\sim$}})$ such that ${\mbox{$\mathfrak{A}$}}_{\tau}{\preccurlyeq}{\mbox{$\mathfrak{C}$}}_{\tau}$ and $L({\mbox{$\mathfrak{A}$}}_{\tau})=L({\mbox{$\mathfrak{C}$}}_{\tau})$.

Let ${\mbox{$\mathcal{V}$}}$ be the variety of the $\tau$-expansions generated by ${\mbox{$\mathfrak{A}$}}_{\tau}$. According to Proposition \[P:generated-by-tau-expansions\], ${\mbox{$\mathfrak{A}$}}_{\tau}\in{\mathbf{H}}{\mathbf{S}}{\mathbf{P}}({\mbox{$\mathcal{V}$}}\cap K^{\ast}_{\tau})$. In view of Proposition \[P:congruences=filters\], the $\tau$-expansions have the congruence extension property and hence ${\mbox{$\mathfrak{A}$}}_{\tau}\in{\mathbf{S}}{\mathbf{H}}{\mathbf{P}}({\mbox{$\mathcal{V}$}}\cap K^{\ast}_{\tau})$. Now we notice that in each algebra of ${\mbox{$\mathcal{V}$}}\cap K^{\ast}_{\tau}$, the element $\tau$ is enrichable.  This will be kept in any direct product of algebras of ${\mbox{$\mathcal{V}$}}\cap K^{\ast}_{\tau}$ and in any homorphic image of the latter, for the first-order formula $$\exists x\forall y((\tau\le x)\& (x{\rightarrow}\tau=\tau)\& (x\le y\vee(y{\rightarrow}\tau)))$$ is preserved under formation of direct products and homomorphic images; cf.  [@mal73], Sections 7.4 and 7.5.  Thus there is a $\tau$-expansion ${\mbox{$\mathfrak{C}$}}_{\tau}$ such that ${\mbox{$\mathfrak{A}$}}_{\tau}{\preccurlyeq}{\mbox{$\mathfrak{C}$}}_{\tau}$ and $\tau$ is enrichable in ${\mbox{$\mathfrak{C}$}}_{\tau}$. Then, by virtue of Proposition \[P:bn-negation-1\], a ${\mbox{$\sim$}}$-negation can be defined in ${\mbox{$\mathfrak{C}$}}_{\tau}$ so that ${\mbox{$\sim$}}{\boldsymbol{1}}=\tau$. It remains to notice that $L({\mbox{$\mathfrak{A}$}}_{\tau})=L({\mbox{$\mathfrak{C}$}}_{\tau})$.

\[C:L(A\_tau)=L(B\_tau)\] For any $\tau$-expansion ${\mbox{$\mathfrak{A}$}}_{\tau}$, there is a $\tau{\mbox{$\sim$}}$-expansion $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ such that ${\mbox{$\mathfrak{A}$}}_{\tau}{\mbox{$\vartriangleleft$}}{\mbox{$\mathfrak{B}$}}_{\tau}$ and $L({\mbox{$\mathfrak{A}$}}_{\tau})=L({\mbox{$\mathfrak{B}$}}_{\tau})$.

Let $({\mbox{$\mathfrak{C}$}}_{\tau},{\mbox{$\sim$}})$ be a $\tau{\mbox{$\sim$}}$-expansion from Proposition \[P:L(A\_tau)=L(C\_tau)\].  Let $({\mbox{$\mathfrak{B}$}}_{\tau},{\mbox{$\sim$}})$ be the subalgebra of $({\mbox{$\mathfrak{C}$}}_{\tau},{\mbox{$\sim$}})$ generated by $|{\mbox{$\mathfrak{A}$}}|\cup\lbrace\tau\rbrace$. It remains to notice that $L({\mbox{$\mathfrak{C}$}}_{\tau}){\subseteq}L({\mbox{$\mathfrak{B}$}}_{\tau}){\subseteq}L({\mbox{$\mathfrak{A}$}}_{\tau})$ and, then, apply Proposition \[P:L(A\_tau)=L(C\_tau)\]. 

Our goal is to prove the following. 

\[conjecture\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebra such that ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Also, let $a\in|{\mbox{$\mathfrak{A}$}}|$ and $(a,{\mbox{$a^{\ast}$}})$ be an ${\mbox{$\mathcal{E}$}}$-pair in ${\mbox{$\mathfrak{B}$}}$. Then, if ${\mbox{$\mathfrak{A}$}}_{\tau_{a}}{\mbox{$\vartriangleleft$}}{\mbox{$\mathfrak{B}$}}_{\tau_{a}}$, then ${\mbox{$\mathfrak{B}$}}$ is isomorphic to ${\delta[{\mbox{$\mathfrak{A}$}}_{a}]}$.

Properties related to Stone embedding {#S:Stone-embedding-properties-main}
=====================================

First, we define two filters of Heyting algebra, among which we designate one, $F_{a}$. In the sequel, this filter will play a key role. 

Some filters of Heyting algebra {#S:filters}
-------------------------------

In this subsection we use [@rs70] as a main reference, though employed implicitly.\
Let us fix a Heyting algebra and an element $a\in|{\mbox{$\mathfrak{A}$}}|$. Then, we define: $$X_{a}={\{x\in|{\mbox{$\mathfrak{A}$}}| ~|~x{\rightarrow}a=a\}}.$$

\[P:Xa\] $X_{a}$ is a filter of .  Moreover, $X_{a}$ is proper if and only if $a\neq{\boldsymbol{1}}$.

Suppose $x_{1},x_{2}\in X_{a}$, that is, $x_{1}{\rightarrow}a=a$ and $x_{2}{\rightarrow}a=a$. Then we have: $$\begin{array}{rl}
    x_{1}{\wedge}x_{2}{\rightarrow}a &= x_{1}{\rightarrow}(x_{2}{\rightarrow}a)\\
    &= x_{1}{\rightarrow}a\\
    &= a.
    \end{array}$$

Next let $x{\rightarrow}a=a$, and $y\geq x$. Then we obtain: $$\begin{array}{rl}
    y{\rightarrow}a &= y{\rightarrow}(x{\rightarrow}a)\\
    &= y{\wedge}x{\rightarrow}a\\
    &= x{\rightarrow}a\\
    &= a.
    \end{array}$$

Finally, it is obvious that ${\boldsymbol{0}}\in X_{a}$ if and only if $a={\boldsymbol{1}}$.

Now we define $$F_{a}={\{x{\vee}(x{\rightarrow}a) ~|~x\in|{\mbox{$\mathfrak{A}$}}|\}}.$$

\[P:Fa\] For any Heyting algebra and element $a\in|{\mbox{$\mathfrak{A}$}}|$, the following conditions are equivalent: $$\begin{array}{cl}
    (\emph{\text{a}}) &y\in F_{a};\\
    (\emph{\text{b}}) &y{\rightarrow}a\leq a\mbox{ and }a\leq y;\\
    (\emph{\text{c}}) &y{\rightarrow}a\leq y.
    \end {array}$$

We prove that $(\text{a})\Rightarrow (\text{b})\Rightarrow (\text{c})\Rightarrow (\text{a})$.

$(\text{a})\Rightarrow (\text{b})$: Let $y\in F_{a}$. Then for some $x\in|{\mbox{$\mathfrak{A}$}}|$, $y=x{\vee}(x{\rightarrow}a)$. It is clear that $a\leq y$. Also, $$\begin{array}{rl}
    y{\rightarrow}a & =(x{\rightarrow}a){\wedge}((x{\rightarrow}a){\rightarrow}a)\\
    &= (x{\rightarrow}a){\wedge}a\\
    &=a.
    \end{array}$$

$(\text{b})\Rightarrow (\text{c})$: Obvious, by transitivity of $\leq$.

$(\text{c})\Rightarrow (\text{a})$: Obvious again, for $y{\rightarrow}a\leq y$ implies $y=y{\vee}(y{\rightarrow}a)$.

\[C:Fa\] $F_{a}=X_{a}\cap[a)$ and hence $F_{a}$ is a filter, all elements of which are dense.  Also, $F_{a}={\{y\in|{\mbox{$\mathfrak{A}$}}| ~|~y{\rightarrow}a\leq y\}}$. Moreover, $F_{a}$ is proper if is nontrivial.[^12]

Some properties of Stone embedding {#S:properties-of-Stone-embedding}
----------------------------------

The main references here are [@rs70], though implicitly,  [@mak72] (see also [@gm05]) and also [@mur86], [§]{}1. 

Let ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. We define: $$\begin{aligned}
&\varphi:{\mathcal{S}_{\mathfrak{B}}}\longrightarrow{\mathcal{S}_{\mathfrak{A}}}:~G\mapsto G\cap|{\mbox{$\mathfrak{A}$}}|;\\
&\widetilde{\varphi}:{\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}\longrightarrow{\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}:~\mathcal{U}\mapsto{\{\varphi(G) ~|~G\in\mathcal{U}\}}.\end{aligned}$$

We note the following property: $$\label{E:axiliary}
\widetilde{\varphi}(\mathcal{U}\cup\mathcal{V})=\widetilde{\varphi}(\mathcal{U})\cup\widetilde{\varphi}(\mathcal{V}).$$

\[P:maksimova-lemma-5\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Also, let $F\in{\mathcal{S}_{\mathfrak{A}}}$ and $a\in|{\mbox{$\mathfrak{A}$}}|\setminus F$. Then there is a filter $G\in{h_{\mathfrak{B}}(\overline{a})}$ such that $F=G\cap|{\mbox{$\mathfrak{A}$}}|$.

[^13] First, we define the filter $[F)_{\mathfrak{B}}$ and note that $[F)_{\mathfrak{B}}\cap|{\mbox{$\mathfrak{A}$}}|=F$. Thus the set $$\Phi:={\{H ~|~H~\text{is a ${\mbox{$\mathfrak{B}$}}$-filter such that  $H\cap|{\mbox{$\mathfrak{A}$}}|=F$}\}}$$ is nonempty.  It is obvious that $\Phi$ satisfies the condition of Zorn’s lemma and hence $\Phi$ contains a maximal filter $G$ w.r.t.  $\subseteq$. We aim to show that $G\in{\mathcal{S}_{\mathfrak{B}}}$.

For contradiction, assume that $x\vee y\in G$, but neither $x\in G$ nor $y\in G$. Next, we define two filters: $H_1:=[G\cup\lbrace x\rbrace)_{\mathfrak{B}}$ and $H_2:=[G\cup\lbrace y\rbrace)_{\mathfrak{B}}$. It is obvious that both $H_1$ and $H_2$ are proper.  Now we show that either $H_1\cap|{\mbox{$\mathfrak{A}$}}|\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$ or $H_2\cap|{\mbox{$\mathfrak{A}$}}|\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$. For contradiction, assume that neither of the last is the case, that is, $H_1\cap|{\mbox{$\mathfrak{A}$}}|\not\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$ and $H_2\cap|{\mbox{$\mathfrak{A}$}}|\not\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$. This implies that there are $z_1\in H_1\cap|{\mbox{$\mathfrak{A}$}}|\setminus G\cap|{\mbox{$\mathfrak{A}$}}|$ and $z_2\in H_2\cap|{\mbox{$\mathfrak{A}$}}|\setminus G\cap|{\mbox{$\mathfrak{A}$}}|$, which yields that $z_1\vee z_2\in H_1\cap H_2\cap|{\mbox{$\mathfrak{A}$}}|$. The latter in turn implies that $x\rightarrow z_1\vee z_2\in G$ and $y\rightarrow z_1\vee z_2\in G$, that is $z_1\vee z_2\in G$. Then, by definition of $G$, $z_1\vee z_2\in F$ and hence either $z_1\in F$ or $z_2\in F$. In both cases, we get a contradiction, for, if, for example, $z_1\in F$, then $z_1\in G\cap|{\mbox{$\mathfrak{A}$}}|$. Thus either $H_1\cap|{\mbox{$\mathfrak{A}$}}|\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$ or $H_2\cap|{\mbox{$\mathfrak{A}$}}|\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$. Now, let us take the first as true.  Then we receive: $F\subseteq H_1\cap|{\mbox{$\mathfrak{A}$}}|\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|=F$. A contradiction, because $G\subset H_1$ and at the same time $G$ is a maximal filter in $\Phi$. Similarly, we get a contradiction, if we start with the second.  Thus $G\in{\mathcal{S}_{\mathfrak{B}}}$. Since $a\notin G$, $G\in{h_{\mathfrak{B}}(\overline{a})}$.

\[C:maksimova-lemma-5\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. For any filter $F\in{\mathcal{S}_{\mathfrak{A}}}$, there is a filter $G\in{\mathcal{S}_{\mathfrak{B}}}$ such that $F=G\cap|{\mbox{$\mathfrak{A}$}}|$; that is to say, the map $\varphi$ is surjective.[^14]

We apply Proposition \[P:maksimova-lemma-5\] for $a={\boldsymbol{0}}$.

\[C:axiliary-one\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. For every $x\in|{\mbox{$\mathfrak{A}$}}|$, $\widetilde{\varphi}({h_{\mathfrak{B}}(x)})={h_{\mathfrak{A}}(x)}$.

For any $x\in|{\mbox{$\mathfrak{A}$}}|$, we obtain: $$\begin{array}{rl}
F\in\widetilde{\varphi}({h_{\mathfrak{B}}(x)}) &\Longleftrightarrow
F=G\cap|{\mbox{$\mathfrak{A}$}}|,~\text{for some $G\in{h_{\mathfrak{B}}(x)}$}\\
&\Longleftrightarrow F\in{h_{\mathfrak{A}}(x)}.\quad[\text{in virtue of Corollary~\ref{C:maksimova-lemma-5}}]
\end{array}$$

\[P:on-prime-filter\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Also, let $F$ be an ${\mbox{$\mathfrak{A}$}}$-filter and $a\in|{\mbox{$\mathfrak{A}$}}|\setminus F$. Then there is a filter $G\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $F\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$. [*(Part 1)*]{} In particular, if the algebras ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ coincide, then there is a filter $G\in\max{h_{\mathfrak{A}}(\overline{a})}$ such that $F\subseteq G$. [*(Part 2)*]{}

We define the set: $$\Phi:={\{H ~|~\text{$H$ is a ${\mbox{$\mathfrak{B}$}}$-filter, $F\subseteq H\cap|{\mbox{$\mathfrak{A}$}}|$ and $a\notin H$}\}}$$ The set $\Phi$ is nonempty, for the filter $[F)_{\mathfrak{B}}$ belongs to it.  Also, it is clear that the set $\Phi$ satisfies the condition of Zorn’s lemma.  Let $G$ be a maximal filter from $\Phi$. By definition, $a\notin G$ and $F\subseteq G\cap|{\mbox{$\mathfrak{A}$}}|$. It remains to show that $G\in{\mathcal{S}_{\mathfrak{A}}}$. After proving that, we will easily conclude that $G\in\max{h_{\mathfrak{B}}(\overline{a})}$.

For contradiction, assume that for some elements $x$ and $y$ of ${\mbox{$\mathfrak{A}$}}$, $x\lor y\in G$ but neither $x\in G$ nor $y\in G$. Next, we define $H_1:=[G\cup\lbrace x\rbrace)_{\mathfrak{B}}$ and $H_2:=[G\cup\lbrace y\rbrace)_{\mathfrak{B}}$. We aim to show that either $a\notin H_1$ or $a\notin H_2$. For contradiction, we suppose that $a\in H_1$ and $a\in H_2$. This implies that for some elements $u$ and $v$ of $G$, $u\le x\rightarrow a$ and $v\le y\rightarrow a$. Both inequalities imply that both $x\rightarrow a\in G$ and $y\rightarrow a\in G$ are true and hence, by premise, $a\in G$. A contradiction.  Thus either $a\notin H_1$ or $a\notin H_2$. Let us take the first as true; that is $a\notin H_1$. Then, since $G\subset H_1$, which implies that $F\subseteq H_{1}\cap|{\mbox{$\mathfrak{A}$}}|$, and $a\notin H_1$, $G$ is not maximal in $\Phi$. A contradiction.  Similarly, we get a contradiction, if we start with the assumption that $a\notin H_2$. Thus $G\in{\mathcal{S}_{\mathfrak{B}}}$ and hence $G\in{h_{\mathfrak{B}}(\overline{a})}$. If $H\in{h_{\mathfrak{B}}(\overline{a})}$ and $G\subseteq H$, then, by definition of $G$, $H=G$. This implies that $G\in\max{h_{\mathfrak{B}}(\overline{a})}$

\[C:on-prime-filter-1\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras such that ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$ and let $a\in|{\mbox{$\mathfrak{A}$}}|$. Then ${\{G\cap|{\mbox{$\mathfrak{A}$}}| ~|~G\in\max{h_{\mathfrak{B}}(\overline{a})}\}}\subseteq\max{h_{\mathfrak{A}}(\overline{a})}$.

Assume that $G\in\max{h_{\mathfrak{B}}(\overline{a})}$. It is obvious that $G\cap|{\mbox{$\mathfrak{A}$}}|\in{h_{\mathfrak{A}}(\overline{a})}$. Let us take any ${\mbox{$\mathfrak{A}$}}$-filter $F$ with $G\cap|{\mbox{$\mathfrak{A}$}}|\subset F$. For contradiction, assume that $a\notin F$. Then, we define a ${\mbox{$\mathfrak{B}$}}$-filter $[G\cup F)_{\mathfrak{B}}$. We note that $G\subset[G\cup F)_{\mathfrak{B}}$. For contradiction, assume that $a\in[G\cup F)_{\mathfrak{B}}$. Then there exist elements $u\in G$ and $v\in F$ such that $u\wedge v\le a$. This implies that $v\rightarrow a\in G$ and hence, by premise, that $v\rightarrow a\in F$, that is $a\in F$. A contradiction.  Thus $a\notin[G\cup F)_{\mathfrak{B}}$. Then, by virtue of Proposition \[P:on-prime-filter\] (part 2), there is a filter $H\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $[G\cup F)_{\mathfrak{B}}\subseteq H$. It is obvious that $G\subset H$. A contradiction.  Thus $a\in F$. Hence, $G\cap|{\mbox{$\mathfrak{A}$}}|\in\max{h_{\mathfrak{A}}(\overline{a})}$.

\[C:on-prime-filter-2\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras such that ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$ and let $a\in|{\mbox{$\mathfrak{A}$}}|$. For any ${\mbox{$\mathfrak{B}$}}$-filter $G$ with $G\cap|{\mbox{$\mathfrak{A}$}}|\in\max{h_{\mathfrak{A}}(\overline{a})}$, there is a filter $H\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $G\subseteq H$ and $H\cap|{\mbox{$\mathfrak{A}$}}|=G\cap|{\mbox{$\mathfrak{A}$}}|$.

Let $G$ be a ${\mbox{$\mathfrak{B}$}}$-filter and $G\cap|{\mbox{$\mathfrak{A}$}}|\in\max{h_{\mathfrak{A}}(\overline{a})}$. The latter in particular implies that $a\notin G$. According to Proposition \[P:on-prime-filter\] (part 2), there is a filter $H\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $G\subseteq H$. The letter implies that $G\cap|{\mbox{$\mathfrak{A}$}}|\subseteq H\cap|{\mbox{$\mathfrak{A}$}}|$. If it were the case that $G\cap|{\mbox{$\mathfrak{A}$}}|\subset H\cap|{\mbox{$\mathfrak{A}$}}|$, then, by premise, we would have that $a\in H\cap|{\mbox{$\mathfrak{A}$}}|$. A contradiction. 

\[C:axiliary-two\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Also, let $a\in|{\mbox{$\mathfrak{A}$}}|$. Then $\widetilde{\varphi}(\max{h_{\mathfrak{B}}(\overline{a})})=\max{h_{\mathfrak{A}}(\overline{a})}$.

Assume that $G\in\max{h_{\mathfrak{B}}(\overline{a})}$. Then, according to Corollary \[C:on-prime-filter-1\], $\varphi(G)\in\max{h_{\mathfrak{A}}(\overline{a})}$. Now, we suppose that $F\in\max{h_{\mathfrak{A}}(\overline{a})}$. Let us form the filter $[F)_{\mathfrak{B}}$. We observe that $a\notin[F)_{\mathfrak{B}}$ and $[F)_{\mathfrak{B}}\cap|{\mbox{$\mathfrak{A}$}}|=F$. In virtue of Proposition \[P:on-prime-filter\], there is $G\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $G\cap|{\mbox{$\mathfrak{A}$}}|=F$, that is $F\in\widetilde{\varphi}(\max{h_{\mathfrak{B}}(\overline{a})})$.

\[P:axiliary\] Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras with ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Also, let $a\in|{\mbox{$\mathfrak{A}$}}|$ and $(a,a^{\ast})$ be an -pair in ${\mbox{$\mathfrak{B}$}}$. Then $\widetilde{\varphi}({h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})})=\delta{h_{\mathfrak{A}}(a)}$.

Indeed, we obtain: $$\begin{array}{rl}
\widetilde{\varphi}({h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})}) &= \widetilde{\varphi}({h_{\mathfrak{B}}(a)}\cup\max{h_{\mathfrak{B}}(\overline{a})})\quad[\text{Proposition~\ref{P:delta-h(x)-1}}]\\
&= \widetilde{\varphi}({h_{\mathfrak{B}}(a)})\cup\widetilde{\varphi}(\max{h_{\mathfrak{B}}(\overline{a})})
\quad[\text{in virtue of~\eqref{E:axiliary}}]\\
&={h_{\mathfrak{A}}(a)}\cup\max{h_{\mathfrak{A}}(\overline{a})}\quad[\text{Corollaries~\ref{C:axiliary-one} and~\ref{C:axiliary-two}}]\\
&=\delta{h_{\mathfrak{A}}(a)}\quad[\text{Proposition~\ref{P:delta-h(x)-1}}]. 
\end{array}$$

\[P:F\_a-is-included-in-F\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra and $a\in|{\mbox{$\mathfrak{A}$}}|$. For any filter $F\in{h_{\mathfrak{A}}(\overline{a})}$, $F\in\max{h_{\mathfrak{A}}(\overline{a})}$ if, and only if, $F_a\subseteq F$.

First, we note that if $a={\boldsymbol{1}}$, then the proposition is trivially true.  Thus we assume that $a\neq{\boldsymbol{1}}$.

Suppose $F\in{h_{\mathfrak{A}}(\overline{a})}$, And, for contradiction, assume that $x\in F_{a}\setminus F$. We notice that $x{\rightarrow}a\not\in F$ (Proposition \[P:Fa\]) and $x{\vee}(x{\rightarrow}a)\not\in F$ (since $F$ is a prime filter).  Now we define a filter $G:=[F\cup\lbrace x{\vee}(x{\rightarrow}a)\rbrace)_{\mathfrak{A}}$. We aim to show that $a\not\in G$. Indeed, if $a$ were in $G$, then for some $y\in F$, we would have $y{\wedge}(x{\vee}(x{\rightarrow}a))\le a$, that is $(x{\vee}(x{\rightarrow}a)){\rightarrow}(y{\rightarrow}a)={\boldsymbol{1}}$. The latter implies that $(x{\rightarrow}(y{\rightarrow}a)){\wedge}((x{\rightarrow}a){\rightarrow}(y{\rightarrow}a))={\boldsymbol{1}}$, which in turn yields that $y{\rightarrow}(x{\rightarrow}a)\in F$. However, the latter immediately implies that $x{\rightarrow}a\in F$. A contradiction.  Thus $a\notin G$. Then, in virtue of Proposition \[P:on-prime-filter\], there is a filter $H\max{h_{\mathfrak{A}}(\overline{a})}$ such that $G\subseteq H$. Noticing that $F\subset H$, we get a contradiction once again, which completes the proof of inclusion $F_a\subseteq F$.

Conversely, assume that $F_a\subseteq F$. For contradiction, we suppose that there is a filter $H\in{h_{\mathfrak{A}}(\overline{a})}$ with $F\subset H$. Let $x\in H\setminus F$. Since $F_a\subseteq F$, $x\vee(x\rightarrow a)\in $.  And, since the filter $F$ is prime, $x\rightarrow a\in F$. This implies that $x\rightarrow a\in H$ and hence $a\in H$. A contradiction. 

\[P:meet-F\_a\] Let ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$, $a\in|{\mbox{$\mathfrak{A}$}}|$ and $(a,{\mbox{$a^{\ast}$}})\in{\mbox{$\mathcal{E}$}}_{\mathfrak{B}}$. If $\bigwedge\!  F_a$ exists in ${\mbox{$\mathfrak{B}$}}$, where $F_a:={\{x\in|{\mbox{$\mathfrak{A}$}}| ~|~x\rightarrow a\le x\}}$, then $\bigwedge\!  F_a={\mbox{$a^{\ast}$}}$ in ${\mbox{$\mathfrak{B}$}}$.

Let us denote $u:=\bigwedge\!  F_a$. We note that ${\mbox{$a^{\ast}$}}\le x$, for every $x\in F_a$ (Section \[S:filters\]).  Hence ${\mbox{$a^{\ast}$}}\le u$. For contradiction, assume that $u\not\le{\mbox{$a^{\ast}$}}$. Then $a\notin[u)_{\mathfrak{B}}$. In virtue of Propositional \[P:on-prime-filter\] (part 2), there is a filter $G\in\max{h_{\mathfrak{B}}(\overline{a})}$ such that $[u)_{\mathfrak{B}}\subseteq G$. According to Proposition \[P:F\_a-is-included-in-F\], we obtain that $[{\mbox{$a^{\ast}$}})_{\mathfrak{B}})\subseteq G$, which implies that, on the one hand $u\vee{\mbox{$a^{\ast}$}}$ is a lower bound of $F_a$, and, on the other, $u<u\vee {\mbox{$a^{\ast}$}}$.

\[C:meet-F\_a-1\] Let ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$, $a\in|{\mbox{$\mathfrak{A}$}}|$ and $(a,{\mbox{$a^{\ast}$}})\in{\mbox{$\mathcal{E}$}}_{\mathfrak{B}}$. Then the equality $\bigwedge{\{{h_{\mathfrak{B}}(x)} ~|~x\in F_a\}}={h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})}$ in $h_{\mathfrak{B}}[{\mbox{$\mathfrak{B}$}}]$, where $F_a:={\{x\in|{\mbox{$\mathfrak{A}$}}| ~|~x\rightarrow a\le x\}}$.

We note that $h_{\mathfrak{B}}[{\mbox{$\mathfrak{B}$}}]{\preccurlyeq}{\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$ and $({h_{\mathfrak{B}}(a)},{h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})})$ is an ${\mbox{$\mathcal{E}$}}$-pair in ${\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$ (Proposition \[P:delta-h(x)-2\]).  Since $\bigcap{\{{h_{\mathfrak{B}}(x)} ~|~x\in F_a\}}$ is the greatest lower bound of ${\{{h_{\mathfrak{B}}(x)} ~|~x\in F_a\}}$ in ${\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$, then the equality is true $\bigwedge{\{{h_{\mathfrak{B}}(x)} ~|~x\in F_a\}}={h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})}$ in ${\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$ and also in $h_{\mathfrak{B}}[{\mbox{$\mathfrak{B}$}}]$.

\[C:meet-F\_a-2\] Let ${\mbox{$\mathfrak{A}$}}$ be a Heyting algebra and $a\in|{\mbox{$\mathfrak{A}$}}|$. Then $\bigwedge{\{{h_{\mathfrak{A}}(x)} ~|~x\in F_{a}\}}$ exists in ${\delta[{\mbox{$\mathfrak{A}$}}_{a}]}$ and the equality ${\delta{h_{\mathfrak{A}}(})}{a}=\bigwedge{\{{h_{\mathfrak{A}}(x)} ~|~x\in F_{a}\}}$, where $F_a:={\{x\in|{\mbox{$\mathfrak{A}$}}| ~|~x\rightarrow a\le x\}}$, is true in $\delta[{\mbox{$\mathfrak{A}$}}_{a}]$.

We first derive from the given the following: $h_{\mathfrak{A}}[{\mbox{$\mathfrak{A}$}}]{\preccurlyeq}{\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$, ${h_{\mathfrak{A}}(a)}\in h_{\mathfrak{A}}[{\mbox{$\mathfrak{A}$}}]$ and $({h_{\mathfrak{A}}(a)},{\delta{h_{\mathfrak{A}}(a)}})$ is an ${\mbox{$\mathcal{E}$}}$-pair in ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ (Proposition \[P:delta-h(x)-2\]); also, $\bigwedge{\{{h_{\mathfrak{A}}(x)} ~|~x\in F_{a}\}}=\bigcap{\{{h_{\mathfrak{A}}(x)} ~|~x\in F_{a}\}}$ in ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$. Then, in virtue of Proposition \[P:meet-F\_a\], the equality $\bigwedge{\{{h_{\mathfrak{A}}(x)} ~|~x\in F_{a}\}}={\delta{h_{\mathfrak{A}}(a)}}$ holds in ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$. Since ${\delta[{\mbox{$\mathfrak{A}$}}_{a}]}{\preccurlyeq}{\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$, the last equality also holds in ${\delta[{\mbox{$\mathfrak{A}$}}_{a}]}$.

Completing the proof of Theorem \[T:main-theorem\] {#S:completing-proof}
==================================================

We aim to prove Conjecture \[conjecture\], from which Theorem \[T:main-theorem\] will follow straightforwardly.\
Let ${\mbox{$\mathfrak{A}$}}$ and ${\mbox{$\mathfrak{B}$}}$ be Heyting algebras such that ${\mbox{$\mathfrak{A}$}}{\preccurlyeq}{\mbox{$\mathfrak{B}$}}$. Gradually, we will be adding more conditions.\
First, we observe that $$\label{E:tilde-phi-surjective}
\textit{the map $\widetilde{\varphi}$ is surjective.}$$

Indeed, this follows from that the map $\varphi$ is surjective (Corollary \[C:maksimova-lemma-5\]).\
Next, we remind the reader that the map $\varphi^{-1}$ is an embedding of ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ into ${\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$; cf.  [@mak72], Lemma 2.\
The following observation is obvious: For any $\mathcal{U}\in{\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$, $$\label{E:phi^{-1}(tilde-phi(U))}
\mathcal{U}\subseteq\varphi^{-1}(\widetilde{\varphi}(\mathcal{U})).$$

Also, it is easy to see that $$\label{E:phi^{-1}(h_A(x)=h_B(x)}
\varphi^{-1}(h_{\mathfrak{A}}(x))=h_{\mathfrak{B}}(x),~\textit{for any $x\in|{\mbox{$\mathfrak{A}$}}|$}.$$

Indeed, we have: $$G\in\varphi^{-1}(h_{\mathfrak{A}}(x))\Longleftrightarrow
G\cap|{\mbox{$\mathfrak{A}$}}|\in h_{\mathfrak{A}}(x)\Longleftrightarrow G\in h_{\mathfrak{B}}(x).$$

Now, assume that $a\in|{\mbox{$\mathfrak{A}$}}|$ and $(a,{\mbox{$a^{\ast}$}})$ is an ${\mbox{$\mathcal{E}$}}$-pair in ${\mbox{$\mathfrak{B}$}}$. Then $$\label{E:h_B(astar)-included-ph^{-1}(delta-h_A(a))}
h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})\subseteq\varphi^{-1}({\deltah_{\mathfrak{A}}(a)}).$$

Indeed, with the help of  and Proposition \[P:axiliary\], we obtain: $$h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})\subseteq\varphi^{-1}(\widetilde{\varphi}(h_{\mathfrak{B}}({\mbox{$a^{\ast}$}})))=\varphi^{-1}({\deltah_{\mathfrak{A}}(a)}).$$

Finally, since ${\deltah_{\mathfrak{A}}(a)}$ is a lower bound of the set ${\{h_{\mathfrak{A}}(x) ~|~x\in F_{a}\}}$ in ${\textsf{H}({\mathcal{S}_{\mathfrak{A}}})}$ (Proposition \[P:delta-h(x)-2\]), using , we conclude that $\varphi^{-1}({\deltah_{\mathfrak{A}}(a)})$ is a lower bound of the set ${\{h_{\mathfrak{B}}(x) ~|~x\in F_{a}\}}$ in ${\textsf{H}({\mathcal{S}_{\mathfrak{B}}})}$. And, in virtue of Corollary \[C:meet-F\_a-1\], we obtain that $$\label{E:last}
\varphi^{-1}({\deltah_{\mathfrak{A}}(a)})=h_{\mathfrak{B}}({\mbox{$a^{\ast}$}}).$$

Further, with the help of and , we derive the statement of Conjecture \[conjecture\].\
At last, using Conjecture \[conjecture\] and Corollary \[C:L(A\_tau)=L(B\_tau)\], we obtain that $L({\mbox{$\mathfrak{A}$}})=L(\delta[{\mbox{$\mathfrak{A}$}}_{a}])$. Thus the condition of Corollary \[C:reducibility-4\] is satisfied and hence Theorem \[T:main-theorem\] is proven. 

Discussion {#S:conclusion}
==========

We have proved that, given a Heyting algebra ${\mbox{$\mathfrak{A}$}}$, the algebra ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ defines the same equational class as ${\mbox{$\mathfrak{A}$}}$ does. ( Theorem \[T:main-theorem\]) In addition, ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ can inherit some algebraic and cardinality properties, if ${\mbox{$\mathfrak{A}$}}$ has them. ( Propositions \[P:countable\] and \[P:sub-irr\]) In view of all these properties, we formulate several open questions, dividing them into two problem sets.\
[<span style="font-variant:small-caps;">Problem set 1</span>]{}\
(a) *Is ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ finitely subdirectly irreducible, providing that ${\mbox{$\mathfrak{A}$}}$ is?*  [^15]\
(b) *Is ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ a double Heyting algebra (alias bi-Heyting algebra), providing that ${\mbox{$\mathfrak{A}$}}$ is?*  [^16]\
(c) *Is ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ projective $($weakly projective$)$, providing that ${\mbox{$\mathfrak{A}$}}$ is?*  [^17]\
(d) *Is ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ finitely approximable, providing that ${\mbox{$\mathfrak{A}$}}$ is?*  [^18]\
Questions like the ones above can be multiplied; we chose only a few.\
The other category of questions is related to elementary properties which may be preserved in ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$.\
[<span style="font-variant:small-caps;">Problem set 2</span>]{}\
(a) *Do ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ and ${\mbox{$\mathfrak{A}$}}$ have the same quasi-equational theory?*\
(b) *Which elementary properties are preserved in ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$?* 

[10]{} Church, A. (1956) [*Introduction to [M]{}athematical [L]{}ogic*]{}, Princeton Univ.  Press, Princeton. 

Esakia, L. (2006) The modalized [H]{}eyting calculus: a conservative modal extension of the intuitionistic logic. [* J. Appl.  Non-Classical Logics*]{}, 16(3–4), 349–366. 

Gabbay, D. and Maksimova, L. (2005) [*Interpolation and [D]{}efinability: [M]{}odal and [I]{}ntuitionistic [L]{}ogics*]{}, volume 46 of [*Oxford Logic Guides*]{}.  The Clarendon Press Oxford University Press, Oxford. 

Ghilardi, S. (1992) Free [H]{}eyting algebras as bi-[H]{}eyting algebras. [* C. R. Math.  Rep. Acad.  Sci.  Canada*]{}, 6:240–244. 

Gorbunov, V. (1998) [*Algebraic [T]{}heory of [Q]{}uasivarieties*]{}.  Siberian School of Algebra and Logic.  Consultants Bureau, New York. 

Gr[ä]{}tzer, G. (1978) [*[G]{}eneral [L]{}attice [T]{}heory*]{}, volume 75 of [*Pure and Applied Mathematics*]{}.  Academic Press, Inc. \[Harcourt Brace Jovanovich, Publishers\], New York-London. 

Gr[ä]{}tzer, G. (1979) [*Universal [A]{}lgebra*]{}.  Springer-Verlag, New York, second edition. 

Kleene, S. [*Introduction to [M]{}etamathematics*]{}.  D. Van Nostrand Co., Inc., New York, N. Y., 1952. 

Kuznetsov, A. (1985) The proof-intuitionistic propositional calculus. [* Soviet Mathematics-Doklady*]{}, 32(1):27–30. 

Kuznetsov, A. and Muravitsky, A. (1986) On superintuitionistic logics as fragments of proof logic extensions. [* Studia Logica*]{}, 45(1):77–99. 

Lambros, C. (1979) A shortened proof of [S]{}obociński’s theorem concerning a restricted rule of substitution in the field of propositional calculi. [* Notre Dame Journal of Formal Logic*]{}, 20(1):112–114. 

Maksimova, L. (1972) Pretabular superintuitionistic logics. [* Algebra and Logika*]{}, 11:308–314. 

Mal’cev, A. (1973) [*Algebraic [S]{}ystems*]{}.  Akademie-Verlag, Berlin.  Posthumous edition, edited by D. Smirnov and M. Ta[ĭ]{}clin, Translated from the Russian by B. D. Seckler and A. P. Doohovskoy. 

Muravitsky, A. (1985) Correspondence of proof-intuitionistic logic extensions to proof-logic extensions. [* Soviet Mathematics-Doklady*]{}, 31(2):345–348. 

Muravitsky, A. (1988) Algebraic proof of the separation property for the proof-intuitionistic calculus. [* Mathematics of the USSR-Sbornik*]{}, 59(2):397–406. 

Muravitsky, A. (1990) Magari and $\Delta$-pseudo-[B]{}oolean algebras. [* Siberian Mathematical Journal*]{}, 31(4):623–628. 

Muravitsky, A. (2008) The contribution of [A]{}. [ V]{}. [ K]{}uznetsov to the theory of modal systems and structures. [* Logic and Logical Philosophy*]{}, 17(1-2):41–58. 

Muravitsky, A. (2014) Logic [K]{}[M]{}: a biography.  In G. [B]{}ezhanishvili, editor, [*[L]{}eo [E]{}sakia on [D]{}uality in [M]{}odal and [I]{}ntuitionistic [L]{}ogics*]{}, pages 155–185.  Springer. 

Muravitsky, A. (2015a) Interconnection of the lattices of extensions of four logics. [* Log.  Univers.*]{},  11:253–281. 

Muravitsky, A. (2015b) On the equipollence of the calculi [I]{}nt and [K]{}[M]{}. [ URL]{} <http://arXiv.or/pdf/1702.00054>. 

Rasiowa, H. and Sikorski, R. (1970) [*The [M]{}athematics of [M]{}etamathematics*]{}.  PWN—Polish Scientific Publishers, Warsaw, third edition, Monografie Matematyczne, Tom 41. 

Rauszer, C. (1971/1972) Representation theorem for semi-Boolean algebras.  I, II. [* Bull.  Acad.  Polon.  Sci.  Sér.  Sci.  Math.  Astronom.  Phys.*]{},  19:881–887; ibid, 19:889–892. 

Soboci[ń]{}ski, B. (1974) A theorem concerning a restricted rule of substitution in the field of propositional calculi. [ I]{}, [II]{}. [* Notre Dame Journal of Formal Logic*]{}, 15:465–476; ibid.  15 (1974), 589–597. 

[^1]: The definitions of $\tau$ and $\rho$ can be found in [@mur85] or in [@mur14a], section 7.4.8. 

[^2]: See definitions in [@km86] or in [@mur14a], section 7.4.8. 

[^3]: Kuznetsov’s Theorem was generalized in [@mur15b], Proposition 4.2.  As a consequence of this generalization, the above diagram has recently been extended; cf.  [@mur15a]. 

[^4]: This axiomatization of ${\mbox{\textbf{KM}}}$ differs from the original one; see [@mur14a], section 7.4.1. 

[^5]: The two are equivalent not just because both are true, but deductively equivalent in a higher order logic. 

[^6]: The algebra ${\mbox{$\overset{{\rightarrow}}{{\mbox{$\mathfrak{A}$}}}$}}$ was employed in [@mur86] to prove the separation property for the proof-intuitionistic calculus.  Also, this algebra was used in our proof of the interpolation property for ${\mbox{\textbf{KM}}}$; cf.  [@mur14a], Section 7.4.7. 

[^7]: We avoid the term *Stone space* in this paper, because topology plays no part in our consideration. 

[^8]: This is also a consequence of a more general property: Any variety is closed under formation of direct limits; cf.  [@gor98], Theorem 1.2.9.  In Section \[S:reducibility\] we will refer to this Theorem again. 

[^9]: Compare with [@gra79], §21, Lemma 3. 

[^10]: The proof of Proposition \[P:equipollence\] is a modification of our proof of Kuznetsov’s Theorem in [@mur15b]. 

[^11]: The notation, ${\textbf{KM}_{\tau}}$, is justified by the formulas , Proposition \[P:bn-negation-1\] and the property Proposition \[P:bn-properties\].e. 

[^12]: The fact that ${\{y\in|{\mbox{$\mathfrak{A}$}}| ~|~y{\rightarrow}a\leq y\}}$ is a filter was established in [@esakia2006], Proposition 4. 

[^13]: The argument employed in this proof is a modification of one “hidden” in the proof of Lemma 5 of [@mak72]. 

[^14]: This property is stated in [@mak72], Lemma 5, but is not discussed there. 

[^15]: For definition, see e.g. [@gra79]. 

[^16]: Double Heyting algebras were studied perhaps for the first time in the doctoral dissertation of C. Rauszer, named there *semi-Boolean algebras*; cf.  [@rauszer1971].  Interest in these algebras became especially evident after S. Ghilardi proved in [@ghilardi1992] that every finitely generated free Heyting algebra is a bi-Heyting algebra. 

[^17]: See definitions e.g. in [@gra79]. 

[^18]: See the definition in [@mal73], p. 60.