|
Abstract : |
We investigate transfer of interpolation in such combinations of modal logic which lead to interaction of the modalities. Combining logics by taking products often blocks transfer of interpolation. The same holds for combinations by taking unions, a generalization of Humberstone?s inaccessibility logic. Viewing first order logic as a product of modal logics, we derive a strong counterexample for failure of interpolation in the finite variable fragments of first order logic. We provide a simple condition stated only in terms of frames and bisimulations which implies failure of interpolation. Its use is exemplified in a wide range of cases. In 1957, W. Craig proved the interpolation theorem for first order logic [Cra57]. Comer [Com69] showed that the property fails for all finite variable fragments except the onevariable fragment. The n-variable fragment of first order logic ?for short Ln ? contains all first order formulas using just n variables and containing only predicate symbols of arity not higher that n (we assume the language has only variables as terms.) Here we will show that the axiom which makes the quantifiers commute can be seen as the reason for this failure. Since Craig?s paper, interpolation has become one of the standard properties that one investigates when designing a logic, though it hasn?t received the status of a completeness or a decidability theorem. One of the main reasons why a logic should have interpolation is because of ?modular theory building?. As we will see below interpolation in modal logic is equivalent to the following property (which is the semantical version of Robinson?s consistency lemma.), |
