|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 4: August 1998.
Intuitionistic propositional logic with only equivalence has no interpolation
IILC, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands. E-mail: email@example.com
We will show in this paper that there is no interpolation theorem for the fragments of pure equivalence, pure equivalence with negation, and pure equivalence with double negation in intuitionistic propositional logic. On the other hand the Beth definability theorem holds for all three fragments. The computer program that was used to calculate the counterexample by computations on a finite Kripke model is briefly sketched.
Key words: Intuitionistic propositional logic, interpolation, equivalence, fragment, automated model checking.