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

Interpolation in singular geometric theories / Guido Gherardi; Paolo Maffezioli; Eugenio Orlandelli. - ELETTRONICO. - (2019), pp. 787-796. (Intervento presentato al convegno Proof-Thoeeoretic SemanticsAssessment and Future Perspectives tenutosi a University of Tuebingen nel 27-30 marzo 2019) [10.15496/publikation-35319].

Interpolation in singular geometric theories

Guido Gherardi;Eugenio Orlandelli
2019

Abstract

We present 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.
2019
Proof-Theoretic Semantics: Assessment and Future Perspectives. Proceedings of the Third Tübingen Conference on Proof-Theoretic Semantics, 27–30 March 2019
787
796
Interpolation in singular geometric theories / Guido Gherardi; Paolo Maffezioli; Eugenio Orlandelli. - ELETTRONICO. - (2019), pp. 787-796. (Intervento presentato al convegno Proof-Thoeeoretic SemanticsAssessment and Future Perspectives tenutosi a University of Tuebingen nel 27-30 marzo 2019) [10.15496/publikation-35319].
Guido Gherardi; Paolo Maffezioli; Eugenio Orlandelli
File in questo prodotto:
File Dimensione Formato  
GherardiMaffezioliOrlandelli_2019_InterpolSingGeomTh.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per accesso libero gratuito
Dimensione 1.5 MB
Formato Adobe PDF
1.5 MB Adobe PDF Visualizza/Apri

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/704717
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact