Interpolation for first order S5 (Q3149986)

It is well known that the interpolation theorem can be proved for many first-order modal logics, but S5 is a notable exception. In this paper, the author gives us a proof of the interpolation theorem for first-order S5 provided the logic is extended in order to contain propositional quantifiers. The proof method is based on prefixed tableaux [see \textit{M. Fitting}, First-order logic and automated theorem proving. 2nd ed. New York: Springer (1996; Zbl 0848.68101)]. In a tableau proof of \(A\to B\), the author shows how to build an interpolant from the closed tableau. To this end, a formula called quasi interpolant is obtained for the initial set of the tableau. Finally, this quasi interpolant is converted in a real interpolant for the proposed formula \(A\to B\).