×

Uniform interpolation and layered bisimulation. (English) Zbl 0854.03026

Hájek, Petr (ed.), Gödel ’96. Logical foundations of mathematics, computer science and physics – Kurt Gödel’s legacy. Proceedings of a conference, Brno, Czech Republic, August 1996. Berlin: Springer-Verlag. Lect. Notes Log. 6, 139-164 (1996).
Summary: We give perspicuous proofs of Uniform Interpolation for the theories IPC, K, GL and S4Grz, using bounded bisimulations. We show that the uniform interpolants can be interpreted as propositionally quantified formulas, where the propositional quantifiers get a semantics with bisimulation extension or bisimulation reset as the appropriate accessibility relation. Thus, reversing the conceptual order, the uniform interpolation results can be viewed as quantifier elimination for bisimulation extension quantifiers.
For the entire collection see [Zbl 0844.00017].

MSC:

03C40 Interpolation, preservation, definability
03C80 Logic with extra quantifiers and operators
03C10 Quantifier elimination, model completeness, and related topics
PDFBibTeX XMLCite