Craig Interpolation on the Logic of Knowledge Everardo Bárcenas1 , José-de-Jesús Lavalle-Martínez2 , Guillermo Molero-Castillo3,4 , and Alejandro Velázquez-Mena1 1 Universidad Nacional Autónoma de México [barcenas,mena]@fi-b.unam.mx 2 Benemérita Universidad Autónoma de Puebla jlavalle@cs.buap.mx 3 Consejo Nacional de Ciencia y Tecnología 4 Universidad Veracruzana ggmoleroca@conacyt.mx Abstract. The Craig interpolation property is described as follows: if a formula φ implies another formula ψ, then there is a formula β in the common language of φ and ψ, such that φ also implies β, as well as β implies ψ. In this paper, we provide a constructive proof of the Craig interpolation property on the modal logic of knowledge Km . The proof is based on the application of the Maehara technique on a tree-hypersequent calculus. We also show, as a consequence of the interpolation property, Beth definability and Robinson joint consistency . 1 Introduction Philosophy and Artificial Intelligence have been the traditional study framework to rea- son about knowledge [12]. More recently, reasoning about knowledge has become of much importance in many areas of computer science, such as distributed systems, cryp- tography, natural language processing and databases [8]. In this paper, we consider as a formal framework to study knowledge, the basic modal logic of knowledge, also known as the multi-modal logic Km . This logic has been shown to be mathematically well-founded [11]. As consequence of being a bisimulation invariant fragment of first order logic, Km posses a nice balance of expressiveness and reasoning efficiency [3]. The interpolation property was first proved for classical first order logic by Craig [6]. Considering a formula φ implies another formula ψ, the interpolation property consists in the existence of a formula β, called the interpolant, in the common language of φ and β, which is assumed to be non-empty, such that φ implies β, and β implies ψ. Some logical consequences of interpolation are Beth definability [1] and Robinson joint consistency [22]. Applications of interpolation in computer science have been recently studied for formal verification [18], computational complexity [5], and knowledge rep- resentation [13, 4], among others. In this paper, we give a constructive proof the Craig interpolation theorem for the modal logic of knowledge Km . The proof implies a straightforward algorithm to com- pute interpolants. 15 1.1 Related work Early studies about the interpolation property in modal logics are reported in [10, 16]. In [10], Gabbay proved interpolation for several mono-modal logics including K and S4. Maksimova in [16] indentifies a close conection of amalgamability of modal logics containing S4, and proved that only a finite number modal logics conaining S4 enjoys interpolation. Maksimova later proved in [15] interpolation of all normal modal log- ics via amalgamation. This result was extended for multi-modal logics in [14]. Marx proved interpolation in [17] for several modal logics with bisimulation. This work in- cludes interpolation proofs for K, fibered modal logics and the multi-modal logics of knowledge and belief. In all the above works, interpolation is proved by semantics meth- ods. Although these methods are quite general and can be applied to several logics, they not provide an explicit construction of interpolants. In the current paper, we provide a syntactic proof of interpolation for the multi-modal logic Km . This proof includes an explicit construction of interpolants. Syntactic interpolation proofs for modal logics KB, KDB, K5 and KD5 are de- scribed in [20]. In this work, interpolation is proved by means of a cut-free complete sequent-like tableau deduction system. Constructive interpolation for modal logics K and T is given in [2]. More precisely, a stronger form of interpolation, called uniform interpolation, is proved in this work. In uniform interpolation, interpolants are com- posed by the common language language of formulas in the implication, but restricted by a choice of propositional variables. The closest work to our paper is [9]. In this work, constructive interpolation is proved for the entire modal cube, composed by the logics resulting from any combination of K, D, T , B, 5 and 4. The proof technique used in this work is based on nested sequents. In our paper, we obtain a constructive interpo- lation proof for the multi-modal logic Km , using the Maehara technique on a cut-free complete tree-hypersequent calculus. In [7], D’Agostino reports an extensive survey on interpolation for non-classical logics, including modal logics. 1.2 Outline We first introduce the multi-modal logic of knowledge Km in Section 2. In Section 3, we describe a complete cut-free tree-hypersequent calculus for Km . Then, in Section 4, by means of Maehara technique, we extract interpolants from tree-hypersequent proofs of Km implications. In Section 5, as a consequence of interpolation, we also prove Beth definability and Robinson joint consistency. Finally, in Section 6, we give a summary of the article and briefly argue further research perspectives. 2 Logic of Knowledge We assume a basic modal language: a non-empty set of propositions PROP; and a non- empty finite set of modalities MOD. The set of formulas is inductively defined by the following grammar. φ := p | ¬φ | φ ∧ φ | 2m φ 16 where p is a proposition and m is a modality. Notation: > := p ∨ ¬p ⊥ := ¬> φ ∨ ψ := ¬(¬φ ∧ ¬ψ) φ → ψ := ¬φ ∨ ψ 3m φ := ¬2m ¬φ A Kripke structure is a tuple M = (W, R, V ) where: – W is a non-empty set called domain; – R is a finite set of binary relations Rm : W × W , for every modality m; and – V : PROP 7→ 2W is valuation function mapping propositions to domain subsets. Given a Kripke structure M = (W, R, V ), formulas are interpreted as follows: M [[p]] = {w ∈ V (p)} M M [[¬φ]] =W \ [[φ]] M M M [[φ ∧ ψ]] = [[φ]] ∩ [[ψ]] M [[2m φ]] = {w | ∀w0 ∈ W : if (w, w0 ) ∈ Rm , o M then w0 ∈ [[φ]] M We may also write M, w |= φ instead of w ∈ [[φ]] , M |= φ when for every w in M , we have that M, w |= φ, in which case we say M is a model of φ. If any Kripke structure is a model of φ, we write |= φ. Definition 1 (Hilbert derivation system). We define the derivation system H by the following schemas and rules, for each m ∈ MOD: A1 φ → (ψ → φ) A2 (φ → (ψ → β)) → ((φ → ψ) → (φ → β)) A3 (¬φ → ¬ψ) → (ψ → φ) A4 2m (φ → ψ) → (2m φ → 2m ψ) φ→ψ φ R1 ψ φ R2 2m φ We say a formula φn is derivable from H, written `H φn , if there is a sequence φ1 , φ2 , . . . , φn , such that for each i ∈ {1, . . . , n}: – φi is either an instance, up to substitution, of a schema in H, or – there is (are) j < i (and k < i) such that φi and φj (and φk ) are instances of the conclusion and premises, resp, of a rule in H. Consider for instance the following derivation of 2m (φ ∧ ψ) → 2m φ: 1. (φ ∧ ψ) → φ, which by notation is an instance of A1 , ¬φ ∨ ψ ∨ φ; 2. 2m ((φ ∧ ψ) → φ), from 1 by R2 ; 3. 2m ((φ ∧ ψ) → φ) → (2m (φ ∧ ψ) → 2m φ), from A4 ; and 4. 2m (φ ∧ ψ) → 2m φ, from 2 and 3 by R1 . Theorem 1 (Correctness [11]). For any formula φ, `H φ, if and only if, |= φ. 17 3 Tree-hypersequents A sequent is an expression Γ ` ∆, where Γ and ∆ are formula multisets, non-empty and finite. Intuitively, a sequent Γ ` ∆ is interpreted, in terms of logical symbols, as an implication, where the antecedent is composed by the disjunction of formulas in Γ , and the consequent is the conjunction of formulas in ∆. We then the define the following interpretation function: n ^ k _ (φ1 , . . . , φn ` ψ1 , . . . , ψk )I := φi → ψj i=1 j=1 where n and k are some positive integers. In sequents, we often write φ, Γ or Γ, φ instead of {φ} ∪ Γ , also ` ∆ instead of > ` ∆, and Γ ` in place of Γ ` ⊥. Tree hypersequents expressions are inductively defined by the following grammar: T :=S [ST ] ST :=∅ | m : T, ST where S is a sequent and m is a modality. We extend the interpretation function of sequents for tree hypersequents as follows: (S [ST ])I :=S I ∨ (ST )I (∅)I :=⊥ (m : T, ST )I :=2m T I ∨ (ST )I When clear from context, we often write tree instead of tree hypersequent. It is usually written S instead of S [∅], also if S is Γ ` ∆, we write φ, S and S, φ instead of φ, Γ ` ∆ and Γ ` φ, ∆, respectively. We write T hSi when a sequent S occurs in a tree T , more precisely: – S [ST ] hSi; – S 0 [ST ] hSi, provided that S 0 is different than S and ST hSi; and – (m : T 0 , ST ) hSi, when either T 0 hSi or ST hSi. We extend the occurring relation T hT 0 i between trees as expected: – T and T 0 are the same; – (S [ST ]) hT 0 i, when ST hT 0 i; – (m : T 0 , ST 0 ) hT 0 i; and – (m : T 00 , ST 0 ) hT 0 i, provided that T 00 is different than T 0 and ST 0 hT 0 i. We also distinguish when m : T 0 occurs in a tree T , written T hm : T 0 i: – (S [ST ]) hm : T 0 i, when ST hm : T 0 i; – (m : T 0 , ST 0 ) hm : T 0 i; and – (m0 : T 00 , ST 0 ) hT 0 i, provided that either m is different than m0 or T 00 is different than T 0 , and ST 0 hm : T 0 i. 18 We say a sequent S occurs, under a modality m, in a finite sequence of tree hyperse- quents m1 : T1 , m2 : T2 , . . . , mk : Tk , when there is an i such that mi is m and Ti has the form S [ST ]. Moreover, we often write S [m : S 0 ] instead of S [ST ], provided S 0 occurs under m in ST . Definition 2 (Tree-hypersequents derivation system). The inference system for tree hypersequents G is defined as follows. – Initial tree hypersequents: T hp, S, pi – Propositional rules: T hS, φi T hφ, Si ¬L ¬R T h¬φ, Si T hS, ¬φi T hφ, ψ, Si T hS, φi T hS, ψi ∧L ∧R T hφ ∧ ψ, Si T hS, φ ∧ ψi – Modal rules: T h2m φ, S [m : φ, S 0 ]i 2m L T h2m φ, S [m : S 0 ]i T hS [m : ` φ, ST ]i 2m R T hS, 2m φ [ST ]i We now define the concept of derivation tree: – any 0 rule (up 0 to00subtitution) of G is a derivation tree; – TT and T T T are derivation trees, provided that T 0 and T 00 are derivation trees, and T0 T0 T 00 – T0 and 0 T 0 are rules in G and T00 and T000 are the lowest tree hypersequents occurring in T 0 and T 00 . If all the branches of a derivation tree, where T is the lowest tree hypersequent, are finite and ends with an initial tree hypersequent, then we say the derivation tree is a proof tree, or simply a proof, of T , or that T is derivable in G, and we write `G T . Consider now for instance the following proof of A4 : T hφ, ψ ` ψi ¬R T hφ ` ψ, φi T hφ ` ψ, ¬ψi ∧R T hφ ` ψ, φ ∧ ¬ψi ¬L 2m ¬(φ ∧ ¬ψ), 2m φ ` [m : ¬(φ ∧ ¬ψ), φ ` ψ] 2m L 2m ¬(φ ∧ ¬ψ), 2m φ ` [m : φ ` ψ] 2m L 2m ¬(φ ∧ ¬ψ), 2m φ ` [m : ` ψ] 2m R 2m ¬(φ ∧ ¬ψ), 2m φ ` 2m ψ ¬L 2m ¬(φ ∧ ¬ψ), 2m φ, ¬2m ψ ` ∧L 2m ¬(φ ∧ ¬ψ) ∧ 2m φ ∧ ¬2m ψ ` ¬R ` ¬(2m ¬(φ ∧ ¬ψ) ∧ 2m φ ∧ ¬2m ψ) Theorem 2 ([21, 19]). For any sequent S, `G S, if and only if, `H S. Corollary 1. For any sequent S, `G S, if and only if, |= S I . 19 4 Interpolation We define the set of non-logical symbols Sym(φ) of a formula φ as follows: – Sym(p) = {p}; – Sym(¬φ) = Sym(φ); – Sym(φ ∧ ψ) = Sym(φ) ∪ Sym(ψ); and – Sym(2m φ) = {m} ∪ Sym(φ). The set of non-logical symbols of a (multi-)set of formulas is defined as expected. For technical convenience, we consider an equivalent extension G0 of the derivation system G, where formulas > are considered per se (not as notation). All rules in G are also in G0 . Additionally, the initial sequent T hS, >i is also included in G0 . Lemma 1 (Maehara’s Lemma). Let T hΓ ` ∆i be derivable in G, and let Γ1 , Γ2 and ∆1 , ∆2 be partitions of Γ and ∆, respectively. Then there is a formula β, called the interpolant, such that T hΓ1 ` ∆1 , βi and T hβ, Γ2 ` ∆2 i are derivable in G0 , and Sym(β) ⊆ (Sym(Γ1 ) ∪ Sym(∆1 )) ∩ (Sym(Γ2 ) ∪ Sym(∆2 )). Proof. By induction on the height of the proof tree. The base case is T hp, Γ ` ∆, pi. The interpolant β is then defined according to the occurrence of propositions p in partitions: T hp, Γ1 ` ∆1 , p, ¬>i T h¬>, Γ2 ` ∆2 i T hΓ1 ` ∆1 , >i T h>, p, Γ2 ` p, ∆2 i T hp, Γ1 ` ∆1 , pi T hp, Γ2 ` ∆2 , pi T hΓ1 ` ∆1 , p, ¬pi T h¬p, p, Γ2 ` ∆2 i Induction step. Assume the last inference is the following: T hΓ ` ∆, φi T hΓ ` ∆, ψi T hΓ ` ∆, φ ∧ ψi By induction hypothesis, there are interpolants β1 and β2 for the upper tree hyper- sequents. There are two possible cases according the occurrence of φ and ψ in the respective partitions. T hΓ1 ` ∆1 , φ, β1 i T hβ1 , Γ2 ` ∆2 i T hΓ1 ` ∆1 , ψ, β2 i T hβ2 , Γ2 ` ∆2 i T hΓ1 ` ∆1 , β1 i T hβ1 , Γ2 ` ∆2 , φi T hΓ1 ` ∆1 , β2 i T hβ2 , Γ2 ` ∆2 , ψi Depending on the occurrence of φ∧ψ in the partitions, we then construct the interpolant φ as follows: T hΓ1 ` ∆1 , φ ∧ ψ, β1 ∨ β2 i T hβ1 ∨ β2 , Γ2 ` ∆2 i T hΓ1 ` ∆1 , β1 ∧ β2 i T hβ1 ∧ β2 , Γ2 ` ∆2 , φ ∧ ψi In the induction step, now consider the last inference is 20 T h2m φ, Γ ` ∆ [m : φ, Γ 0 ` ∆0 ]i T h2m φ, Γ ` ∆ [m : Γ 0 ` ∆0 ]i By induction, there is an interpolant β for the upper tree hypersequent. By the occur- rence of 2m φ in partitions, we distinguish two cases: T h2m φ, Γ1 ` ∆1 , β [m : φ, Γ 0 ` ∆0 ]i T hβ, Γ2 ` ∆2 [m : φ, Γ 0 ` ∆0 ]i T hΓ1 ` ∆1 , β [m : φ, Γ 0 ` ∆0 ]i T hβ, 2m φ, Γ2 ` ∆2 [m : φ, Γ 0 ` ∆0 ]i We then construct the following interpolants: T h2m φ, Γ1 ` ∆1 , 2m φ ∧ β [m : Γ 0 ` ∆0 ]i T h2m φ ∧ β, Γ2 ` ∆2 [m : Γ 0 ` ∆0 ]i T hΓ1 ` ∆1 , ¬2m φ ∨ β [m : Γ 0 ` ∆0 ]i T h¬2m φ ∨ β, 2m φ, Γ2 ` ∆2 [m : Γ 0 ` ∆0 ]i Consider now the last inference is the following: T hΓ ` ∆ [m : ` φ, ST ]i T hΓ ` ∆, 2m φ [ST ]i We obtain the following interpolant β by induction: T hΓ1 ` ∆1 , β [m : ` φ, ST ]i T hβ, Γ2 ` ∆2 [m : ` φ, ST ]i There are then two cases depending on the occurrence of 2m φ in partitions: T hΓ1 ` ∆1 , 2m φ, ¬2m φ ∧ β [ST ]i T h¬2m φ ∧ β, Γ2 ` ∆2 [ST ]i T hΓ1 ` ∆1 , 2m φ ∨ β [ST ]i T h2m φ ∨ β, Γ2 ` ∆2 , 2m φ [ST ]i Theorem 3 (Craig Interpolation). For any two formulas φ and ψ, if |= φ → ψ, then there is a formula β, such that |= φ → β, |= β → ψ and Sym(β) ⊆ Sym(φ) ∩ Sym(β), provided that there is a proposition p such that p ∈ Sym(φ) ∩ Sym(β). Proof. Assume |= φ → ψ, then by Corollary 1, φ ` ψ is derivable in G. By Lemma 1, there is a formula β, such that φ ` β and β ` φ are derivable in G0 . Let p ∈ Sym(φ) ∩ Sym(β). Now, let β 0 be obtained from β by replacing > by ¬(p ∧ ¬p). It is straightforward that φ ` β and β ` φ are derivable in G, and hence (by Corol- lary 1) |= φ → β and |= β → ψ. 21 5 Definability and Consistency Definition 3 (Implicit definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk are propositions occurring in it. We say φ(p, p1 , . . . , pk ) defines p implicitly if |= (φ(p, p1 , . . . , pk ) ∧ φ(p0 , p1 , . . . , pk )) → (p ↔ p0 ) where p 6= p0 . Definition 4 (Explicit definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk are propositions occurring in it. We say φ(p, p1 , . . . , pk ) defines p explicitly, when |= φ(p, p1 , . . . , pk ) → (p ↔ ψ) where Sym(ψ) ⊆ Sym(φ(p, p1 , . . . , pk )) \ {p}. Theorem 4 (Beth Definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk are propositions occurring in it. If φ(p, p1 , . . . , pk ) defines p implicitly, then φ(p, p1 , . . . , pk ) defines p explicitly. Proof. From the implicit definability assumption, it is easy to see that |= (φ(p, p1 , . . . , pk ) ∧ p) → (φ(p0 , p1 , . . . , pk ) → p0 ) By the Craig Interpolation Theorem 3, we then obtain |= (φ(p, p1 , . . . , pk ) ∧ p) → ψ |= ψ → (φ(p0 , p1 , . . . , pk ) → p0 ) where Sym(ψ) ⊆ Sym(φ(p, p1 , . . . , pk )) \ {p}. Before definining the notion of consistency, we need a precise description of some concepts. An axiom system is a finite set of formulas. An axiom sequence is a (possibly empty) subset of an axiom system. We say a sequent S is derivable (provable) in G from an axiom system A, if there is an axiom sequence A0 of A, such that `G A0 , S. Definition 5 (Consistency). An axiom system is inconsistent if the empty sequent is derivable from it. We say an axiom system is consistent if it is not inconsistent. Theorem 5 (Robinson Joint Consistency). Consider two consistent axiom systems A1 and A2 , if for any formula φ, such that Sym(φ) ⊆ Sym(A1 ) ∩ Sym(A2 ), it is not the case that both φ and ¬φ are derivable from A1 and A2 (or A2 and A1 ), respectively, then A1 ∪ A2 is consistent. Proof. We prove the contrapositive. If A1 ∪ A2 is not consistent, then there are two axiom sequences A01 and A02 of A1 and A2 , resp., such that A1 , A2 ` are derivable in G. Recall each A1 and A2 is consistent, then not empty. By Lemma 1, there is an interpolant φ, where Sym(φ) ⊆ Sym(A1 ) ∩ Sym(A2 ), such that A1 ` φ and φ, A2 ` (hence A2 ` ¬φ) are both derivable in G0 . As in the proof of Theorem 3, it is straight forward that both A1 ` φ and A2 ` ¬φ are also derivable in G by replaceing all the occurrences of > in φ by ¬(p ∧ ¬p) for a p ∈ Sym(A1 ) ∪ Sym(A2 ). 22 6 Conclusions In this paper, we describe a constructive proof of the Craig interpolation property. The proof is based on the Maehara technique on a complete cut-free tree-hypersequent cal- culus. An interpolant algorithm can easily be inferred from the proof. A complexity analysis of this algorithm is prospected as further research. We are also interested in constructive interpolation proofs for other more expressive modal logics, such as Km with converse, CTL and the µ-calculus. References 1. Beth, E.W.: On Padoa’s method in the theory of definition. Journal of Symbolic Logic 21(2) (1956) 2. Bílková, M.: Uniform interpolation and propositional quantifiers in modal logics. Studia Logica 85(1) (2007) 3. Blackburn, P., Benthem, J.F.A.K.v., Wolter, F.: Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York, NY, USA (2006) 4. ten Cate, B., Franconi, E., Seylan, I.: Beth definability in expressive description logics. J. Artif. Intell. Res. 48 (2013) 5. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1) (1979) 6. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3) (1957) 7. D’Agostino, G.: Interpolation in non-classical logics. Synthese 164(3) (2008) 8. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge, MA, USA (2003) 9. Fitting, M., Kuznets, R.: Modal interpolation via nested sequents. Ann. Pure Appl. Logic 166(3) (2015) 10. Gabbay, D.M.: Craig’s interpolation theorem for modal logics. In: Hodges, W. (ed.) Confer- ence in Mathematical Logic — London ’70. Lecture Notes in Mathematics. Springer (1972) 11. Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowl- edge and belief. Artif. Intell. 54(2) (1992) 12. Hintikka, J.: Knowledge and Belief. Ithaca: Cornell University Press (1962) 13. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive de- scription logics. In: Walsh, T. (ed.) IJCAI, Proceedings of the 22nd International Joint Con- ference on Artificial Intelligence. IJCAI/AAAI (2011) 14. Madarász, J.X.: The Craig interpolation theorem in multi-modal logics. Bulletin of the Sec- tion of Logic 3(24) (1995) 15. Maksimova, L.: Amalgamation and interpolation in normal modal logics. Studia Logica 50(3-4) (1991) 16. Maksimova, L.L.: Interpolation theorems in modal logics and amalgamable varieties of topo- logical boolean algebras. Algebra and Logic 18(5) (1979) 17. Marx, M.: Interpolation in modal logic. In: Haeberer, A.M. (ed.) Algebraic Methodology and Software Technology, 7th International Conference, AMAST, Proceedings. Lecture Notes in Computer Science, vol. 1548. Springer (1998) 18. McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer (2018) 23 19. Munoz-Toriz, J.P., Bárcenas, E., Martínez-Ruiz, I., Arrazola-Ramírez, J.R.E.: (Hy- per)sequent calculi for the ALC(S4) description logics. Computación y Sistemas 20(1) (2016) 20. Nguyen, L.A.: Analytic tableau systems and interpolation for the modal logics kb, kdb, k5, KD5. Studia Logica 69(1) (2001) 21. Poggiolesi, F.: Sequent calculi for modal logic. Ph.D. thesis, Università degli Studi di Firenze, Université Paris I Panthéon-Sorbonne (2008) 22. Robinson, A.: A result on consistency and its application to the theory of definition. Journal of Symbolic Logic 25(2) (1960) 24