Interpolation theorems for intuitionistic predicate logic

DOI10.1016/S0168-0072(01)00060-4MaRDI QIDQ5957915zbMATH OpenOpenAlexFDO

Authors G. E. Mints

Publication date 11 December 2002

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(01)00060-4

zbMATH Keywords

interpolation theoremintuitionistic logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Interpolation, preservation, definability (03C40) Cut-elimination and normal-form theorems (03F05)

Review text

For the classical first-order logic the Craig interpolation theorem may be extended to partitions \(\Gamma;\Gamma^\prime\vdash\Delta;\Delta^\prime\) of the sequent \(\Gamma,\Gamma^\prime\vdash\Delta,\Delta^\prime\) meaning that, for each partition, there is an interpolant \(I\) such that both sequents \(\Gamma\vdash\Delta,I\) and \(I,\Gamma^\prime\vdash\Delta^\prime\) are provable. The same extension of the Craig interpolation theorem to the case of intuitionistic predicate logic is not possible. However, in this paper the author presents a version of such an extension true for intuitionistic propositional calculus and a more complicated version for the predicate language case.

Recommendations

• Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach
• Der Interpolationssatz der intuitionistischen Prädikatenlogik
• Interpolation in extensions of first-order logic
• Interpolation in superintuitionistic predicate logics with equality
• Interpolation in fragments of intuitionistic propositional logic

Cites work

• A logic program for transforming sequent proofs to natural deduction proofs
• scientific article; zbMATH DE number 1292293 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3252193 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• scientific article; zbMATH DE number 3074067 (Why is no real title available?)
• Indexed systems of sequents and cut-elimination
• Interpolation properties of superintuitionistic logics
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Proof theory
• Representing scope in intuitionistic deductions

Cited in

(33)

• Sentential logics and Maehara interpolation property
• A unified approach to relative interpolation
• Der Interpolationssatz der intuitionistischen Prädikatenlogik
• Craig's interpolation theorem for the intuitionistic logic and its extensions - a semantical approach
• On Gabbay's proof of the Craig interpolation theorem for intuitionistic predicate logic
• Sequent calculi for intuitionistic Gödel-Löb logic
• The interpolation problem in finite-layered pre-Heyting logics
• Interpolation in extensions of first-order logic
• Towards a clausal analysis of cut-elimination
• Interpolation properties for provability logics GL and GLP
• Interpolation theorem of Hao Wang's partial predicate calculus
• Failure of interpolation in constant domain intuitionistic logic
• scientific article; zbMATH DE number 3841821 (Why is no real title available?)
• scientific article; zbMATH DE number 4210104 (Why is no real title available?)
• Interpolation and implicit definability in extensions of the provability logic
• A weak form of interpolation in equational logic
• Propositional Interpolation and Abstract Interpretation
• scientific article; zbMATH DE number 3937157 (Why is no real title available?)
• Coinductive formulas and a many-sorted interpolation theorem
• scientific article; zbMATH DE number 31597 (Why is no real title available?)
• Intuitionistic propositional logic with only equivalence has no interpolation
• Interpolation theorems for some variants of LTL
• A refinement of the Craig-Lyndon interpolation theorem for classical first-order logic with identity
• scientific article; zbMATH DE number 1931663 (Why is no real title available?)
• A variant of Craig's interpolation theorem for intuitionistic fuzzy formulas. II
• Cut-elimination, completeness, and Craig interpolation theorems for Gurevich's extended first-order intuitionistic logic with strong negation
• Full cut elimination and interpolation for intuitionistic logic with existence predicate
• Tools and Algorithms for the Construction and Analysis of Systems
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• scientific article; zbMATH DE number 3271481 (Why is no real title available?)
• Basic propositional calculus. II: Interpolation
• Hypersequent calculi for intuitionistic logic with classical atoms
• Combining intuitionistic and classical propositional logic: Gentzenization and Craig interpolation

This page was built for publication: Interpolation theorems for intuitionistic predicate logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5957915)