Algebraic proof of the separation property for an intuitionistic provability calculus

A. U. Muravitskii

Sbornik. Mathematics, Tome 59 (1988) no. 2, pp. 397-406

Résumé

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.