Archive for Mathematical Logic

, Volume 40, Issue 5, pp 349–364 | Cite as

Basic Propositional Calculus II. Interpolation

II. Interpolation
  • Mohammad Ardeshir
  • Wim Ruitenburg


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 Σ∪ {CC′} is a set of sequents over ?, such that Π,Σ⊢CC′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢CC′. Second, let A be a formula over ℒ, and C 1, C 2 be formulas over ?, such that AC 1C 2. Then there exists a formula B over ℳ such that AB and BC 1C 2.

Mathematics Subject Classification (2000): Primary 03F99; Secondary 03F07 
Key words or phrases: Basic logic – Kripke model – Interpolation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Mohammad Ardeshir
    • 1
  • Wim Ruitenburg
    • 2
  1. 1.Sharif University of Technology, P.O. Box 11365-9415, Tehran, Iran. (e-mail:
  2. 2.Department of Mathematics, Statistics and Computer Science, Marquette University, P.O. Box 1881, Milwaukee, WI 53201, USA. e-mail:

Personalised recommendations