Погружение импликативного фрагмента классической логики в импликативный фрагмент интуиционистской.

Abstract

A translation from the calculus $Cl_\supset$ which is a formalization of the implicative fragment of classical logic to the calculus $Int_\supset$ which is a formalization of the implicative fragment of intuitionistic logic is constructed. This translation is such that for all formulas $A$ the following condition is satisfied: a formula $A$ is deducible in $Cl_\supset$ iff the translation of $A$ is deducible in $Int_\supset$.