Craig Interpolation on the Logic of Knowledge

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 reason about knowledge [ 12 ]. More recently, reasoning about knowledge has become of much importance in many areas of computer science, such as distributed systems, cryptography, 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 representation [ 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 compute interpolants. 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 logics 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 includes 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 methods. 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 described 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 composed 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 interpolation 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 nonempty finite set of modalities MOD.

The set of formulas is inductively defined by the following grammar.

:= p j : j ^

j 2m 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: [[p]]M = fw 2 V (p)g [[: ]]M =W n [[ ]]M [[ ^ [[2m ]]M = fw j 8w0 2 W : if (w; w0) 2 Rm;

then w0 2 [[ ]]Mo We may also write M; w j= instead of w 2 [[ ]]M, M j= when for every w in M , we have that M; w j= , in which case we say M is a model of . If any Kripke structure is a model of , we write j= .

Definition 1 (Hilbert derivation system). We define the derivation system H by the following schemas and rules, for each m 2 MOD: A1 A2 ( A3 (: A4 2m(

! R1 R2 2m ! ( ! ) ! ( ! )) ! (( ! ! : ) ! ( ! ) ! ) ! (2m ! 2m )

) ! ( ! )) We say a formula n is derivable from H, written `H 1; 2; : : : ; n, such that for each i 2 f1; : : : ; ng: n, if there is a sequence – 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. ( ^ ) ! 2. 2m(( ^ 3. 2m(( ^ 4. 2m( ^

, which by notation is an instance of A1, : _ ) ! ), from 1 by R2; ) ! ) ! (2m( ^ ) ! 2m ), from A4; and ) ! 2m , from 2 and 3 by R1. _ ; Theorem 1 (Correctness [ 11 ]). For any formula , `H , if and only if, j= .

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 ( 1; : : : ; n ` 1; : : : ; k)I := ^

i ! i=1 k _ j=1 j where n and k are some positive integers.

In sequents, we often write ; or ; instead of f g [ , also ` instead of > ` , and ` in place of ` ?.

Tree hypersequents expressions are inductively defined by the following grammar: where S is a sequent and m is a modality. We extend the interpretation function of sequents for tree hypersequents as follows:

T :=S [ST ]

ST :=; j m : T; ST (S [ST ])I :=SI _ (ST )I

(;)I :=? (m : T; ST )I :=2mT 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; – S0 [ST ] hSi, provided that S0 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 0i between trees as expected: – T and T 0 are the same; – (S [ST ]) hT 0i, when ST hT 0i; – (m : T 0; ST 0) hT 0i; and – (m : T 00; ST 0) hT 0i, provided that T 00 is different than T 0 and ST 0 hT 0i. We also distinguish when m : T 0 occurs in a tree T , written T hm : T 0i: – (S [ST ]) hm : T 0i, when ST hm : T 0i; – (m : T 0; ST 0) hm : T 0i; and – (m0 : T 00; ST 0) hT 0i, provided that either m is different than m0 or T 00 is different than T 0, and ST 0 hm : T 0i. We say a sequent S occurs, under a modality m, in a finite sequence of tree hypersequents 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 : S0] instead of S [ST ], provided S0 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: – Propositional rules:

T hS; i

:L T h: ; Si T h ; ; Si

^L

T h ^ ; Si – Modal rules:

T hp; S; pi

T h ; Si T hS; : i T hS; i

T hS; :R T hS; i ^ i

^R T h2m ; S [m : ; S0]i 2mL

T h2m ; S [m : S0]i

T hS [m : ` ; ST ]i 2mR

T hS; 2m [ST ]i We now define the concept of derivation tree: – any rule (up to subtitution) of G is a derivation tree; – TT0 and T 0 T T 00 are derivation trees, provided that T 0 and T 00 are derivation trees, and – TT00 and T00 T T000 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

T h ` 2m:( ^ : ); 2m 2m:( ^ : ); 2m 2m:( ^ : ); 2m 2m:( ^ : ); 2m

` 2m 2m:( ^ : ); 2m ; :2m

` 2m:( ^ : ) ^ 2m

T h ; T h ` ` i ; : i ;

^ : i ` [m : :( ^ : ); ` ] :2LmL ` [m : ` ] 2mL ` [m : ` ] :R ^R 2mR :L

^L ` :(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, j= SI . ^ :2m `

^ :2m ) :R We define the set of non-logical symbols Sym( ) of a formula as follows: p ; – Sym(p) = f g – Sym(: ) = Sym( ); – Sym( ^ ) = Sym( ) [ Sym( ); and – Sym(2m ) = fmg [ 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 int1e;rpo2labnet,psaurctihtiothnastoTf h a1n`d 1,;resipaecntdivTelyh. T; he2n`ther2ei iasrae fdoerrmivualable ,incaGlle0,datnhde 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 `

`

T h2m ; ` [m : 0 ` 0]i By induction, there is an interpolant for the upper tree hypersequent. By the occurrence of 2m in partitions, we distinguish two cases: [m : ; 0 ` T h2m ; 1 ` 1; [m : ; 0 ` T h ; 2 ` 2 [m : ; 0 ` T h 1 ` T h ; 2m ; 2 ` We then construct the following interpolants: Consider now the last inference is the following: We obtain the following interpolant

T h

T h ` ` by induction: [m : ` ; ST ]i ; 2m [ST ]i There are then two cases depending on the occurrence of 2m in partitions: Theorem 3 (Craig Interpolation). For any two formulas and , if j= ! , then there is a formula , such that j= ! , j= ! and Sym( ) Sym( ) \ Sym( ), provided that there is a proposition p such that p 2 Sym( ) \ Sym( ). tPhreoroef.isAassfuomr meuj=la !,suc,hthtehnatby C`orollaarnyd1, `` isardeerdivearibvlaebilne Gin. BGy0.LLemetmpa 12, 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 Corollary 1) j= ! and j= ! .

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 j= ( (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 j= (p; p1; : : : ; pk) ! (p $ ) where Sym( )

Sym( (p; p1; : : : ; pk)) n fpg.

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

j= ( (p; p1; : : : ; pk) ^ p) ! ( (p0; p1; : : : ; pk) ! p0) By the Craig Interpolation Theorem 3, we then obtain j= ( (p; p1; : : : ; pk) ^ p) ! j=

! ( (p0; p1; : : : ; pk) ! p0) where Sym( )

Sym( (p; p1; : : : ; pk)) n fpg.

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 2 Sym(A1) [ Sym(A2).

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 calculus. 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.) Conference 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 knowledge 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 description logics . In: Walsh, T . (ed.) IJCAI, Proceedings of the 22nd International Joint Conference on Artificial Intelligence. IJCAI/AAAI ( 2011 )

14. Madarász , J.X. : The Craig interpolation theorem in multi-modal logics . Bulletin of the Section 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 topological 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 )

19. Munoz-Toriz , J.P. , Bárcenas , E. , Martínez-Ruiz , I. , Arrazola-Ramírez , J.R.E. : (Hyper)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 )