CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishIn this work we prove the interpolation theorem for some first-order theory. Previous results by Negri and von Plato (2011) and Dyckhoff and Negri (2015) have shown how to prove cut elimination in the presence of non-logical rules. Often cut elimination allows a constructive proof of the interpolation theorem. Thus, the question as to whether and to what extent interpolation holds in first-order theories naturally arises. Our aim is to give an answer to this question. First, we show that the standard Takeuti-Maehara techinique fails when first-order axioms are formulated as rules. Then, using an alternative strategy based on negative normal forms, we identify a class of theories for which interpolation holds. The proof we give is entirely constructive. As a case study, we consider the theory of strict partial orders and we show how to extend the result to linear orders as well.
| Titolo: | Interpolation Theorem for First-Order Theories | |
| Autore/i: | GHERARDI, GUIDO; MAFFEZIOLI, PAOLO; ORLANDELLI, EUGENIO | |
| Autore/i Unibo: | ||
| Anno: | 2017 | |
| Rivista: | ||
| Abstract: | In this work we prove the interpolation theorem for some first-order theory. Previous results by Negri and von Plato (2011) and Dyckhoff and Negri (2015) have shown how to prove cut elimination in the presence of non-logical rules. Often cut elimination allows a constructive proof of the interpolation theorem. Thus, the question as to whether and to what extent interpolation holds in first-order theories naturally arises. Our aim is to give an answer to this question. First, we show that the standard Takeuti-Maehara techinique fails when first-order axioms are formulated as rules. Then, using an alternative strategy based on negative normal forms, we identify a class of theories for which interpolation holds. The proof we give is entirely constructive. As a case study, we consider the theory of strict partial orders and we show how to extend the result to linear orders as well. | |
| Data stato definitivo: | 17-ott-2017 | |
| Appare nelle tipologie: | 1.06 Abstract in rivista |
File in questo prodotto:
Copyright © 2021