In this survey, we report our recent work concerning combination results for interpolation and uniform interpolation in the context of quantifier-free fragments of first-order theories. We stress model-theoretic and algebraic aspects connecting this topic with amalgamation, strong amalgamation, and model-completeness. We give sufficient (and, in relevant situations, also necessary) conditions for the transfer of the quantifier-free interpolation property to combined first-order theories; we also investigate the non-disjoint signature case under the assumption that the shared theory is universal Horn. For convex, strong-amalgamating, stably infinite theories over disjoint signatures, we also provide a modular transfer result for the existence of uniform interpolants. Model completions play a key role in the whole paper: They enter into transfer results in the non-disjoint signature case and also represent a semantic counterpart of uniform interpolants.
Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories / S. Ghilardi, A. Gianola. - In: MATHEMATICS. - ISSN 2227-7390. - 10:3(2022 Feb), pp. 461.1-461.22. [10.3390/math10030461]
Interpolation and Uniform Interpolation in Quantifier-Free Fragments of Combined First-Order Theories
S. GhilardiPrimo
;
2022
Abstract
In this survey, we report our recent work concerning combination results for interpolation and uniform interpolation in the context of quantifier-free fragments of first-order theories. We stress model-theoretic and algebraic aspects connecting this topic with amalgamation, strong amalgamation, and model-completeness. We give sufficient (and, in relevant situations, also necessary) conditions for the transfer of the quantifier-free interpolation property to combined first-order theories; we also investigate the non-disjoint signature case under the assumption that the shared theory is universal Horn. For convex, strong-amalgamating, stably infinite theories over disjoint signatures, we also provide a modular transfer result for the existence of uniform interpolants. Model completions play a key role in the whole paper: They enter into transfer results in the non-disjoint signature case and also represent a semantic counterpart of uniform interpolants.File | Dimensione | Formato | |
---|---|---|---|
mathematics-1513407-final version.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
352.34 kB
Formato
Adobe PDF
|
352.34 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.