Basic Propositional Calculus II. InterpolationII. Interpolation

被引:0
|
作者
Mohammad Ardeshir
Wim Ruitenburg
机构
[1] Sharif University of Technology,
[2] P.O. Box 11365-9415,undefined
[3] Tehran,undefined
[4] Iran. (e-mail: ardeshir@math.sharif.ac.ir),undefined
[5] Institute for Studies in Theoretical Physics and Mathematics,undefined
[6] P.O. Box 19395-1795,undefined
[7] Tehran,undefined
[8] Iran.,undefined
[9] Department of Mathematics,undefined
[10] Statistics and Computer Science,undefined
[11] Marquette University,undefined
[12] P.O. Box 1881,undefined
[13] Milwaukee,undefined
[14] WI 53201,undefined
[15] USA. e-mail: wimr@mscs.mu.edu,undefined
来源
关键词
Mathematics Subject Classification (2000): Primary 03F99; Secondary 03F07; Key words or phrases: Basic logic – Kripke model – Interpolation;
D O I
暂无
中图分类号
学科分类号
摘要
Let ℒ and ? be propositional languages over Basic Propositional Calculus, and ℳ = ℒ∩?. Weprove two different but interrelated interpolation theorems. First, suppose that Π is a sequent theory over ℒ, and Σ∪ {C⇒C′} is a set of sequents over ?, such that Π,Σ⊢C⇒C′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢C⇒C′. Second, let A be a formula over ℒ, and C1, C2 be formulas over ?, such that A∧C1⊢C2. Then there exists a formula B over ℳ such that A⊢B and B∧C1⊢C2.
引用
收藏
页码:349 / 364
页数:15
相关论文
共 50 条