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