论文标题
Craig插值定理在双元性谓词逻辑中失败
Craig interpolation theorem fails in bi-intuitionistic predicate logic
论文作者
论文摘要
在本文中，我们表明，双关键谓词逻辑缺乏Craig插值属性。我们通过调整Mints，Olkhovikov和Urquhart给出的反示例进行直觉谓词逻辑（G. Mints，G。K。Olkhovikov和A. Urquhart。更准确地说，我们表明存在一个有效的含义$ ϕ \rightarrowψ$没有插值（即，在$ ϕ $和$ψ$的词汇交叉中，公式$θ$，使得$ ϕ \ rightarrowθ$和$θ$ and $θ$和$θ\ rightarrowψ$有效）。重要的是，该结果与不幸的是，不幸的是，由Rauszer在（CecyliaRauszer。Craigintropolation定理延长直觉逻辑的延伸。公牛。Ac。pol。pol。pol。pol。pol。sc.sc。，25（4），25（4），337--341（1977（1977））之上，此属性是正确的，这是正确的，请参见此属性，此属性是正确的，这是正确的，请参见此属性，这是正确的，请参见此属性，这是正确的，请参阅此属性。 Jipsen，Kowalski和Ono在N. Galatos中使用此术语，P。Jipsen，T。Kowalski，\＆H。Ono。鉴于扣除定理因双元素逻辑而失败，并具有全球后果，因此该财产的两个表述并非等效。
In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains (G. Mints, G. K. Olkhovikov and A. Urquhart. Failure of Interpolation in Constant Domain Intuitionistic Logic. Journal of Symbolic Logic, 78: 937--950 (2013)). More precisely, we show that there is a valid implication $ϕ\rightarrow ψ$ with no interpolant (i.e. a formula $θ$ in the intersection of the vocabularies of $ϕ$ and $ψ$ such that both $ϕ\rightarrow θ$ and $θ\rightarrow ψ$ are valid). Importantly, this result does not contradict the unfortunately named `Craig interpolation' theorem established by Rauszer in (Cecylia Rauszer. Craig Interpolation Theorem for an Extention of Intuitionistic Logic. Bull. Ac. Pol. Sc., 25(4), 337--341 (1977)) since that article is about the property more correctly named `deductive interpolation' (see Galatos, Jipsen, Kowalski and Ono's use of this term in N. Galatos, P. Jipsen, T. Kowalski, \& H. Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics. Studies in Logic and the Foundations of Mathematics, Vol. 151. Amsterdam: Elsevier B. V. (2007)) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent.
