Interpolation and the Interpretability Logic of PA

AbstractWe investigate the modal logic of interpretability over Peano arithmetic. Our main result is a compactness theorem that extends the arithmetical completeness theorem for the interpretability logic ILMω. This extension concerns recursively enumerable sets of formulas of interpretability logic (rather than single formulas). As corollaries we obtain a uniform arithmetical completeness theorem for the interpretability logic ILM and a partial answer to a question of Orey from 1961. After some simplifications, we also obtain Shavrukov's embedding theorem for Magari algebras (a.k.a. diagonalizable algebras).

Download Full-text

A note on the interpretability logic of finitely axiomatized theories

Studia Logica ◽

10.1007/bf00370185 ◽

1991 ◽

Vol 50 (2) ◽

pp. 241-250 ◽

Cited By ~ 1

Author(s):

Maarten de Rijke

Keyword(s):

Interpretability Logic

Download Full-text

The Closed Fragment of the Interpretability Logic of PRA with a Constant for $\mathrm{I}\Sigma_1$

Notre Dame Journal of Formal Logic ◽

10.1305/ndjfl/1117755145 ◽

2005 ◽

Vol 46 (2) ◽

pp. 127-146 ◽

Cited By ~ 2

Author(s):

Joost J. Joosten

Keyword(s):

Interpretability Logic

Download Full-text

A new principle in the interpretability logic of all reasonable arithmetical theories

Logic Journal of IGPL ◽

10.1093/jigpal/jzp082 ◽

2009 ◽

Vol 19 (1) ◽

pp. 1-17 ◽

Cited By ~ 7

Author(s):

E. Goris ◽

J. J. Joosten

Keyword(s):

Interpretability Logic

Download Full-text

Decidability of interpretability logics ILM0 and ILW*

Logic Journal of IGPL ◽

10.1093/jigpal/jzx027 ◽

2017 ◽

Vol 25 (5) ◽

pp. 758-772 ◽

Cited By ~ 1

Author(s):

Luka Mikec ◽

Tin Perkov ◽

Mladen Vuković

Keyword(s):

Open Problem ◽

Modal Logics ◽

Finite Model ◽

Model Property ◽

Filtration Method ◽

Finite Model Property ◽

Missing Link ◽

Interpretability Logic

Abstract The finite model property is a key step in proving decidability of modal logics. By adapting the filtration method to the generalized Veltman semantics for interpretability logics, we have been able to prove the finite model property of interpretability logic ILM0 w.r.t. generalized Veltman models. We use the same technique to prove the finite model property of interpretability logic ILW* w.r.t. generalized Veltman models. The missing link needed to prove the decidability of ILM0 was completeness w.r.t. generalized Veltman models, which we obtain in this article. Thus, we prove the decidability of ILM0, which was an open problem. Using the same technique, we prove that ILW* is also decidable.

Download Full-text