Basic propositional calculus. II: Interpolation (Q5945567)
From MaRDI portal
scientific article; zbMATH DE number 1657162
Language | Label | Description | Also known as |
---|---|---|---|
English | Basic propositional calculus. II: Interpolation |
scientific article; zbMATH DE number 1657162 |
Statements
Basic propositional calculus. II: Interpolation (English)
0 references
2001
0 references
[For Part I see Math. Log. Q. 44, No. 3, 317-343 (1998; Zbl 0912.03005).] Basic propositional calculus BPC is a proper subsystem of intuitionistic propositional calculus IPC through a weakened modus ponens. Consequently the interpolation theorem permits a generalized form, and requires an original proof. If \(A\) is a formula over a language \(L\), and \(C_1\) and \(C_2\) are formulas over a language \(N\), such that \(A\&C_1\) entails \(C_2\), then there is a formula \(B\) over the intersection language of \(L\) and \(N\) such that both \(A\) entails \(B\) and \(B\&C_1\) entails \(C_2\). Additionally, if \(A\), \(C_1\), and \(C_2\) are conjunctions of implications, then \(B\) can be chosen to be a conjunction of implications.
0 references
Kripke model
0 references
basic propositional calculus
0 references
subsystem of intuitionistic propositional calculus
0 references
weakened modus ponens
0 references
interpolation theorem
0 references