On Axiomatization of Boolean Modalities*

Fengkui Ju

College of Philosophy and Sociology,Beijing Normal University fengkui.ju@bnu.edu.cn

Xiangmei Hu

Yiwu Experimental School Attached to Zhejiang Normal University hu_xiangmei@126.com

On Axiomatization of Boolean Modalities*

Fengkui Ju

College of Philosophy and Sociology,Beijing Normal University fengkui.ju@bnu.edu.cn

Xiangmei Hu

Yiwu Experimental School Attached to Zhejiang Normal University hu_xiangmei@126.com

.The modality constructors complement,intersection and union,called boolean modalities,raise the issue of completeness.Union is modally definable but neither of the other two is.This means that it is nontrivial to prove the completeness of the logics having them. G.Gargov and S.Passy introduces a way,called copy method,to handle them as a whole. This method does not work for strong completeness and can not separately handle the three modalities either.We in this paper improve this method to a more general one without these disadvantages.

PII:1674-3202(2015)-01-0023-14

1 Introduction

1.1 Boolean Modalities

Boolean Modal Logic(BML),proposed in[4],is a normal modal logic and also a propositional dynamic logic.Its language is an extension of Propositional Calculus (PC)with a set of modalities.This set has a structure:the composite modalities in it are generated from the atomic ones in it by three modality constructors:complement, intersection and union.Let Π0be a countable set of atomic modalities and Φ0a countable set of atomic propositions.Let a range over Π0and p over Φ0.The sets ΠCIUof modalities and ΦCIUof propositions of BML are defined as follows1:

Here 1 is the universal modality.The empty modality 0 is defined as.The dual[α]φ of〈α〉φ,other routine propositional connectives and the falsity⊥are defined in the usual way.

1Here C,I and U in ΠCIUand ΦCIUrepresent complement,intersection and union respectively.

The semantics of BML is a standard relational semantics:modalities are binary relations and modality constructors are operations of binary relations.A model M of ΦCIU,called a ΦCIU-model,is a tuple(W,{Rα|α∈ΠCIU},V)where W is a nonempty set of states,V is a function from Φ0to 2W,and the set{Rα|α∈ΠCIU} meets the following conditions:

M,w⊩φ,φbeingtrueatthestatew inthemodelM,isdefinedasusual.Aformulaφ isvalid ifandonlyifforanyMandw ofM,M,w⊩φ.Themodalityconstructors-,∩and∪are the operations of complement,intersection and union of binary relations. They are called boolean modalities for this reason.

Each modality of BML can be intuitively viewed as an action.One way to look at BML is that it is a logic of actions:〈α〉φ indicates that there is a way to perform the action α s.t.φ is the case after α is done;[α]φ says that φ is the case after α is done in whatever way.One area where BML has applications is deontic logic which concerns agents’actions.For instance,BML serves as the basis of the deontic logics introduced in[5]and[6].In what follows,we also call modalities as actions and modality constructors as action constructors.

1.2 Our Work

Union of binary relations is modally definable;however,neither complement norintersection is.This means that showing the completeness of BML is not a straightfor ward task.The completeness is accomplished by[3].Its proof uses such a property of BML:any action can be equivalently transformed to an action which is what we call complete normal forms.Suppose that we are considering only finitely many atomic actions a1,...,an.The actions a1∩···∩an,...,are called basic blocks where each atomic action occurs once.There are 2nbasic blocks.A union of some basic blocks is called a complete normal form w.r.t.a1,...,an.For a ΦCIU-model, basic blocks are like atomic parts of the universe of binary tuples:they are pairwise disjoint;the union of them is the whole universe;any action is the union of some of them.The core part of the proof presented in[3]is how to get these atomic parts right in the canonical model.2In this paper,we use some terminologies about completeness of modal logics such as“canonical”without giving any explanations,and also some general results for modal logics without giving any proofs.For the details of them,see[1].It does this by using a technique of transforming models called copy method.

Completenormalformsarerelativetofinitelymanyatomicactionsandthisproof shows only the weak completeness of BML.This is one disadvantage of the method. There are seven possible combinations of the three boolean modalities:(1)-;(2)∩;(3)∪;(4)-,∩;(5)-,∪;(6)∩,∪;(7)-,∩,∪.Each of them corresponds to a sublogic of BML,i.e.,the logic taking only the action constructors in this case;the last case corresponds to BML itself.The completeness of the logic for the case(3)is not interesting,as there is a modal formula which is canonical for union.The logics for the cases(4)and(5)have the same expressivity as BML.Therefore,from the perspective of axiomatization,only three among the seven cases are interesting:(1), (2)and(6).The proof in[3]is not applicable for the cases(2)and(6),simply because there is no complement there.This is another disadvantage of it.

We in this paper improve the copy method to a more general one which can handle the strong completeness for all these logics in a similar way.The main improvement is that we use a translation of actions into PC and a notion called the set of negative requirements which will be explained later.In what follows,we first present anaxiomatizationforBMLandshowitscompletenessbytheimprovedmethod.During presenting the proof,we point out its key steps.Then we show the completeness of other interesting sublogics of BML by focusing on these steps.

2 Completeness of LCIU

We use LCIUto denote Boolean Modal Logic in the sequel.

2.1 Axiomatization

Let ΦPCbe the language of PC generated from Φ0under¬,∧and∨,where Φ0is a countable set of atomic propositions.

Definition 1(Translation)σ:ΠCIU→ΦPCis such a function:

ασis called the translation of α in ΦPC.

The axiomatization of the logic LCIUconsists of four classes of axioms:

A.The basic axioms of normal modal logics:

B.The axiom for union:〈α∪β〉φ↔(〈α〉φ∨〈β〉φ).

C.The axioms for the universal modality:

D.The universal axiom:〈α〉φ→〈β〉φ where ασ→βσis a tautology in PC. and two inference rules:

1.Modus Ponens:given φ and φ→ψ,prove ψ;

2.Generalization:given φ,prove[α]φ.

As we will see later,the universal axiom is an axiom of all the axiomatizations we presentforthesublogicsofBML.ToshowthestrongcompletenessofLCIU,itsuffices to show that for any consistent set Σ of formulas,there is a ΦCIU-model N and a state s of it s.t.N,s⊩Σ.Let Σ be a consistent set.

2.2 The Canonical Model and Its Generated Submodel

Definition 2(Canonical Model)is a model where

1.WCis the set of maximal consistent sets;

2.Rαuv⇔for any φ,φ∈v implies〈α〉φ∈u;

3.V(p)={u∈WC|p∈u}.

By the so called Lindenbaum’s Lemma and Truth Lemma for modal logic,there is a w ∈WCs.t.MC,w ⊩ Σ.It can be verified that this model has the following properties:

Lemma 1

The class C of axioms guarantee thatis an equivalence relation on WC;however, it can be verified thatIt might not be the case thatMCisnotaΦCIU-model.WewanttoproperlytransformMCtoaΦCIU-model.

Let M=(W,{Rα|α∈Π},V)be the generated submodel of MCfrom w under.Asgeneratedsubmodelspreservemodalsatisfiability,wehaveM,w⊩Σ. By Lemma 1,we can see that the following lemma holds:

Lemma 2

M might not be a ΦCIU-model either,as Rα∩Rβ⊆Rα∩βstill might not hold.

2.3 Imitations

Let ω be the number of the atomic actions.We now define two crucial notions.

Definition 3(Negative Requirements)For any u,v∈W,Γuv={¬ασ|¬Rαuv}. Γuvis called the set of negative requirements w.r.t.u and v.

Definition 4(Approved Valuations)For any u,v∈W,Fuvis the collection of all the valuations F in PC s.t.F⊩Γuv.Fuvis called the set of approved valuations w.r.t. u and v.

By a valuation in PC,we means a function from Φ0to{1,0}.Let κ be the cardinality of Fuv.κ≤2ω,as there are at most 2ωvaluations.Enumerate the elements of Fuvas F1,...,Fκ.

Lemma 3(Well-definedness Lemma)Fuvis not empty for any u,v∈W.

ProofAssume Fuvis empty.Then Γuvis not consistent.Then there are actionstautology.Thenis a tautology.Aswe know that(α1∪···∪αn)σis a tautology.Then(α1∪···∪αn)σ↔ ⊤is a tautology,that is,(α1∪···∪αn)σ↔ 1σis a tautology.By the Universal Axiom, we getBy Lemma 2,R1=W ×W. ThenBy Lemma 2,Rα1uv or...or Rαnuv.Sincewe know¬Rα1uv,...,¬Rαnuv.Here we get a contradiction. □

Define g:{δ|1≤δ≤2ω}→{δ|1≤δ≤κ}as a surjective function.As Fuvis not empty,1≤κ.This means that{δ|1≤δ≤κ}is not empty.Since κ≤2ω,we know that g is well-defined.g is called the distribution function in the sequel.Note that g is also relative to u and v.The intuitive meaning of g will be explained later.

Let W1,...,W2ωbe 2ωpairwise disjoint sets which have the same cardinality with W.For any i s.t.1≤ i≤ 2ω,let fibe a bijective function from Wito W. We now define 2ωmodels with these sets as universes where the sets of negative requirements play a role.

Definition 5(Imitations)For any i s.t.1≤i≤2ω,Mi=is such a model:

Each Miis called an imitation of M.

Here are some explanations.Given any s,t∈Wi.fi(s)and fi(t)are elements of W.The set Γfi(s)fi(t)of negative requirements w.r.t.fi(s)and fi(t)contains the information about which relations fi(s)and fi(t)do not have in the original model M.F1,...,Fκare all the valuations in PC satisfying these requirements.Intuitively, eachFirepresentsapossibilityofwhatrelationsfi(s)andfi(t)canbeinwithoutviolating any of the requirements.There are at most 2ωsuch possibilities.W1,...,W2ω are 2ωcopies of W.On each of such copies,we realize a possibility.The distribution function g specifies which possibilities are realized in which copies.Since g is surjective,all the possibilities are realized in some copy.g might not be injective, which means that some different copies might share one same possibility.The Figure 1 helps to understand this.

Figure 1:Imitations

For any imitation Miand any relationof it,is defined essentially by the truth values of the translation of α in all the valuations assigned to i.This guarantees that each Miis a ΦCIU-model:

Lemma 4

Although the imitations of M might be different from M,they have some similarity with M,as shown by the following lemma.

Lemma 5(Lemma of Primary Bounded Morphisms)

2.Suppose Rαuv.We first show that Γuv∪{ασ}is consistent.Assume not.Then Fg(i)⊩ ασwhere Fg(i)∈ Ffi(s)fi(t).Assume Thenthereareα1,...,αn∈¬ασis a tautology.Thenis a tautology.As(α1∪···∪αn)σ=isatautology.BytheUniversalAxiom,weknowBy Lemma 2, Rα1uv or…or Rαnuv.As,we know¬Rα1uv,...,¬Rαnuv. Here we have a contradiction.Then Γuv∪{α}is consistent.Then there is a valuation F in PC s.t.F⊩Γuv∪{α}.Then F=Fjfor some Fj∈Fuv.Let i be s.t.g(i)=j. Then Fg(i)⊩ασ.Then□

ThislemmaisnotsayingthateachfiisasocalledboundedmorphismfromMitoM. Bounded morphisms have two conditions:the forth and back conditions.The first item of this lemma tells that each fisatisfies the first condition.But what the second item says is not that each fisatisfies the back condition.It is not even that there is a fimeeting the condition.It is something else.

2.4 The Final Model

Definition 6(The Final Model)N=(U,{Sα|α∈Π},Z)is such a model:

N is a mix of all imitations of M.Let us call s and s′of U each others twins if f(s)=f(s′).

Note that one can have many twins in this sense.The imitations are mixed in such a way:for any s,t∈U,if s and t are in the relation Sα,then any of s’s twins and t are in Sα.We illustrate this by Figure 2.s and s′are twins and both of them corresponds to w.As s and t have the relationin the model M1,s′and t have the relation Sain the final model N.Similarly,as s′and t′have the relationin M2,s and t′have the relation Sbin N.

The following lemma says that N is a ΦCIU-model:

Figure 2:The Final Model

Lemma 6

Proof Given s,t∈U.Let i and s′be s.t.t,s′∈Wiand fi(s′)=f(s).

Let f=f1∪···∪f2ω.Then f is a function from U to W.Since each fiis surjective,f is surjective as well.

Lemma7(LemmaofBoundedMorphism)f isaboundedmorphismfromNtoM:

1.if Sαst,then Rαf(s)f(t);

2.if Rαf(s)v,then there is a t∈U s.t.Sαst and f(t)=v.

RecallM,w⊩Σ.Sincef issurjective,thereisas∈U s.t.f(s)=w.Asmodal satisfiability is invariant under bounded morphisms,we know N,s⊩Σ.Finally,we have the following proposition:

Proposition 1(Strong Completeness of LCIU)The logic LCIUis strongly complete w.r.t.the class of ΦCIU-models.

3 Completeness of LIand LIU

We use ΦIto denote the sub-language of ΦCIUwith only the action constructor intersection and ΦIUto denote the sub-language of ΦCIUwith only intersection and union.Let ΠIand ΠIUbe the sets of actions of ΦIand ΦIUrespectively.A model of ΦIis called a ΦI-model and a model of ΦIUis called a ΦIU-model.Let LIbe the logic of ΦIand LIUthe logic of ΦIU.Now we present axiomatizations for LIand LIUand show their completeness.As we can see,both of the two proofs are similar with the one for the completeness of LCIU.

3.1 LI

The axiomatization of LIhas two classes of axioms:(i)the basic axioms for normal modal logics;(ii)the universal axiom:〈α〉φ→ 〈β〉φ where ασ→ βσis a tautology.Note that here α and β contain only the action constructor∩,and ασand βσcontain only the propositional connective∧.The inference rules of the axiomatization for LIare(i)modus ponens and(ii)generalization.Let Σ be a consistent set of formulas.We want to find a ΦI-model N and a state s of it s.t.N,s⊩Σ.

The canonical model M=(W,{Rα|α∈Π},V)of LIis defined as Definition 2.Let w ∈W be s.t.M,w⊩Σ.By the Universal Axiom,we know Rα∩β⊆Rα∩Rβ.M might not be a ΦI-model,as Rα∩Rβmight not be a subset of Rα∩β. Foranyu,v∈W,Γuv,thesetofnegativerequirementsw.r.t.uandv,andFuv,theset of approved valuations w.r.t.u and v,are defined as Definition 3 and 4 respectively.

Lemma 8For any α1,...,αn∈is not a tautology.

To see that this lemma holds,simply let all the atomic propositions occurring inbe false.This lemma says that none of the actions in ΠIis equivalent to the universal modality.With the help of this lemma,we can show the following one:

Lemma 9(Well-definedness Lemma)For any u,v∈W,Fuvis not empty.

Let ω be the number of the atomic actions and κ the number of the elements of Fuv.The distribution function g is defined as before.Lemma 9 implies that g is well-defined.Let W1,...,W2ωbe 2ωdisjoint copies of W.For any i s.t.1≤ i≤2ω,define fias a bijective function from Wito W.For any i,define an imitationof M in the way of Definition 5.It can be easily verified that each Miis a ΦI-model:

Lemma 10For any α,α1,...,αn∈ΠI,is a tautology, thenis a tautology for some i.

ProofSupposethatασ→isatautology.Assumethatforanyi≤n,is not a tautology.Since any of α,α1,...,αnis an intersection of some atomic actions,any of ασ,is a conjunction of some atomic propositions. Then for any i,there is an atomic proposition inwhich is not occurring in ασ, otherwiseis a tautology.Consider a valuation of PC in which only such atomic propositions are false.Then ασis true and anyis false.Then ασ→is false.This is impossible. □

With his lemma,we can show a similar result with Lemma 5 which shows some similarity between M and its imitations.

Lemma 11(Lemma of Primary Bounded Morphism)

Proof1.SupposeThen Fg(i)⊩ ασwhere Fg(i)∈ Ffi(s)fi(t).AssumeThen We get a contradiction.

2.SupposeRαuv.WefirstshowthatΓuv∪{α}isconsistent.Assumenot.Then there areis a tautology.Thenis a tautology.By Lemma 10,is a tautology for some i.By the Universal Axiom,Rα⊆Rαi.Since Rαuv,Rαiuv.∈Γuv,we know¬Rα1uv,...,¬Rαnuv.We get a contradiction. Then Γuv∪{α}is consistent.Then there is a valuation F in PC s.t.F⊩Γuv∪{α}. Then F=Fjfor some Fj∈Fuv.Let i be s.t.1≤i≤ 2ωand g(i)=j.Then Fg(i)⊩ασ.Then□

The final model N=(U,{Sα|α∈Π},Z)is defined as Definition 6.It can be checked that N is a ΦI-model:Sα∩β=Sα∩Sβ.Define a function f:U→W as f1∪···∪f2ω.The following lemma implies that modal satisfiability is invariant under f.Finally,we have the strong completeness of LI.

Lemma 12(Lemma of Bounded Morphism)f is a bounded morphism from N to M:

Proposition 2(Strong Completeness of LI)The logic LIis strongly complete w.r.t. the class of ΦI-models.

The logic LIhas applications in epistemic logic.For instance,the intersection modality is used to formalize distributed knowledge in[2]and[7].Both of them present a proof for the completeness of LI.The two proofs are different from ours,although the former also uses some kind of copy technique.

3.2 LIU

The axiomatization of LIUhas three classes of axioms:(i)the basic axioms for normalmodallogics;(ii)theaxiomforunion;(iii)theuniversalaxiom:〈α〉φ→〈β〉φ where ασ→βσis a tautology.Here α and β do not contain complement and ασand βσdo not contain negation.The inference rules of the axiomatization for LIUare(i) modus ponens and(ii)generalization.The proof for the strong completeness of LIUis similar with the proof for the strong completeness of LI.Here we just show some key lemmas;all the notions used in the sequel are defined as above.

Lemma 13For any α1,...,αn∈ΠIU,is not a tautology.

ProofSinceα1,...,αndonothavecomplement,donothavenegation. Thendoes not contain complement.Let F be a valuation of PC s.t. F(p)=0 for any atomic proposition p.It can be seenThenis not a tautology. □

Lemma 14(Well-definedness Lemma)For any u,v∈W,Fuvis not empty.

ProofAssumethatFuvisempty.ThenΓuvisnotconsistent.Thenthereareα1,...,→⊥is a tautology.Thenis a tautology.By Lemma 13,this is impossible. □

Lemma 15(Lemma of Primary Bounded Morphism)

Proof1.SupposeThen Fg(i)⊩ ασwhere Fg(i)∈ Ffi(s)fi(t).AssumeThenWe get a contradiction.

2.Suppose Rαuv.We claim that Γuv∪{α}is consistent.Assume not.Then there areis a tautology.Then ασ→is a tautology.As(α1∪···∪αn)σ=is a tautology.By the Universal Axiom, Rα⊆Rα1∪··∪αn.Since Rαuv,Rα1∪··∪αnuv.By the Axiom for Union,Rα1uv or…or Rαnuv.we knowWe get a contradiction.Then Γuv∪{α}is consistent.Then there is a valuation F in PC s.t. F⊩Γuv∪{α}.Then F=Fjfor some Fj∈Fuv.Let i≤2ωbe s.t.g(i)=j.ThenThen□

3.3 Two Remarks

The improved method we present also works for the completeness of the logic LCwhose language ΦCcontains only the action constructor complement.We here just describe the basic ideas of the proof.The core part of this proof is how to get=W×W-Rα.The universal modality is expressible in ΦCand we introduce it as a derived expression.The special axioms of the axiomatization of LCinclude the three axioms for the universal modality,listed in the subsection 2.1,and the universal axiom.With the first class of axioms,we can properly transform the canonical model toabettermodelMwhereistheuniversalrelation,aswhatwedoinproving the completeness of LCIU.Then we define the imitations of M and the final model as before.The final model is a ΦC-model and it is equivalent to M.Finally we have the strong completeness of LC.

In order to show the weak completeness of the sublogics of BML,we for some purpose might want to show that a consistent formula is satisfiable in a finite model. Our method has no problems with this issue,but we have to adapt it in some places. The main change is this:we do not copy a model for 2ωtimes and we just copy it for 2ntimes,where n is the number of the atomic actions occurring in the formula in consideration;accordingly,the crucial result,the lemma of primary bounded morphism,is not generally for all actions,but just for those generated from the n atomic actions.For the weak completeness,this is enough.

4 Conclusion

The set of negative requirements plays an important role in constructing proper models in the proofs of completeness of Boolean Modal Logic and its sublogics. Modal satisfiability is invariant under bounded morphisms;bounded morphisms require the forth and back conditions to be satisfied.On the one hand,the set contains enough information of the forth condition;on the other hand,it reserves enough room for the satisfaction of the back condition.The expressivity of the formulas in this set depends on what action constructors are in consideration.This feature offers the method a general taste.

The translation we use in this work is from the set of actions to the language of Propositional Calculus.Such a translation is not very intuitive;a more natural one is from the action set to the first-order language.More specifically,each action should correspond to a first-order formula with two free variables.However,for the purposeof dealing with boolean modalities,the translation we present is enough,as boolean modalities do not essentially involve any quantifiers.Nonetheless,this might open a door to generalize this method to some more complex modalities such as composition which in fact contains existential quantification.

[1] P.Blackburn,M.de Rijke and Y.Venema,2002,Modal Logic,Cambridge:Cambridge University Press.

[2] W.van Der Hoek and J.-J.C.Meyer,1992,“Making some issues of implicit knowledge explicit”,International Journal of Foundations of Computer Science,3(2):193-223.

[3] G.Gargov and S.Passy,1990,“A note on boolean modal logic”,in P.P.Petkov(ed.), Mathematical Logic,pp.311-321,New York:Plenum Press.

[4] G.Gargov,S.Passy and T.Tinchev,1987,“Modal environment for boolean speculations”,in D.G.Skordev(ed.),Mathematical Logic and Its Applications,pp.253-263, Berlin:Springer US.

[5] R.Hilpinen,2001,“Deontic logic”,in L.Goble(ed.),The Blackwell Guide to Philosophical Logic,pp.159-182,Oxford:Blackwell.

[6] F.Ju and L.Liang,2013,“A dynamic deontic logic based on histories”,in D.Grossi,O. Roy and H.Huang(eds.),Logic,Rationality,and Interaction,vol.8196,pp.176-189, Berlin/Heidelberg:Springer.

[7] Y.N.Wáng and T.Ågotnes,2013,“Public announcement logic with distributed knowledge:Expressivity,completeness and complexity”,Synthese,190(1):135-162.

布尔模态的公理化

琚凤魁
北京师范大学哲学与社会学学院
fengkui.ju@bnu.edu.cn
胡祥梅
浙江师范大学附属义乌实验学校
hu_xiangmei@126.com

布尔模态（即模态生成算子补、交、并）涉及到了完全性问题。并模态是模态可定义的，但是补和交都不是。这意味着证明包含这三个模态的逻辑的完全性不是一件简单直接的事情。Gargov和Passy使用复制方法从整体上处理这三个模态，但是，这个方法不适用于强完全性，也不能单独处理这三个模态。本文改进了这个方法，使得改进后的方法更具一般性，并且没有这两个不足之处。

Received 2014-11-20

*This research was supported by the National Social Science Foundation of China(No.12CZX053) and the Fundamental Research Funds for the Central Universitie(No.SKZZY201304).Shujiao Li also has contributions to this work.We would also like to thank Jiahong Guo,Xinwen Liu,Hu Liu,Johan van Benthem and Yanjing Wang for their useful comments and kind help.