Abstract

This paper is concerned with the logical structure of intuitionistic equality theories. We prove that De Jongh theorem holds for the theory of decidable equality, but uniform De Jongh theorem fails even for the theory of weakly decidable equality. We also show that the theory of weakly decidable equality is the weakest equality theory which enjoys Glivenko theorem.