Interpolation Theorem for First-Order Theories

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.