Preskoči na sadržaj
Moj profil Upisi

ispravak · 2024

Correction to: Decidability of interpretability logics ILM_0 and ILW*

Tin Perkov

Sažetak

In "Decidability of interpretability logics ILM_0 and ILW*", we show that some systems of interpretability logic are decidable, namely ILM_0 and ILW*⁠, and we give alternative proofs for other systems, which were already known to be decidable. These results are proved via finite model property, which is established using filtration techniques, adapted to Verbrugge semantics for interpretability logic. During further research we (more precisely, the second and third author in collaboration with S. Horvat) found an error in "Decidability of interpretability logics ILM_0 and ILW*". Namely, filtrations defined in "Decidability of interpretability logics ILM_0 and ILW*" make use of bisimulations between Verbrugge models (or generalized Veltman models, as they were called in the literature until recently) and their finite approximations, and the following claim is used essentially in order to obtain finiteness of filtration: assuming the alphabet is finite, if worlds from two Verbrugge models are
n-modally equivalent, then they are n-bisimilar. The proof of this claim in "Decidability of interpretability logics ILM_0 and ILW*" contains an error, and in fact the claim does not hold. Fortunately, this is fixed by changing definitions of n⁠-bisimulations between Verbrugge models, i.e., by defining a weaker notion of w-bisimulation.

Ključne riječi

modal logic interpretability logic decidability