Skolemization in intermediate logics with the finite model property

Abstract

An alternative Skolemization method, which removes strong quantifiers from formulas, is presented that is sound and complete with respect to intermediate predicate logics with the finite model property. For logics without constant domains the method makes use of an existence predicate, while for logics with constant domains no additional predicate is necessary. In both cases an analogue of Hebrand's theorem is obtained and it is proved that the one-variable fragment of a logic with the finite model property is decidable once the propositional fragment of the logic is. It is also shown that for constant domain logics with the finite model property these results imply that interpolation holds for the logic once it holds for its propositional fragment. For logics without constant domains some of these results, but with far more complicated proofs, have been obtained in (iemhoff 2010).