Proving Craig and Lyndon interpolation using labelled sequent calculi

DOI10.1007/978-3-319-48758-8_21MaRDI QIDQ2835880zbMATH OpenOpenAlexFDO

Authors Roman Kuznets

Publication date 30 November 2016

Published in Logics in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.05656

zbMATH Keywords

modal logicCraig interpolationLyndon interpolationlabelled sequentsGeach formulas

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Interpolation, preservation, definability (03C40)

Abstract: We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of internal sequent calculi, including sequents, hypersequents, and nested sequents. Here we adapt the method to a more general external formalism of labelled sequents and provide sufficient criteria on the Kripke-frame characterization of a logic that guarantee the IPs. In particular, we show that classes of frames definable by quantifier-free Horn formulas correspond to logics with the IPs. These criteria capture the modal cube and the infinite family of transitive Geach logics.

Recommendations

• Craig interpolation via hypersequents
• Modal interpolation via nested sequents
• Interpolation method for multicomponent sequent calculi
• Interpolation for intermediate logics via hyper- and linear nested sequents
• scientific article; zbMATH DE number 3863170

Cites work

• scientific article; zbMATH DE number 5920153 (Why is no real title available?)
• A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi
• Absence of the interpolation property in the consistent normal modal extensions of the Dummett logic
• Beth definability in expressive description logics
• Craig interpolation in displayable logics
• Geometrisation of first-order logic
• Interpolation method for multicomponent sequent calculi
• Labelled tree sequents, tree hypersequents and nested (deep) sequents
• Modal interpolation via nested sequents
• Modal logic for philosophers
• Multi-dimensional modal logic
• Partition-based logical reasoning for first-order and propositional theories
• Proof Analysis
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• The logic of exact covers: completeness and uniform interpolation
• Uniform Interpolation by Resolution in Modal Logic

Cited in

(12)

• Through an inference rule, darkly
• Lyndon Interpolation for Modal $$\mu $$-Calculus
• Lyndon interpolation theorem of instantial neighborhood logic-constructively via a sequent calculus
• Multicomponent proof-theoretic method for proving interpolation properties
• Modal interpolation via nested sequents
• Craig’s trick and a non-sequential system for the Lambek calculus and its fragments
• Interpolation method for multicomponent sequent calculi
• Interpolation for intermediate logics via hyper- and linear nested sequents
• Craig interpolation via hypersequents
• Uniform Lyndon interpolation property in propositional modal logics
• Horn filter pairs and Craig interpolation in propositional logic
• Extensions of \textsf{K5}: proof theory and uniform Lyndon interpolation

This page was built for publication: Proving Craig and Lyndon interpolation using labelled sequent calculi

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