Interpolation in Extensions of First-Order Logic

  1. Gherardi, Guido
  2. Maffezioli, Paolo
  3. Orlandelli, Eugenio
Revista:
Studia Logica

ISSN: 0039-3215,  1572-8730

Año de publicación: 2019

Volumen: 108

Número: 3

Páginas: 619-648

Tipo: Artículo

DOI: 10.1007/S11225-019-09867-0 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Studia Logica

Resumen

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.

€ Ver financiación

Información de financiación

Financiadores

Referencias bibliográficas

  • Baaz, M., and R. Iemhoff, On interpolation in existence logics, in Logic for Programming, Artificial Intelligence, and Reasoning, vol. 3835 of Lecture Notes in Computer Science, Springer, 2005, pp. 697–711.
  • Bonacina, M., and M. Johansson, Interpolation systems for ground proofs in automated deduction: a survey, Journal of Automated Reasoning 54: 353–390, 2015.
  • Casari, E., La matematica della verità, Bollati Boringhieri, 2006.
  • Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, The Journal of Symbolic Logic 22(3): 269–285, 1957.
  • Dragalin, A.G., Mathematical Intuitionism: Introduction to Proof Theory, American Mathematical Society, 1988.
  • Fitting, M., and R. Kuznets, Modal interpolation via nested sequents, Annals of Pure and Applied Logic 166(3): 274–305, 2015.
  • Gabbay, D., and L. Maksimova, Interpolation and Definability: Modal and Intuitionistic Logics, Oxford University Press, 2005.
  • Gallier, J., Logic for Computer Science, 2nd edn., Dover, 2015.
  • Gentzen, G., Investigation into logical deductions, in M.E. Szabo, (ed.), The collected papers of Gerhard Gentzen, chap. 3, North-Holland, 1969, pp. 68–131.
  • Heyting, A., Intuitionism. An introduction, North-Holland, 1956.
  • Kuznets, R., Multicomponent proof-theoretic method for proving interpolation property, Annals of Pure and Applied Logic 169(2): 1369–1418, 2018.
  • Maehara, S., On the interpolation theorem of Craig, Suugaku 12: 235–237, 1960. (in Japanese).
  • Negri, S., Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Mathematical Logic 38(8): 521–547, 1999.
  • Negri, S., Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem, Archive for Mathematical Logic 42(4): 389–401, 2003.
  • Negri, S., and J. von Plato, Cut elimination in the presence of axioms, The Bulletin of Symbolic Logic 4(4): 418–435, 1998.
  • Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, 2001.
  • Negri, S., and J. von Plato, Proof Analysis: A Contribution to Hilbert’s Last Problem, Cambridge University Press, 2011.
  • von Plato, J., Positive lattices, in P. Schuster, U. Berger, and H. Osswald, (eds.), Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum, vol. 306 of Synthese Library, Kluwer, 2001, pp. 185–197.
  • Rasga, J., W. Carnielli, and C. Sernadas, Interpolation via translations, Mathematical Logic Quarterly 55(5): 515–534, 2009.
  • Takeuti, G., Proof Theory, vol. 81 of Studies in Logic and the Foundations of Mathematics, 2nd edn., North-Holland, 1987.
  • Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory, 2nd edn., Cambridge University Press, 2000.