# 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.

## Key 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.