Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


The present article describes a method for proving Downward Löwenheim-Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim-Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim- Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim-Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem.

Original languageEnglish
Pages (from-to)1717-1752
Number of pages36
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - Sept 1 2017
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic


Dive into the research topics of 'Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors'. Together they form a unique fingerprint.

Cite this