scientific article; zbMATH DE number 1735871
The interpretability logic is a nonstandard modal logic which describes the relation of relative interpretability between arithmetical theories like \(T+A\) and \(T+B,\) where \(A\) and \(B\) are formulas [for detailed definitions see e.g. \textit{A. Visser}, CSLI Lect. Notes 87, 307-359 (1998; Zbl 0915.03020) or \textit{G. Japaridze} and \textit{D. de Jongh}, in: S.\ Buss (ed.), Handbook of proof theory, 475-546 (1998; Zbl 0915.03019)]. The main result of the paper under review is that arrow interpolations hold for IL, i.e., if \(\vdash_{\text{IL}} A\rightarrow B\) then there is a formula \(I\) in the common language of \(A\) and \(B\) such that \(\vdash_{\text{IL}} A\rightarrow I\) and \(\vdash_{\text{IL}} I\rightarrow B.\) For showing interpolation, the authors use a standard model-theoretic Henkin-style proof. Since IL is not compact, maximal consistent sets are confined to finite adequate subsets of the language. As corollaries the authors obtain turnstile interpolation (i.e.\ if \(A\vdash_{\text{IL}}B\) then there is a formula \(I\) in the common language such that \(A\vdash_{\text{IL}} I\) and \(I\vdash_{\text{IL}} B\)) and \(\triangleright\)-interpolation (i.e. if \(\vdash_{\text{IL}} A\triangleright B\) then there is a formula \(I\) in common language such that \(\vdash_{\text{IL}} A\triangleright I\) and \(\vdash_{\text{IL}} I\triangleright B\)). The authors also show that all these properties transfer to the system ILP. It is proved that the system ILW doesn't have the property of arrow interpolation. \textit{A. Visser} [loc. cit.] proved that systems between \(\text{ILM}_0\) and ILM do not have interpolation. The interpolation property for the system ILF is an open problem. For all provability and interpretability logics it is shown that the Beth definability property and the fixed points property are interderivable. This implies that all extensions of the basic system of provability logic GL and all extensions of IL have the Beth property. For the entire collection see [Zbl 0979.00027].
- Explicit fixed points in interpretability logic
- Craig interpolation in the presence of unreliable connectives
- Interpretability degrees of finitely axiomatized sequential theories
- Preservation of Craig interpolation by the product of matrix logics
- Interpretability logic IL does not have finite subtree property
- Interpolation and implicit definability in extensions of the provability logic
- scientific article; zbMATH DE number 7104937 (Why is no real title available?)
- Countably many sublogics of the interpretability logicILhaving fixed point properties
- The fixed point and the Craig interpolation properties for sublogics of \textbf{IL}
- The persistence principle over weak interpretability logic
- Unary interpretability logics for sublogics of the interpretability logic \textbf{IL}
- Lewisian fixed points. I: Two incomparable constructions
- An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics
- A note on the normal form of closed formulas of interpretability logic
- Interpolation and the interpretability logic of PA
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4329232)
