{\it E. W. Dijkstra} and {\it C. S. Scholten} [Predicate calculus and program semantics. Texts and Monographs in Computer Science. New York: Springer-Verlag (1990; Zbl 0698.68011)] have proposed a formalization of classical predicate logic in the form of a calculus of equational deduction (CED) based on logical equivalence. The author proposes an intuitionstic variant (I-CED) of CED. Completeness of I-CED is proved by means of an embedding of I-CED into a complete Hilbert-style intuitionistic predicate calculus.
Reviewer: Valery Plisko (Moskva)