In this paper we introduce the modelwise interpolation property of a logic that states that whenever \(\models\phi\to\psi\) holds for two formulas \(\phi\) and \(\psi\), then for every model \(\mathfrak{M}\) there is an interpolant formula \(\chi\) formulated in the intersection of the vocabularies of \(\phi\) and \(\psi\), such that \(\mathfrak{M}\models\phi\to\chi\) and \(\mathfrak{M}\models\chi\to\psi\), that is, the interpolant formula in Craig interpolation may vary from model to model. We compare the modelwise interpolation property with the standard Craig interpolation and with the local interpolation (...) property by discussing examples, most notably the finite variable fragments of first order logic, and difference logic. As an application we connect the modelwise interpolation property with the local Beth definability, and we prove that the modelwise interpolation property of an algebraizable logic can be characterized by a weak form of the superamalgamation property of the class of algebras corresponding to the models of the logic. (shrink)

In this paper, we introduce a general technology, calledtaming, for finding well-behaved versions of well-investigated logics. Further, we state completeness, decidability, definability and interpolation results for a multimodal logic, calledarrow logic, with additional operators such as thedifference operator, andgraded modalities. Finally, we give a completeness proof for a strong version of arrow logic.

Biró, B. and I. Sain, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Annals of Pure and Applied Logic 63 201-225. We show that one can prove the partial correctness of more programs using Peano's axioms for the time frames of three-sorted time models than using only Presburger's axioms, that is it is useful to allow multiplication of time points at program verification and in dynamic and temporal logics. We organized the paper (...) as follows: 1. Preliminaries, 2. The main result, 3. Peano arithmetic with bounded multiplication, 4. Connections with temporal logics and dynamic logics, Acknowledgements, References. (shrink)