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

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

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
Volume27
Issue number6
DOIs
Publication statusPublished - Sep 1 2017
Externally publishedYes

Fingerprint

Interpolation
First-order Logic
Interpolate
Logic
Higher-order Logic
Theorem
Partial Algebra
Algebra
Preorder
Model Theory
Morphism
Semantics
Open Problems
Arbitrary
Demonstrate
Borrowing

All Science Journal Classification (ASJC) codes

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

Cite this

Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors. / Gaina, Daniel Mircea.

In: Journal of Logic and Computation, Vol. 27, No. 6, 01.09.2017, p. 1717-1752.

Research output: Contribution to journalArticle

@article{85a4c853e7754487b752144bcb3b1052,
title = "Downward L{\"o}wenheim-Skolem Theorem and interpolation in logics with constructors",
abstract = "The present article describes a method for proving Downward L{\"o}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{\"o}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{\"o}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{\"o}wenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward L{\"o}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.",
author = "Gaina, {Daniel Mircea}",
year = "2017",
month = "9",
day = "1",
doi = "10.1093/logcom/exv018",
language = "English",
volume = "27",
pages = "1717--1752",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "6",

}

TY - JOUR

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

AU - Gaina, Daniel Mircea

PY - 2017/9/1

Y1 - 2017/9/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85031902006&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85031902006&partnerID=8YFLogxK

U2 - 10.1093/logcom/exv018

DO - 10.1093/logcom/exv018

M3 - Article

VL - 27

SP - 1717

EP - 1752

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 6

ER -