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

L Hendriks

IILC, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands. E-mail: lhendrik@wins.ua.nl

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.

Pages 589-593


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_04/080589.sgm.abs.html
Last modification: 11 September 1998.
Copyright© Oxford University Press, 1998.