Failure of interpolation in constant domain intuitionistic logic. (English) Zbl 1327.03007

The intuitionistic logic of constant domains CD is obtained from intuitionistic predicate logic by adding the scheme \(\forall x\,(A\lor B)\to(A\lor\forall x\,B)\). Its modal counterpart under the Gödel-Tarski translation is the system S4+BF obtained by adding the Barcan formula to S4.
There are two published proofs that CD has the interpolation property. A model-theoretic proof was given by D. M. Gabbay [J. Symb. Log. 42, 269–271 (1977; Zbl 0372.02016)], but that proof contained gaps. A proof-theoretic proof was proposed by E. G. K. Lopez-Escobar [J. Symb. Log. 46, 87–88 (1981; Zbl 0469.03015)], but in a later article of the same author [J. Symb. Log. 48, 595–599 (1983; Zbl 0547.03022)] it was admitted that the earlier proof was incorrect.
In the present paper, a counterexample to the interpolation property for CD is given. Namely, the implication \(\Gamma\to\Delta\), where \(\Gamma\) is \(\forall x\exists y\,(Py\land(Qy\to Rx))\land\neg\forall x\,Rx)\) and \(\Delta\) is \(\forall x\,(Px\to(Qx\lor S))\to S\), is deducible in CD but has no interpolant in CD. Nevertheless, its modal translation has an interpolant in S4+BF.


03B20 Subsystems of classical logic (including intuitionistic logic)
03C40 Interpolation, preservation, definability
Full Text: DOI arXiv Euclid


[1] Montague type semantics for nonclassical logics. I (1969)
[2] Craig interpolation theorem for intuitionistic logic and extensions Part III 42 pp 269– (1977) · Zbl 0372.02016
[3] Handbook of modal logic (2007) · Zbl 1114.03001
[4] Modal logic (2001) · Zbl 0998.03015
[5] The foundations of mathematics: a study in the philosophy of science (1959)
[6] Koninklijke Nederlandse Akademie van Wetenschappen, Mededelingen, Nieuwe Reeks 19 pp 357– (1956)
[7] Proof theory (1987)
[8] Proofs, categories and computations: Essays in honor of Grigori Mints (2010) · Zbl 1203.03007
[9] A short introduction to intuitionistic logic (2000) · Zbl 1036.03003
[10] A second paper ”On the interpolation theorem for the logic of constant domains 48 pp 595– (1983)
[11] On the interpolation theorem for the logic of constant domains 46 pp 87– (1981)
[12] Formal systems and recursive functions pp 92– (1965)
[13] DOI: 10.1007/BF01991851 · Zbl 0233.02020
[14] A logic stronger than intuitionism 36 pp 249– (1971)
[15] Indagationes Mathematicae 26 pp 596– (1964)
[16] Interpolation and definability: Modal and intuitionistic logics (2005) · Zbl 1091.03001
[17] Failures of the interpolation lemma in quantified modal logics 44 pp 201– (1979) · Zbl 0415.03015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.