Contracting Intuitionistic Theories

I reformulate the AGM-account of contraction (which would yield an account also of revision). The reformulation involves using introduction and elimination rules for relational notions. Then I investigate the extent to which the two main methods of partial meet contraction and safe contraction can be employed for theories closed under intuitionistic consequence. I would like to thank the organisers, Heinrich Wansing, Sergei Odintsov and Yaroslav Shramko, of the Dresden Workshop on Constructive Negation, July 2–4, 2004, for providing the opportunity to present the ideas in this paper for the first time to a constructively critical audience. I am grateful to Sven Ove Hansson for useful comments on an earlier draft. A special note of thanks is owed also to Joongol Kim, who spotted a mistake in an earlier attempt of mine to prove a stronger form of Theorem 8.6. The results in this paper were presented to the Central Division Meeting of the American Philosophical Association in Chicago in April 2005.