Interpolation in extensions of first-order logic

TL;DR

This paper proves that certain extended first-order logics with geometric axioms possess the Craig's interpolation property, enabling new proofs of interpolation for various mathematical theories.

Contribution

It generalizes Maehara's lemma to a broader class of logical systems, establishing interpolation for extensions with singular geometric axioms.

Findings

Interpolation holds for classical and intuitionistic first-order logic with identity.

Interpolation applies to theories of equivalence relations, orders, and order-like structures.

Provides a unified proof approach for multiple mathematical theories.

Abstract

We prove a generalization of Maehara's lemma to show that the extensions of classical and intuitionistic first-order logic with a special type of geometric axioms, called singular geometric axioms, have Craig's interpolation property. As a corollary, we obtain a direct proof of interpolation for (classical and intuitionistic) first-order logic with identity, as well as interpolation for several mathematical theories, including the theory of equivalence relations, (strict) partial and linear orders, and various intuitionistic order theories such as apartness and positive partial and linear orders.