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.

Interpolation Theorem for First-Order Theories

GHERARDI, GUIDO;MAFFEZIOLI, PAOLO;ORLANDELLI, EUGENIO
2017

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.
2017
Guido, Gherardi; Paolo, Maffezioli; Eugenio, Orlandelli
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/609117
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact