Skolemization in intermediate logics with the finite model property

Matthias Baaz*, R. Iemhoff

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

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).
Original languageEnglish
Pages (from-to)224-237
Number of pages14
JournalLogic Journal of the IGPL
Volume24
Issue number3
DOIs
Publication statusPublished - Jun 2016

Keywords

  • Skolemization
  • Herbrand's theorem
  • interpolation
  • intermediate logic

Fingerprint

Dive into the research topics of 'Skolemization in intermediate logics with the finite model property'. Together they form a unique fingerprint.

Cite this