The idea that the good model-theoretic and algorithmic properties of Modal Logics are due to the guarded nature of their quantification was put forward by Andreka, van Benthem and Nemeti in a series of papers in the 1990s, exploiting the satisfiability problem, the tree model property, and other similar properties of the Guarded Fragment of First Order Logic(GF). Since then, further work on the Guarded Fragment has been done by various authors, in some cases reinforcing this idea, in some others not. At least at first sight, Craig interpolation is on the negative side: there are implications in GF without an interpolant in GF, while Modal Logic (and even the μ-calculus, a powerful extension of Modal Logic) enjoys a much stronger form of interpolation, the uniform one, in which the interpolant of a valid implication not only exists, but only depends on the antecedent and on the common language of antecedent and consequent. However, Hoogland and Marx proved that Craig interpolation is restored in GFif we consider the modal character of GFwith more attention, that is, if relations appearing on guards are viewed as “modalities” and the rest as “propositions”, and only the latter enter in the common language. In this paper we strengthen this result by showing that GF enjoys a Modal Uniform Interpolation Theorem (in the sense of Hoogland and Marx).

Bisimulation quantifiers and uniform interpolation for guarded first order logic

D'AGOSTINO, Giovanna;
2015-01-01

Abstract

The idea that the good model-theoretic and algorithmic properties of Modal Logics are due to the guarded nature of their quantification was put forward by Andreka, van Benthem and Nemeti in a series of papers in the 1990s, exploiting the satisfiability problem, the tree model property, and other similar properties of the Guarded Fragment of First Order Logic(GF). Since then, further work on the Guarded Fragment has been done by various authors, in some cases reinforcing this idea, in some others not. At least at first sight, Craig interpolation is on the negative side: there are implications in GF without an interpolant in GF, while Modal Logic (and even the μ-calculus, a powerful extension of Modal Logic) enjoys a much stronger form of interpolation, the uniform one, in which the interpolant of a valid implication not only exists, but only depends on the antecedent and on the common language of antecedent and consequent. However, Hoogland and Marx proved that Craig interpolation is restored in GFif we consider the modal character of GFwith more attention, that is, if relations appearing on guards are viewed as “modalities” and the rest as “propositions”, and only the latter enter in the common language. In this paper we strengthen this result by showing that GF enjoys a Modal Uniform Interpolation Theorem (in the sense of Hoogland and Marx).
File in questo prodotto:
File Dimensione Formato  
010714RevisedGuardedUI.pdf

non disponibili

Descrizione: Post Print Articolo
Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 320.59 kB
Formato Adobe PDF
320.59 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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