From interpolation to proofs
From a proof-theoretic perspective, the idea that interpolation is tied to provability is a natural one. Thinking about Craig interpolation, if a ‘nice’ proof of a valid implication φ→ψ is available, one may succeed in defining an interpolant by induction on the proof-tree, starting from leaves and proceeding to the implication at the root. This method has recently been applied even to fixed point logics admitting cyclic proofs [1, 4]. In contrast, for uniform interpolation, there is no single proof to work from but a collection of proofs to accommodate: a witness to each valid implication φ→ψ where the vocabulary of ψ is constrained. Working over a set of prospective proofs and relying on the structural properties of sequent calculus is the essence of Pitts’ seminal result on uniform interpolation for intuitionistic logic [3].
In this talk we explore the opposite direction of the above endeavour, arguing that uniform interpolation can entail completeness of a proof system. We will demonstrate this in the case of propositional modal µ-calculus by showing that the uniform interpolants obtained from cyclic proofs [2] play an important role in establishing completeness for the natural Hilbert axiomatisation of this fixed point logic.
References
- [1]
- Bahareh Afshari and Graham E. Leigh, Lyndon interpolation for modal mu-calculus, Language, Logic, and Computation TbiLLC 2019 (Cham), (Aybüke Özgün and Yulia Zinova, editors), vol. 13206, Lecture Notes in Computer Science, 2022, pp. 197–213.
- [2]
- Bahareh Afshari, Graham E. Leigh and Guillermo Menédez Turata, Uniform interpolation from cyclic proofs: The case of modal mu-calculus., Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021 (Birmingham, UK), (Anupam Das and Sara Negri, editors), vol. 12842, Springer, 2021, pp. 335–353.
- [3]
- Andrew M. Pitts, On an interpretation of second order quantification in first order intuitionistic propositional logic, Journal of Symbolic Logic, vol. 57 (1992), no. 1, pp. 33–52.
- [4]
- Daniyar Shamkanov, Circular Proofs for Gödel-Löb Logic, arXiv preprint arXiv:1401.4002, 2014.
This document was translated from LATEX by HEVEA.