Algebraic proof of the separation property for an intuitionistic provability calculus

For intuitionistic provability calculus $I^\Delta$ obtained from the intuitionistic propositional calculus by adjoining to the postulates of the latter the axioms $(p\supset\Delta p)$, $((\Delta p\supset p)\supset p)$ and $(\Delta p\supset(((q\supset p)\supset q)\supset q))$, an algebraic proof is given of the separation property: $I^\Delta\vdash a$ if and only if there exists a derivation of formula $a$ whose terms contain only those connectives that occur in $a$. The proof is achieved by constructing an (isomorphic) embedding of pseudo-Boolean algebras, and on this basis then constructing embeddings, into $\Delta$-pseudo-Boolean algebras, of algebras whose classes approximate corresponding fragments of the calculus $I^\Delta$.
Bibliography: 14 titles.