Skolemization in intermediate logics of finite width

Abstract

An alternative Skolemization method, which removes strong quantifiers from formulas, is presented that is sound and complete with respect to intermediate predicate logics of finite width. 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 as well. It is shown that for constant domain logics of finite width these results imply that interpolation holds for the logic once it holds for its propositional fragment.