On one embedding of Heyting algebras

TL;DR

This paper provides an algebraic interpretation of Kuznetsov's theorem by constructing an enrichable Heyting algebra that embeds the original, demonstrating their equivalence in generating the same variety of Heyting algebras.

Contribution

It introduces a new algebraic construction of an enrichable Heyting algebra that embeds any given Heyting algebra, linking algebraic properties to proof-theoretic equivalences.

Findings

The embedding preserves certain properties of the original algebra.

Both algebras generate the same variety of Heyting algebras.

The algebraic construction is equivalent to Kuznetsov's theorem.

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.

Equations

$$\text{mbox}Int+A⊢B⟺\text{mbox}KM+A⊢B,$$

$$\tau$$

$$\alpha \leftrightarrow \beta :=(\alpha \to \beta )\wedge (\beta \to \alpha ).$$

$$p\to \square p,(\square p\to p)\to p,\square p\to (q\vee (q\to p)),$$

$$\begin{array}[]{cl}(\text{a})&x\leq\square x,\\ (\text{b})&\square x\rightarrow x\leq x,\\ (\text{c})&\square x\leq y\vee(y\rightarrow x).\end{array}$$

$$\begin{array}[]{cl}(\text{a})&a\leq b,\\ (\text{b})&b\rightarrow a=a,\\ (\text{c})&b\leq x\vee(x\rightarrow a),~{}\textit{for any $x\in|\mbox{$\mathfrak{A}$}|$}.\end{array}$$

$$b\le b^{\prime }\vee (b^{\prime }\to a)=b^{\prime }\vee a=b^{\prime }.$$

$$\begin{array}[]{rl}\neg b\leq b\rightarrow a&\Leftrightarrow\neg b\leq a\\ &\Rightarrow\neg b\leq b\\ &\Leftrightarrow\neg b\leq\bm{0}.\end{array}$$

$$\mbox{$\mathfrak{A}$}\preccurlyeq\mbox{$\mathfrak{B}$}$$

$$L(\mbox{$\mathfrak{A}$})=\{A\in\mathfrak{F}_{\mathcal{L}}~{}|~{}v(A)=\bm{1},~{}\text{for any valuation $v$ in $\mbox{$\mathfrak{A}$}$}\}.$$

$$\mbox{$\mathfrak{A}$}\models\Gamma$$

$$\Gamma /\models A,$$

$$\Gamma \models A$$

$$\mbox{$\mathfrak{A}$}\models\Gamma\Longrightarrow\mbox{$\mathfrak{A}$}\models A.$$

$$\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,\\ \bm{0}=\emptyset~{}\text{and}~{}\bm{1}=\mathcal{S}_{\mathfrak{A}}.\end{array}$$

$$h_{\mathfrak{A}}(\overline{x})=\{F\in {\mathcal{S}}_{\mathfrak{A}}|x\notin F\},$$

$$\max h_{\mathfrak{A}}(\overline{x}),$$

$$\delta X=\{F\in {\mathcal{S}}_{\mathfrak{A}}|(\forall F^{\prime }\in {\mathcal{S}}_{\mathfrak{A}})(F\subset F^{\prime }\Rightarrow F^{\prime }\in X)\}.$$

$$\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 })\}.$$

$$h_{\mathfrak{A}}(\mbox{$\mathfrak{A}$})=\{h_{\mathfrak{A}}(x)~{}|~{}x\in|\mbox{$\mathfrak{A}$}|\}~{}\text{and}~{}\Delta_{\mathfrak{A}}=\{\delta h_{\mathfrak{A}}(x)~{}|~{}x\in|\mbox{$\mathfrak{A}$}|\}.$$

$$\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}$$

$$\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}$$

$$|x|=\{y|y\equiv x\},$$

$$|x|=|y|⟺x=y.$$

$$|x|\odot |y|=|{\phi }_{ij}(x)\odot y|,$$

$$\neg |x|=|\neg x|.$$

$$|x|\le |y|⟺\text{either i≤j and φij(x)≤jy, or j≤i and x≤iφji(y)},$$

$${\phi }_i:x\mapsto |x|,$$

$$\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\geq 0$}.\end{array}$$

$$X⋐Y$$

Full text

1. The history of one question

The present paper is about an algebraic interpretation of the main theorem of Kuznetsov (1985) by Alexander Kuznetsov. This theorem reads:

[TABLE]

where Int and 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 Kuznetsov and Muravitsky (1986) that the lattices of the normal extensions of Grz (Grzegorczyk logic), of GL (provability logic) and of the aforementioned logics Int and KM are connected by the following commutative diagram:

[TABLE]

where $\tau$ and $\rho$ are lattice isomorphisms and inverses of one another,111The definitions of $\tau$ and $\rho$ can be found in Muravitsky (1985) or in Muravitsky (2014), section 7.4.8. $\lambda$ and $\mu$ are meet epimorphisms222See definitions in Kuznetsov and Muravitsky (1986) or in Muravitsky (2014), section 7.4.8. 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.333Kuznetsov’s Theorem was generalized in Muravitsky (2015b), Proposition 4.2. As a consequence of this generalization, the above diagram has recently been extended; cf. Muravitsky (2015a).

1.1. Syntactic background

We will, at first, be dealing with formulas (alias terms) of two propositional languages, $\mathcal{L}_{a}$ and \mbox{\mathcal{L}}_{\square}. The language $\mathcal{L}_{a}$ is grounded on a denumerable set Var of propositional variables and the logical constants: $\wedge,\vee,\rightarrow$ and $\neg$. Unspecified $\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 $\mathcal{L}_{a}$. Regarding the sets of $\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 5.1, we will introduce two more extensions of $\mathcal{L}_{a}$. Let $\mathcal{L}$ be a propositional language which is an extension (not necessarily proper) of $\mathcal{L}_{a}$. A homomorphism of a formula algebra $\mathfrak{F}_{\mathcal{L}}$ into $\mathfrak{F}_{\mathcal{L}}$ is called a substitution. Metavariables for $\mathcal{L}$-formulas (or $\mathcal{L}$-terms) are $\alpha,\beta,\ldots$. As usual, we denote:

[TABLE]

Now Int can be defined as an $\mathcal{L}_{a}$-system given by any suitable axioms for intuitionistic propositional logic (see, e.g., Church (1956), § 26) and two inference rules, (uniform) substitution and modus ponens. KM is defined as an \mbox{\mathcal{L}}_{\square}-system by the axioms and inference rules of Int plus the following three formulas:

[TABLE]

where $p$ and $q$ are two distinct variables of Var.444This axiomatization of KM differs from the original one; see Muravitsky (2014), section 7.4.1.

1.2. 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., Rasiowa and Sikorski (1970), where those algebras are call pseudo-Boolean.)

Definition 1.1** (KM-algebra).**

An algebra \mbox{\mathfrak{A}}=\langle\mbox{\mathcal{A}},\wedge,\vee,\rightarrow,\square,\bm{0},\bm{1}\rangle is said to be a KM-algebra if \langle\mbox{\mathcal{A}},\wedge,\vee,\rightarrow,\bm{0},\bm{1}\rangle is a Heyting algebra (the Heyting reduct of $\mathfrak{A}$), with a least and greatest elements $\bm{0}$ (the zero) and $\bm{1}$ (the unit), respectively, and the unary operation $\square$ satisfies the following conditions:

[TABLE]

The universe $\mathcal{A}$ will often be denoted by |\mbox{\mathfrak{A}}|.

As was noted in Muravitsky (1990), if $\mathfrak{A}$ is a KM-algebra, the operation $\square$ is defined in $\mathfrak{A}$ uniquely. This gives rise to the following definition.

Definition 1.2** (enrichable element, enrichable Heyting algebra).**

Let $\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 $\mathfrak{A}$:

[TABLE]

A Heyting algebra is called enrichable if every element of this algebra is enrichable.

Proposition 1.1**.**

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

Proof.

For contradiction, we suppose that elements $b$ and $b^{\prime}$ enrich $a$, that is the properties (a)–(c) of Definition 1.2 are true for $b$ and $b^{\prime}$. Then we obtain:

[TABLE]

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 Rasiowa and Sikorski (1970), chapter IV, § 5.

Proposition 1.2**.**

If $a$ is enriched in $\mathfrak{A}$ with $b$, then the latter is dense; that is $\neg b=\bm{0}$.

Proof.

Indeed,

[TABLE]

∎

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. Muravitsky (2014), 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. Kuznetsov (1985), Corollary 1.) In fact, the last statement is equivalent to Kuznetsov’s Theorem.555The two are equivalent not just because both are true, but deductively equivalent in a higher order logic. However, Kuznetsov states another equivalent of his Theorem:

Every Heyting algebra $\mathfrak{A}$ is a subalgebra (up to isomorphism) of some enrichable Heyting algebra in the variety generated by $\mathfrak{A}$.

(Cf. Kuznetsov (1985), Corollary 2.)

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

[TABLE]

What do we know about $\mathfrak{B}$, besides its existence? According to Remark 3 of Muravitsky (2008), if $K$ is the class of all enrichable algebras of the variety generated by $\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 $\mathfrak{B}$, it is hardly possible to answer some natural questions about properties which can be preserved in $\mathfrak{B}$. For instance, grounding only on this membership, we do not know whether $\mathfrak{B}$ can be countable, providing that $\mathfrak{A}$ is; or whether $\mathfrak{B}$ can be subdirectly irreducible, if $\mathfrak{A}$ is.

In the remaining part of the paper, we show, given a Heyting algebra $\mathfrak{A}$, how to define such $\mathfrak{B}$ that the properties (A)–(B) are fulfilled. In fact, one possible candidate for $\mathfrak{B}$ has already been proposed in Muravitsky (1988), where we constructed algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}} (see definition in Section 2) which possesses the property (A).666The algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}} was employed in Muravitsky (1988) to prove the separation property for the proof-intuitionistic calculus. Also, this algebra was used in our proof of the interpolation property for KM; cf. Muravitsky (2014), Section 7.4.7.

Let $\mathcal{L}$ be an extension of $\mathcal{L}_{a}$. Given $\mathcal{L}$-algebras $\mathfrak{A}$ and $\mathfrak{B}$, we write

[TABLE]

if $\mathfrak{A}$ is a subalgebra (up to isomorphism) of $\mathfrak{B}$.

We conclude this section with the following definition.

Definition 1.3** (valuation, logic of algebra).**

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

[TABLE]

Given a language $\mathcal{L}$, an $\mathcal{L}$-algebra $\mathfrak{A}$ and any nonempty set $\Gamma$ of $\mathcal{L}$-formulas, we denote

[TABLE]

if \Gamma\subseteq L(\mbox{\mathfrak{A}}). And if $A$ is an $\mathcal{L}$-formula, we write

[TABLE]

if there is an $\mathcal{L}$-algebra $\mathfrak{A}$ such that \mbox{\mathfrak{A}}\models\Gamma and \mbox{\mathfrak{A}}\not\models A. Finally, we use

[TABLE]

in the usual sense:

[TABLE]

1.3. The structure of the present paper

In Section 2, given a Heyting algebra $\mathfrak{A}$, we define an algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}} which will play in the sequel the role of $\mathfrak{B}$ in the above conditions (A) and (B). We show (referring chiefly to Muravitsky (1988)) that \overset{\rightarrow}{\mbox{\mathfrak{A}}} satisfies (A). Also, we demonstrate some preservation properties over transition from $\mathfrak{A}$ to \overset{\rightarrow}{\mbox{\mathfrak{A}}} and state the main theorem (Theorem 2.1). In Section 3, we find a sufficient condition (Corollary 3.2.1) for the main theorem. This leads us to the idea of one-element enrichment. In Section 4 we develop an algebraic view on one-element enrichment and in Section 5 a proof-theoretic view on it. In Section 6 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 7. In Section 8 we make a final effort to complete the proof of Theorem 2.1. Thus, as the reader can see, this paper is devoted to the proof of one theorem. In Section 9 we formulate open questions about properties which \overset{\rightarrow}{\mbox{\mathfrak{A}}} may have, providing that $\mathfrak{A}$ possesses them.

2. Algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}}

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 Rasiowa and Sikorski (1970), Grätzer (1979), Gorbunov (1998), and Muravitsky (1988). We start with the following notions and notations.

• •

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

• •

Given a Heyting algebra $\mathfrak{A}$, $\mathcal{S}_{\mathfrak{A}}$ denotes both the set of all prime filters of $\mathfrak{A}$ and the poset $(\mathcal{S}_{\mathfrak{A}},\subseteq)$.777We avoid the term Stone space in this paper, because topology plays no part in our consideration. The filters of an algebra $\mathfrak{A}$ are called $\mathfrak{A}$-filters.

• •

Given an algebra $\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:

[TABLE]

• •

Given an algebra $\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 $\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

[TABLE]

for any x\in|\mbox{\mathfrak{A}}|. Further, we will find the usefulness of the set

[TABLE]

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 Muravitsky (1988), §1.

We start with the definition of operation $\delta$  in $\textsf{H}(\mathcal{S}_{\mathfrak{A}})$:

[TABLE]

In particular, for any particular a\in\mbox{\mathfrak{A}},

[TABLE]

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

Proposition 2.1** (Muravitsky (1988), Lemma 1).**

Let $\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})$.

Proposition 2.2** (Muravitsky (1988), Lemmas 3 and 4).**

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 $\delta h_{\mathfrak{A}}(x)$. Moreover, if an element a\in|\mbox{\mathfrak{A}}| is enriched in $\mathfrak{A}$ with an element $a^{\ast}$, then \delta h_{\mathfrak{A}}(a)=h(\mbox{a^{\ast}}).

We will be using the following notation:

[TABLE]

Then, we denote by \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 $\mathfrak{A}$, we define a denumerable sequence of algebras as follows:

[TABLE]

Along with the sequence \{\mbox{\mathfrak{A}}_{i}\}_{i<\mbox{\omega}}, we also have the embeddings:

[TABLE]

Thus the sequence \{\mbox{\mathfrak{A}}_{i}\}_{i<\mbox{\omega}} along with the embeddings $\varphi_{ij}$, $i\leq j$, form a direct family Grätzer (1979). Let \overset{\rightarrow}{\mbox{\mathfrak{A}}} be the direct limit of this family.

We remind the reader that the carrier of \overset{\rightarrow}{\mbox{\mathfrak{A}}} consists of the equivalence classes on \bigcup\{\mbox{\mathcal{A}}_{i}~{}|~{}i<\mbox{\omega}\}:

[TABLE]

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},

[TABLE]

Next we define:

[TABLE]

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:

[TABLE]

(Cf. Grätzer (1979) or Gorbunov (1998).)

Further, we define: For x\in\mbox{\mathcal{A}}_{i} and y\in\mbox{\mathcal{A}}_{j},

[TABLE]

where $\leq_{i}$ and $\leq_{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 \overset{\rightarrow}{\mbox{\mathfrak{A}}}.

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

\{\bm{1}_{i}~{}|~{}i<\mbox{\omega}\} is the unit of \overset{\rightarrow}{\mbox{\mathfrak{A}}}

and

\{\bm{0}_{i}~{}|~{}i<\mbox{\omega}\} is the zero of \overset{\rightarrow}{\mbox{\mathfrak{A}}}

Indeed, it is obvious that $\bm{1}_{i}\equiv\bm{1}_{j}$ and $\bm{0}_{i}\equiv\bm{0}_{j}$. Thus $|\bm{0}_{0}|\leq|x|\leq|\bm{1}_{0}|$.

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

Proposition 2.3**.**

\overset{\rightarrow}{\mbox{\mathfrak{A}}}* is a Heyting algebra.*

Proof follows from the definition of \overset{\rightarrow}{\mbox{\mathfrak{A}}} and the fact that each $\varphi_{ij}$ is an embedding. Also, we have to use (3).888This is also a consequence of a more general property: Any variety is closed under formation of direct limits; cf. Gorbunov (1998), Theorem 1.2.9. In Section 3 we will refer to this Theorem again.

Proposition 2.4**.**

Each \mbox{\mathfrak{A}}_{i} is embedded into \overset{\rightarrow}{\mbox{\mathfrak{A}}}.

Proof.

It is clear that the map

[TABLE]

where x\in\mbox{\mathfrak{A}}_{i} and i<\mbox{\omega}, is an embedding of \mbox{\mathfrak{A}}_{i} into \overset{\rightarrow}{\mbox{\mathfrak{A}}}. Indeed, $\varphi_{i}(x)=|\bm{1}_{i}|$ means $|x|=|\bm{1}_{i}|$. Then we apply (3). ∎

Also, we observe the following.

Proposition 2.5**.**

If $\mathfrak{A}$ is countable, then \overset{\rightarrow}{\mbox{\mathfrak{A}}} is countable as well.

Proof.

Since each \mbox{\mathfrak{A}}_{i} is countable, \overset{\rightarrow}{\mbox{\mathfrak{A}}} is also countable. ∎

Proposition 2.6**.**

If $\mathfrak{A}$ is subdirectly irreducible, so are each \mbox{\mathfrak{A}}_{i} and \overset{\rightarrow}{\mbox{\mathfrak{A}}}.

Proof.

Let $\omega$ be the pre-top element of $\mathfrak{A}$. Algebra $\textsf{H}(\mathcal{S}_{\mathfrak{A}})$ is subdirectly irreducible, for h(\mbox{\omega}) is a pre-top element in it. Therefore, \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=\bm{1}_{i}$. Therefore, \{\mbox{\omega}_{i}~{}|~{}i<\mbox{\omega}\} is a pre-top element of \overset{\rightarrow}{\mbox{\mathfrak{A}}}. ∎

We want to show that \overset{\rightarrow}{\mbox{\mathfrak{A}}} is enrichable. We will do it by employing the following lemma.

Lemma 2.1** (Muravitsky (1988), Corollary 2).**

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 \overset{\rightarrow}{\mbox{\mathfrak{A}}}.

Proposition 2.7**.**

Algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}} is enrichable.

Proof.

Let x\in|\mbox{\mathfrak{A}}_{i}|. Then $h_{\mathfrak{A}_{i}}(x)$ is enriched with $\delta h_{\mathfrak{A}_{i}}(x)$ in \mbox{\mathfrak{A}}_{i+1}. It remains to apply Lemma 2.1. ∎

In this paper we aim to prove the following theorem.

Theorem 2.1**.**

Given a Heyting algebra $\mathfrak{A}$, the algebras $\mathfrak{A}$ and \overset{\rightarrow}{\mbox{\mathfrak{A}}} generate one and the same variety. In other words, $\mathfrak{A}$ and \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}$}}}).

3. Reduction to one-element enrichment

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

Proposition 3.1**.**

Given an algebra $\mathfrak{A}$, the following conditions are equivalent$:$

[TABLE]

Proof.

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 Gorbunov (1998), Theorem 1.2.9, \overset{\rightarrow}{\mbox{\mathfrak{A}}} is a subalgebra of ultraproduct of some of \mbox{\mathfrak{A}}_{i}’s and hence generates the same variety. ∎

Corollary 3.1.1**.**

A sufficient condition for Theorem 2.1 is that for any Heyting algebra $\mathfrak{A}$, L(\mbox{\mathfrak{A}})=L(\mbox{\delta[\mbox{$\mathfrak{A}$}]}).

Proof.

Indeed, if L(\mbox{\mathfrak{A}})=L(\mbox{\delta[\mbox{$\mathfrak{A}$}]}), for any algebra $\mathfrak{A}$, then starting from an algebra \mbox{\mathfrak{A}}=\mbox{\mathfrak{A}}_{0}, we obtain the condition (b) of Proposition 3.1. ∎

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

• •

Given two sets $X$ and $Y$,

[TABLE]

denotes that $X$ is a finite subset of $Y$.

• •

Let $\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=\{a\}$, the subalgebra of \delta[\mbox{\mathfrak{A}}] generated by |h_{\mathfrak{A}}(\mbox{\mathfrak{A}})|\cup\{\delta h_{\mathfrak{A}}(x)~{}|~{}x\in X\}.

Proposition 3.2**.**

Given an algebra $\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}$}}}).

Proof.

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}}].999Compare with Grätzer (1979), §21, Lemma 3. Thus, by virtue of Gorbunov (1998), 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 3.1.1. ∎

Corollary 3.2.1**.**

A sufficient condition for Theorem 2.1 is that, given a Heyting algebra $\mathfrak{A}$, for any a\in|\mbox{\mathfrak{A}}|, L(\mbox{\mathfrak{A}})=L(\delta[\mbox{\mathfrak{A}}_{a}]).

Proof.

Suppose for any algebra $\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 Muravitsky (1990), Lemma 5, the algebras \delta[\mbox{\mathfrak{A}}_{\{a,b\}}] 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}}_{\{a,b\}}]). 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 3.2. ∎

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

4. One-element enrichment from an algebraic viewpoint

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

Definition 4.1** ($\mathcal{E}$-pair, relation $\mathcal{E}$).**

Given an algebra $\mathfrak{A}$ and a,\mbox{a^{\ast}}\in|\mbox{\mathfrak{A}}|, (a,\mbox{a^{\ast}}) is an $\mathcal{E}$-pair $($in \mathfrak{A}$$) if $a$ is enriched with $a^{\ast}$ in $\mathfrak{A}$. Then, we define:**

[TABLE]

We will drop the subscript ‘$\mathfrak{A}$’ and write simply ‘$\mathcal{E}$’ when confusion is unlikely.

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

Definition 4.2** ($\sim$-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:

[TABLE]

Sometimes, it will be convenient, instead of \mbox{\sim}x, to write $t(x)$ (perhaps with a subscript at ‘$\sim$’ and ‘$t$’).

It is obvious that in any Heyting algebra with $\sim$-negation, the following quasi-identity holds:

[TABLE]

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

Proposition 4.1**.**

The following properties hold in any Heyting algebra with $\sim$-negation.

[TABLE]

Proof.

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

(b): From (a) just proved we have: \mbox{\sim}\bm{1}\leq\mbox{\sim}x and \mbox{\sim}\bm{1}\leq\mbox{\sim}\mbox{\sim}x and hence \mbox{\sim}\bm{1}\leq\mbox{\sim}x\wedge\mbox{\sim}\mbox{\sim}x. And by virtue of Definition 4.2.b, we get \mbox{\sim}x\wedge\mbox{\sim}\mbox{\sim}x=\mbox{\sim}\bm{1}.

(c): According to (a) above, \mbox{\sim}x\leq\mbox{\sim}\bm{0} and \mbox{\sim}\mbox{\sim}x\leq\mbox{\sim}\bm{0} and hence \mbox{\sim}x\vee\mbox{\sim}\mbox{\sim}x\leq\mbox{\sim}\bm{0}. Then, with help of Definition 4.2.c, we get \mbox{\sim}x\vee\mbox{\sim}\mbox{\sim}x=\mbox{\sim}\bm{0}.

(d): Using (a) above twice and, then, (b), we obtain:

[TABLE]

(e): We use (c) and (a) twice to obtain:

[TABLE]

(f): Using (c) and (b) above and Definition 4.2.d, we get:

[TABLE]

(g): We obtain:

[TABLE]

(h): Using (4), (a) and (d), we receive:

[TABLE]

(i): In virtue of Definition 4.2.b and (a), we have: \mbox{\sim}x\leq(x\rightarrow\mbox{\sim}\bm{1})\wedge\mbox{\sim}\bm{0}.

In virtue of Definition 4.2.a, we have: (x\rightarrow\mbox{\sim}\bm{1})\wedge\mbox{\sim}\mbox{\sim}\bm{1}\leq\mbox{\sim}x. Then, we use (e) to get (x\rightarrow\mbox{\sim}\bm{1})\wedge\mbox{\sim}\bm{0}\leq\mbox{\sim}x.

(j): With help of (i), we get:

[TABLE]

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

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

Corollary 4.1.1**.**

Given a $\sim$-negation, (\mbox{\sim}\bm{1},\mbox{\sim}\bm{0}) is an $\mathcal{E}$-pair. Hence \neg\mbox{\sim}\bm{0}=\bm{0}.

Proof.

Indeed, from Proposition 4.1.a, we derive that \mbox{\sim}\bm{1}\leq\mbox{\sim}\bm{0}. And Definition 4.2.d gives us \mbox{\sim}\bm{0}\rightarrow\mbox{\sim}\bm{1}\leq\mbox{\sim}\bm{1}. Further, in virtue of Definitions 4.2.c and 4.2.b, we obtain that \mbox{\sim}\bm{0}\leq x\vee(x\rightarrow\mbox{\sim}\bm{1}).

The equality \neg\mbox{\sim}\bm{0}=\bm{0} follows from Proposition 1.2 ∎

Corollary 4.1.2**.**

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

Proof.

Assume that \mbox{\sim}_{1}\bm{1}=\mbox{\sim}_{2}\bm{1}. In view of Proposition 4.1.i, we need to show that \mbox{\sim}_{1}\bm{0}=\mbox{\sim}_{2}\bm{0}. According to Corollary 4.1.1, both pairs (\mbox{\sim}_{1}\bm{1},\mbox{\sim}_{1}\bm{0}) and (\mbox{\sim}_{2}\bm{1},\mbox{\sim}_{2}\bm{0}) belong to \mbox{\mathcal{E}}_{\mathfrak{A}}. In virtue of Proposition 1.1, \mbox{\sim}_{1}\bm{0}=\mbox{\sim}_{2}\bm{0}. The converse is obvious. ∎

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

Proposition 4.2**.**

Given a Heyting algebra $\mathfrak{A}$, if (a,\mbox{a^{\ast}}) is an $\mathcal{E}$-pair, then the operation

[TABLE]

is a $\sim$-negation in $\mathfrak{A}$ so that a=\mbox{\sim}\bm{1} and \mbox{a^{\ast}}=\mbox{\sim}\bm{0}.

Proof.

We have to check that the definition of \mbox{\sim}x above satisfies the properties (a)–(d) of Definition 4.2.

(a): In any Heyting algebra, the following holds:

[TABLE]

(b): We also have:

[TABLE]

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

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

The last proposition inspires the next definition.

Definition 4.3** ($t_{\varepsilon}$-negation, $\varepsilon_{t}$ pair).**

Given an $\mathcal{E}$-pair $\varepsilon=(a,a^{\ast})$ in a Heyting algebra, we define a $\sim$-negation as follows:

[TABLE]

On the other hand, given a $\sim$-negation $t(x)$, we denote $\varepsilon_{t}=(t(\bm{1}),t(\bm{0}))$.

Proposition 4.3**.**

If $t(x)$ is a $\sim$-negation, then

[TABLE]

If $\varepsilon=(a,a^{\ast})$ is an $\mathcal{E}$-pair, then

[TABLE]

Proof.

According to Definition 4.3 and Proposition 4.1.i,

[TABLE]

Further, according to Definition 4.3 and Proposition 4.2,

[TABLE]

∎

Corollary 4.3.1**.**

Given a Heyting algebra $\mathfrak{A}$, there is a one-one correspondence between \mbox{\mathcal{E}}_{\mathfrak{A}} and $\sim$-negations in $\mathfrak{A}$.

Definition 4.4** ($\sim$-expansion, Heyting reduct, class $K$).**

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

Proposition 4.4**.**

Class $K$ is a variety.

Proof follows immediately from Definition 4.2.

Proposition 4.5**.**

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

Proof follows straightforwardly from Definition 4.2.a.

In the sequel, we will use the last proposition without reference.

So far, talking about one-element enrichment in this section, we introduced $\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.

Definition 4.5** ($\tau$-expansion, \tau\mbox{\sim}-expansion, classes $K_{\tau}$ and $K^{\ast}_{\tau}$).**

Let $\mathfrak{A}$ be a Heyting algebra. We enrich the signature of $\mathfrak{A}$ with a nullary operation $\tau$ and call \mbox{\mathfrak{A}}_{\tau}=(\mbox{\mathfrak{A}},\tau) a $\tau$-expansion of $\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 $\sim$-expansion of \mbox{\mathfrak{A}}_{\tau} that satisfies the identity \mbox{\sim}\bm{1}=\tau is called a \tau\mbox{\sim}-expansion $($of \mathfrak{A}$$), in symbols (\mbox{\mathfrak{A}}_{\tau},\mbox{\sim}). In \mbox{\mathfrak{A}}_{\tau} and (\mbox{\mathfrak{A}}_{\tau},\mbox{\sim}), $\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.

Proposition 4.6**.**

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

In Section 5, 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 $\mathcal{L}_{\tau}$-formulas is a subvariety of $K^{\ast}_{\tau}$.

Definition 4.6** (packing, relation $\vartriangleleft$).**

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. $\sim$ and as such is a relative subalgebra of a $($full$)$ algebra (\mbox{\mathfrak{B}}_{\tau},\mbox{\sim}) $($in the sense of Grätzer (1979), §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}).

Proposition 4.7**.**

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\{\mbox{\sim}\bm{0}\}. 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\{\mbox{\sim}\bm{0}\}, then (\mbox{\mathfrak{A}}_{\tau},\mbox{\sim})\vartriangleleft(\mbox{\mathfrak{B}}_{\tau},\mbox{\sim}).

Proof.

The first part follows straightforwardly by the property Proposition 4.1.i. The second part is obvious. ∎

Proposition 4.8**.**

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$:$

[TABLE]

Proof.

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

Then, $(\text{b})\Rightarrow(\text{c})$ follows straightforward from Proposition 4.1.c.

Now we prove $(\text{c})\Rightarrow(\text{a})$. Since, by premise, \mbox{\sim}\bm{1}\in\mbox{\mathfrak{A}}_{\tau}, we use Proposition 4.1.i. ∎

Proposition 4.9**.**

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:

[TABLE]

Proof.

The conditional $(\text{a})\Rightarrow(\text{b})$ is obvious. Next, assume that (b) is true. Then, by virtue of Proposition 4.1.e,

[TABLE]

thus (c) is true. Finally, suppose that \mbox{\sim}_{1}\tau=\mbox{\sim}_{2}\tau. The latter,as above, implies that

[TABLE]

Then, we apply Proposition 4.1 ∎

Let $\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}),\delta h(\tau_{a}))$ is an $\mathcal{E}$-pair (Proposition 2.2). Thus, by adding of the $\sim$-negation to \delta[\mbox{\mathfrak{A}}_{\tau_{a}}], corresponding to this $\mathcal{E}$-pair, in the way provisioned in Proposition 4.2, we obtain a \tau\mbox{\sim}-expansion. Moreover, by virtue of Proposition 4.7, (\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.

Proposition 4.10**.**

Given a Heyting algebra $\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 4.6).

5. One-element enrichment from a proof-theoretic viewpoint

In this section we prove an analog of Kuznetsov’s Theorem (Proposition 5.2), where in place of $\square$ the connective $\sim$ is used.101010The proof of Proposition 5.2 is a modification of our proof of Kuznetsov’s Theorem in Muravitsky (2015b). We need it to derive an analog of Kuznetsov’s Corollary 2 mentioned on p. 1.2, which is obtained as Corollary 6.2.1.

5.1. The $\mathcal{L}_{\tau}$-equipollence of two calculi

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

[TABLE]

Calculus $\textbf{Int}_{\tau}$ is defined in the language $\mathcal{L}_{\tau}$, while the calculi $\textbf{Int}_{\tau\sim}$ and $\textbf{KM}_{\tau}$ are defined in the language $\mathcal{L}_{\tau\sim}$. The calculus $\textbf{Int}_{\tau}$ is Int in the language $\mathcal{L}_{\tau}$. The calculus $\textbf{Int}_{\tau\sim}$ is defined by the axioms of Int in the language $\mathcal{L}_{\tau\sim}$. The calculus $\textbf{KM}_{\tau}$ is $\textbf{Int}_{\tau\sim}$ plus the following formulas:

[TABLE]

The postulated inference rules of all calculi under consideration are (uniform) substitution and modus ponens.111111The notation, $\textbf{KM}_{\tau}$, is justified by the formulas (1), Proposition 4.2 and the property Proposition 4.1.e.

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 $\mathcal{L}_{\tau}$ of a formula $B^{\ast}$ from axioms of Int and a formula $A^{\ast}$ as a premise by using substitution of $\mathcal{L}_{\tau}$-formulas and modus ponens..

• •

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

• •

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

If a derivation $\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 $\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.

Definition 5.1** (refined derivation).**

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. Sobociński (1974); Lambros (1979).)

Suppose $S=\{\alpha_{1},\ldots,\alpha_{n}\}$ is a finite set of $\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 $\mathcal{L}_{\tau\sim}$-formulas.

Definition 5.2** (pure derivation, $\Vdash$).**

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 $\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 5.2 and Corollary 5.2.1. We will reach this goal through the following key, though auxiliary, notion.

Definition 5.3** (relation $\ll$, set $\mathcal{I}$, root $r_{0}$).**

Let $\mathbb{N}$ be the set of nonnegative numbers. Then we arrange the pairs of $\mathbb{N}^{2}$ by the following relation:

[TABLE]

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.

Proposition 5.1**.**

The poset $\mathcal{I}$ satisfies the descending chain condition Grätzer (1978).

Proof.

First we notice that

[TABLE]

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 (5), 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$. ∎

Definition 5.4** (down-complete chains in $\mathcal{I}$).**

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

Definition 5.5** (rank of derivation, $\vdash_{s}$).**

We say that a refined derivation $\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

[TABLE]

Given formulas $\alpha$, $\beta$ and $\gamma$, we denote by

[TABLE]

the result of replacement of all occurrences of $\beta$ in $\alpha$ with $\gamma$.

Lemma 5.1**.**

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}})=\{\sim\!A^{\ast}_{1},\ldots,\sim\!A^{\ast}_{n}\}, for some formulas $A^{\ast}_{1},\ldots,A^{\ast}_{n}$, and $\gamma=A^{\ast}_{i}$, then M(\mbox{\mathcal{D}}^{\ast})=\{\sim\!A^{\ast}_{1},\ldots,\sim\!A^{\ast}_{i-1},\sim\!A^{\ast}_{i+1},\sim\!\tau\}, in which case $s=t=(1,n)$;**

• •

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

Proof.

Let us denote by

[TABLE]

the given derivation. Obviously, $\gamma_{n}=\beta$. Then, we define:

[TABLE]

We notice that $\delta$ does not contain $\sim\!\gamma$. Further, we define:

[TABLE]

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 Int-axiom. Then $\gamma_{i}^{\ast}$ is also an instance of the same 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 $\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

[TABLE]

Now we denote:

[TABLE]

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\leq m_{1}<m$ and some $n_{1}\geq 1$. We observe that in both cases $t\ll s$ and $t\neq s$. ∎

Lemma 5.2**.**

Let \mbox{\mathcal{D}}:\textbf{KM}_{\tau}+\alpha\vdash\beta be a refined derivation such that M(\mbox{\mathcal{D}})=\{\sim\!\tau\}. 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}]$.

Proof.

Assume that the formulas

[TABLE]

are all the instances of the axiom (c) in the refined derivation $\mathcal{D}$. Then, we define:

[TABLE]

Thus, if the list (6) is nonempty, then we denote:

[TABLE]

for some $\sim$-free formulas $B^{\ast}_{1},\ldots,B^{\ast}_{k}$.

Further, we denote:

[TABLE]

Now we consider the following cases.

Case 1: $\gamma_{i}$ is an instance of an Int-axiom. Then $\gamma_{i}^{\ast}$ is also an instance of the same 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 (6) 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 (6) is nonempty, then $\gamma_{i}^{\ast}=(\bigwedge_{1\leq j\leq k}(B^{\ast}_{j}\vee(B^{\ast}_{j}\rightarrow\tau))\rightarrow\tau)\rightarrow\tau$. Then we observe:

[TABLE]

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., Kleene (1956), § 26)

[TABLE]

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\leq j\leq 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:

[TABLE]

Further, we denote:

[TABLE]

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

Proposition 5.2**.**

The calculi $\textbf{KM}_{\tau}$ and $\textbf{Int}_{\tau}$ are $\mathcal{L}_{\tau}$-equipollent;* that is, for any $\mathcal{L}_{\tau}$-formulas $A^{\ast}$ and $B^{\ast}$,*

[TABLE]

Proof.

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\geq 1$. Using Lemma 5.1, 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})=\{\mbox{\sim}\tau\}. Then, we apply Lemma 5.2, to get $\textbf{KM}_{\tau}+A^{\ast}\Vdash B^{\ast}$. The latter means that $\textbf{Int}_{\tau}+A^{\ast}\vdash B^{\ast}$. ∎

Corollary 5.2.1**.**

For any set $\Gamma$ of $\mathcal{L}_{\tau}$-formulas and any $\mathcal{L}_{\tau}$-formula $A^{\ast}$, the following equivalence holds:**

[TABLE]

Proof follows immediately from Proposition 5.2.

5.2. Completeness of $\textbf{KM}_{\tau}$

We intend to prove the following.

Proposition 5.3**.**

For any $\mathcal{L}_{\tau\sim}$-formula $\alpha$, $\textbf{KM}_{\tau}\vdash\alpha$ if, and only if, any \tau\mbox{\sim}-expansion validates $\alpha$.

Proof.

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:

[TABLE]

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 4.2 are true but also \mbox{\sim}\bm{1}=\tau (Definition 4.5). The latter and Proposition 4.1.e imply that \mbox{\sim}\bm{0}=\mbox{\sim}\tau. And, by virtue of Corollary 4.1.1, we conclude that (\tau,\mbox{\sim}\tau) is an $\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 4.3, $(\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 $\mathcal{E}$-pair in \mbox{\mathfrak{A}}_{\tau}. According to Proposition 4.2, \mbox{\sim}x is a $\sim$-negation in \mbox{\mathfrak{A}}_{\tau} and \tau=\mbox{\sim}\bm{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.

Corollary 5.3.1**.**

Let $\Lambda\cup\{\alpha\}$ be a set of $\mathcal{L}_{\tau\sim}$-formulas. Then

[TABLE]

Also, we obtain the following.

Corollary 5.3.2**.**

The class $K_{\tau}^{\ast}$ is a variety. Moreover, for any $\mathcal{L}_{\tau}$-formula $A^{\ast}$,

[TABLE]

Proof.

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

Now, using Corollary 5.2.1 with $\Gamma=\emptyset$ and Proposition 5.3, we receive the equivalence above. ∎

6. Connecting the two viewpoints on one-element enrichment

We connect the two viewpoints discussed above in Sections 4 and 5 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 $\mathcal{L}_{\tau}$.

Proposition 6.1**.**

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

Proof.

Let

[TABLE]

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 5.3.1, $\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}}. ∎

Proposition 6.2**.**

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}).

Proof.

Let $\mathcal{V}$ be the variety of the $\tau$-expansions generated by \mbox{\mathfrak{A}}_{\tau}. According to Proposition 6.1, \mbox{\mathfrak{A}}_{\tau}\in\mathbf{H}\mathbf{S}\mathbf{P}(\mbox{\mathcal{V}}\cap K^{\ast}_{\tau}). In view of Proposition 4.5, 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

[TABLE]

is preserved under formation of direct products and homomorphic images; cf. Mal’cev (1973), 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 4.2, a $\sim$-negation can be defined in \mbox{\mathfrak{C}}_{\tau} so that \mbox{\sim}\bm{1}=\tau. It remains to notice that L(\mbox{\mathfrak{A}}_{\tau})=L(\mbox{\mathfrak{C}}_{\tau}). ∎

Corollary 6.2.1**.**

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}).

Proof.

Let (\mbox{\mathfrak{C}}_{\tau},\mbox{\sim}) be a \tau\mbox{\sim}-expansion from Proposition 6.2. Let (\mbox{\mathfrak{B}}_{\tau},\mbox{\sim}) be the subalgebra of (\mbox{\mathfrak{C}}_{\tau},\mbox{\sim}) generated by |\mbox{\mathfrak{A}}|\cup\{\tau\}. 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 6.2. ∎

Our goal is to prove the following.

Conjecture 6.1**.**

Let $\mathfrak{A}$ and $\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 $\mathcal{E}$-pair in $\mathfrak{B}$. Then, if \mbox{\mathfrak{A}}_{\tau_{a}}\mbox{\vartriangleleft}\mbox{\mathfrak{B}}_{\tau_{a}}, then $\mathfrak{B}$ is isomorphic to \delta[\mbox{\mathfrak{A}}_{a}].

7. Properties related to Stone embedding

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.

7.1. Some filters of Heyting algebra

In this subsection we use Rasiowa and Sikorski (1970) as a main reference, though employed implicitly.

Let us fix a Heyting algebra $\mathfrak{A}$ and an element a\in|\mbox{\mathfrak{A}}|. Then, we define:

[TABLE]

Proposition 7.1**.**

$X_{a}$* is a filter of $\mathfrak{A}$. Moreover, $X_{a}$ is proper if and only if $a\neq\bm{1}$.*

Proof.

Suppose $x_{1},x_{2}\in X_{a}$, that is, $x_{1}\rightarrow a=a$ and $x_{2}\rightarrow a=a$. Then we have:

[TABLE]

Next let $x\rightarrow a=a$, and $y\geq x$. Then we obtain:

[TABLE]

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

Now we define

[TABLE]

Proposition 7.2**.**

For any Heyting algebra $\mathfrak{A}$ and element a\in|\mbox{\mathfrak{A}}|, the following conditions are equivalent:

[TABLE]

Proof.

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,

[TABLE]

$(\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)$. ∎

Corollary 7.2.1**.**

$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 $\mathfrak{A}$ is nontrivial.121212The fact that \{y\in|\mbox{\mathfrak{A}}|~{}|~{}y\rightarrow a\leq y\} is a filter was established in Esakia (2006), Proposition 4.*

7.2. Some properties of Stone embedding

The main references here are Rasiowa and Sikorski (1970), though implicitly,  Maksimova (1972) (see also Gabbay and Maksimova (2005)) and also Muravitsky (1988), §1.

Let \mbox{\mathfrak{A}}\preccurlyeq\mbox{\mathfrak{B}}. We define:

[TABLE]

We note the following property:

[TABLE]

Proposition 7.3**.**

Let $\mathfrak{A}$ and $\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}}|.

Proof.

131313The argument employed in this proof is a modification of one “hidden” in the proof of Lemma 5 of Maksimova (1972).

First, we define the filter $[F)_{\mathfrak{B}}$ and note that [F)_{\mathfrak{B}}\cap|\mbox{\mathfrak{A}}|=F. Thus the set

[TABLE]

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\{x\})_{\mathfrak{B}}$ and $H_{2}:=[G\cup\{y\})_{\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})$. ∎

Corollary 7.3.1** (comp. Maksimova (1972), Lemma 5).**

Let $\mathfrak{A}$ and $\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.141414This property is stated in Maksimova (1972), Lemma 5, but is not discussed there.

Proof.

We apply Proposition 7.3 for $a=\bm{0}$. ∎

Corollary 7.3.2**.**

Let $\mathfrak{A}$ and $\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)$.

Proof.

For any x\in|\mbox{\mathfrak{A}}|, we obtain:

[TABLE]

∎

Proposition 7.4** (folklore).**

Let $\mathfrak{A}$ and $\mathfrak{B}$ be Heyting algebras with \mbox{\mathfrak{A}}\preccurlyeq\mbox{\mathfrak{B}}. Also, let $F$ be an $\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 $\mathfrak{A}$ and $\mathfrak{B}$ coincide, then there is a filter $G\in\max h_{\mathfrak{A}}(\overline{a})$ such that $F\subseteq G$. (Part 2)

Proof.

We define the set:

[TABLE]

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 $\mathfrak{A}$, $x\lor y\in G$ but neither $x\in G$ nor $y\in G$. Next, we define $H_{1}:=[G\cup\{x\})_{\mathfrak{B}}$ and $H_{2}:=[G\cup\{y\})_{\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\leq x\rightarrow a$ and $v\leq 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})$ ∎

Corollary 7.4.1**.**

Let $\mathfrak{A}$ and $\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}).

Proof.

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 $\mathfrak{A}$-filter $F$ with G\cap|\mbox{\mathfrak{A}}|\subset F. For contradiction, assume that $a\notin F$. Then, we define a $\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\leq 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 7.4 (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}). ∎

Corollary 7.4.2**.**

Let $\mathfrak{A}$ and $\mathfrak{B}$ be Heyting algebras such that \mbox{\mathfrak{A}}\preccurlyeq\mbox{\mathfrak{B}} and let a\in|\mbox{\mathfrak{A}}|. For any $\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}}|.

Proof.

Let $G$ be a $\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 7.4 (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. ∎

Corollary 7.4.3**.**

Let $\mathfrak{A}$ and $\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})$.

Proof.

Assume that $G\in\max h_{\mathfrak{B}}(\overline{a})$. Then, according to Corollary 7.4.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 7.4, 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}))$. ∎

Proposition 7.5**.**

Let $\mathfrak{A}$ and $\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 $\mathcal{E}$-pair in $\mathfrak{B}$. Then \widetilde{\varphi}(h_{\mathfrak{B}}(\mbox{a^{\ast}}))=\delta h_{\mathfrak{A}}(a).

Proof.

Indeed, we obtain:

[TABLE]

∎

Proposition 7.6**.**

Let $\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$.

Proof.

First, we note that if $a=\bm{1}$, then the proposition is trivially true. Thus we assume that $a\neq\bm{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 7.2) and $x\vee(x\rightarrow a)\not\in F$ (since $F$ is a prime filter). Now we define a filter $G:=[F\cup\{x\vee(x\rightarrow a)\})_{\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))\leq a$, that is $(x\vee(x\rightarrow a))\rightarrow(y\rightarrow a)=\bm{1}$. The latter implies that $(x\rightarrow(y\rightarrow a))\wedge((x\rightarrow a)\rightarrow(y\rightarrow a))=\bm{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 7.4, 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. ∎

Proposition 7.7**.**

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 $\mathfrak{B}$, where F_{a}:=\{x\in|\mbox{\mathfrak{A}}|~{}|~{}x\rightarrow a\leq x\}, then \bigwedge\!F_{a}=\mbox{a^{\ast}} in $\mathfrak{B}$.

Proof.

Let us denote $u:=\bigwedge\!F_{a}$. We note that \mbox{a^{\ast}}\leq x, for every $x\in F_{a}$ (Section 7.1). Hence \mbox{a^{\ast}}\leq u. For contradiction, assume that u\not\leq\mbox{a^{\ast}}. Then $a\notin[u)_{\mathfrak{B}}$. In virtue of Propositional 7.4 (part 2), there is a filter $G\in\max h_{\mathfrak{B}}(\overline{a})$ such that $[u)_{\mathfrak{B}}\subseteq G$. According to Proposition 7.6, 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}}. ∎

Corollary 7.7.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\leq x\}.

Proof.

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 $\mathcal{E}$-pair in $\textsf{H}(\mathcal{S}_{\mathfrak{B}})$ (Proposition 2.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}}]. ∎

Corollary 7.7.2**.**

Let $\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\leq x\}, is true in \delta[\mbox{\mathfrak{A}}_{a}].

Proof.

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 $\mathcal{E}$-pair in $\textsf{H}(\mathcal{S}_{\mathfrak{A}})$ (Proposition 2.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 7.7, 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}]. ∎

8. Completing the proof of Theorem 2.1

We aim to prove Conjecture 6.1, from which Theorem 2.1 will follow straightforwardly.

Let $\mathfrak{A}$ and $\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

[TABLE]

Indeed, this follows from that the map $\varphi$ is surjective (Corollary 7.3.1).

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. Maksimova (1972), Lemma 2.

The following observation is obvious: For any $\mathcal{U}\in\textsf{H}(\mathcal{S}_{\mathfrak{B}})$,

[TABLE]

Also, it is easy to see that

[TABLE]

Indeed, we have:

[TABLE]

Now, assume that a\in|\mbox{\mathfrak{A}}| and (a,\mbox{a^{\ast}}) is an $\mathcal{E}$-pair in $\mathfrak{B}$. Then

[TABLE]

Indeed, with the help of (9) and Proposition 7.5, we obtain:

[TABLE]

Finally, since $\delta h_{\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 2.2), using (10), we conclude that $\varphi^{-1}(\delta h_{\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 7.7.1, we obtain that

[TABLE]

Further, with the help of (10) and (12), we derive the statement of Conjecture 6.1.

At last, using Conjecture 6.1 and Corollary 6.2.1, we obtain that L(\mbox{\mathfrak{A}})=L(\delta[\mbox{\mathfrak{A}}_{a}]). Thus the condition of Corollary 3.2.1 is satisfied and hence Theorem 2.1 is proven.

9. Discussion

We have proved that, given a Heyting algebra $\mathfrak{A}$, the algebra \overset{\rightarrow}{\mbox{\mathfrak{A}}} defines the same equational class as $\mathfrak{A}$ does. (Theorem 2.1) In addition, \overset{\rightarrow}{\mbox{\mathfrak{A}}} can inherit some algebraic and cardinality properties, if $\mathfrak{A}$ has them. (Propositions 2.5 and 2.6) In view of all these properties, we formulate several open questions, dividing them into two problem sets.

Problem set 1

(a) Is \overset{\rightarrow}{\mbox{\mathfrak{A}}} finitely subdirectly irreducible, providing that $\mathfrak{A}$ is? 151515For definition, see e.g. Grätzer (1979).

(b) Is \overset{\rightarrow}{\mbox{\mathfrak{A}}} a double Heyting algebra (alias bi-Heyting algebra), providing that $\mathfrak{A}$ is? 161616Double Heyting algebras were studied perhaps for the first time in the doctoral dissertation of C. Rauszer, named there semi-Boolean algebras; cf. Rauszer (1971/1972). Interest in these algebras became especially evident after S. Ghilardi proved in Ghilardi (1992) that every finitely generated free Heyting algebra is a bi-Heyting algebra.

(c) Is \overset{\rightarrow}{\mbox{\mathfrak{A}}} projective $($weakly projective$)$, providing that $\mathfrak{A}$ is? 171717See definitions e.g. in Grätzer (1979).

(d) Is \overset{\rightarrow}{\mbox{\mathfrak{A}}} finitely approximable, providing that $\mathfrak{A}$ is? 181818See the definition in Mal’cev (1973), p. 60.

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 \overset{\rightarrow}{\mbox{\mathfrak{A}}}.

Problem set 2

(a) *Do \overset{\rightarrow}{\mbox{\mathfrak{A}}} and $\mathfrak{A}$ have the same quasi-equational theory?

*(b) Which elementary properties are preserved in \overset{\rightarrow}{\mbox{\mathfrak{A}}}?