Paper Info
Title
Downward Löwenheim-Skolem Theorem and interpolation in logics with constructors.
Abstract
The present article describes a method for proving Downward Lowenheim-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 Lowenheim-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 Lowenheim-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 Lowenheim-Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Lowenheim-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.
Year
DOI
Venue
2017
10.1093/logcom/exv018
JOURNAL OF LOGIC AND COMPUTATION
Keywords
Field
DocType
institution,algebraic specification,first-order logic,interpolation,constructor-based logic
Discrete mathematics,Open problem,Interpolation,Preorder,Model theory,Extensional definition,Löwenheim–Skolem theorem,Morphism,Semantics,Mathematics
Journal
Volume
Issue
ISSN
27
SP6
0955-792X
Citations 
PageRank 
References 
0
0.34
0
Authors
1
Name
Order
Citations
PageRank
Daniel Găină1425.30