A New Way of Defining Deductive Consequence for Modal and Predicate Logic

Xuefeng Wen

Abstract.Deductive consequence has been defined in various ways in modal logic and predicate logic.Though most of them can be proved to be equivalent,they have different advantages and disadvantages.We propose a new way of defining deductive consequence of axiomatic systems for modal and predicate logic,by distinguishing two kinds of rules in an axiomatic system.We argue that the new definition not only inherits all advantages of existing definitions but also unifies all six consequences in modal and predicate logic.We show some pedagogical merits of the new definition as well.

1 Introduction

Basically,we have two approaches to defining a logic (or what follows from what).One is semantic approach,which specifies the semantic values of the formulas in a formal language and defines a semantic consequence associating the semantics to formalize what follows from what.The other is syntactic approach,which gives a proof system by specifying the rules of manipulating the formulas in a formal language,and defines a deductive consequence associating the proof system to formalize what follows from what.Usually,soundness and completeness are proved to show that the two approaches define the same logic,indicating the correctness of each other.

We have now various methods of defining proof systems:axiomatic systems,natural deduction systems,tableau systems,sequent calculi,etc.Deductive consequence is defined differently in different types of proof systems.Even within axiomatic systems,we have different ways of defining deductive consequence for modal logic and predicate logic.Though most of them can be proved to be equivalent,they have different advantages and disadvantages.

We attempt to propose a new way of defining deductive consequence in the context of axiomatic systems.We suppose the new definition is applicable to as many logics as possible.But we confine ourselves to modal and predicate logic in this paper.By modal logic,we mean propositional modal logic.By predicate logic,we mean classical first-order logic.Why are we interested in giving a new definition of deductive consequence for modal logic and predicate logic in particular? The reason is that the rule of necessitation in modal logic,namely inferring □φ from φ,and the rule of generalization,namely inferring ∀xφ from φ in axiomatic systems have caused some confusion for beginners and even for experts in logic.One consequence of the confusion is that there has been debate about whether the deduction theorem holds in modal logic(cf.[14]).Moreover,compared to classical propositional logic,various semantic consequences can be defined in modal logic and predicate logic,which makes the notion of deductive consequence for them more complicated.The new definition of deductive consequence attempts to inherit all advantages of existing definitions and avoid their disadvantages.Most importantly,the new definition attempts to give a unified notion for all semantic consequences in modal and predicate logic.We will see that various semantic consequences in modal and predicate logic can actually be unified into one notion.So a unified deductive consequence for them would be desirable.

The remaining part of the paper is organized as follows.Section 2 gives the new definition,under which the deduction theorem and the difference between derivable rules and admissible rules are revisited.Section 3 shows how the new definition can unify the six consequences in modal and predicate logic.Before concluding the paper,Section 4 compares the new definition with existing definitions.All proofs are given in the appendix.

2 A New Way of Defining Deductive Consequence

It is easily seen that the rules of necessitation and generalization are different from the rule of modus ponens.The latter preserves local truth.In modal logic,this means that at every world in every model,if φ and φψ are true,so is ψ.In predicate logic,this means that in every model with every assignment,if φ and φψ are satisfied,so is ψ.But the rules of necessitation and generalization do not preserve local truth.They only preserve global truth.In modal logic,this means that if φ is true at all worlds in a model,so is □ψ.In predicate logic,this means that if φ is satisfied in a model with all assignments,so is ∀xφ.But the difference between necessitation/generalization and modus ponens is not reflected in standard axiomatic systems.There is a reason why the difference is neglected.In classical propositional logic and classical first-order logic that cares about only sentences(namely formulas without free variables),with the deduction theorem and compactness,every valid inference can be reduced to a valid formula.Hence,a proof system can only care about theorems without paying attention to derivation with assumptions.In this case,we only care whether a rule preserves validity.In deriving theorems,the difference between necessitation/generalization and modus ponens is unimportant.

But if we do care about derivation with assumptions,without distinguishing necessitation/generalization from modus ponens,we may derive false conclusion from true premises,making the proof system unsound.Indeed,the difference is reflected in most existing definitions of deductive consequence for modal and predicate logic.Our idea is that the distinction should be made in an axiomatic system in the first place.This can not only make the distinction prominent,but also bring forth a clearer and unified notion of deductive consequence.Moreover,the distinction between derivable rules and admissible rules will be much clearer and natural.It may also shed new light on the deduction theorem.

First,we define precisely what a rule is.Then we redefine axiomatic systems,followed by the new definition of deductive consequence associating newly defined axiomatic systems.

2.1 Rules

For any set S,let ℘+(S)denote the set of all non-empty subsets of S.In the sequel,we suppose any language L is closed under,i.e.,for all φ,ψ ∈L,(φψ)∈L.

Definition 1(Rules).Given a language L,a rule in L is a relation R ⊆℘+(L)×L.A rule R is closed under substitution,if for every substitution σ,for every(Γ,φ)∈R,(Γσ,φσ)∈R.It is finite,if for every(Γ,φ)∈R,Γ is finite.

By this definition,the rules of modus ponens,necessitation,and uniform substitution in the modal language L□can be represented as follows.They are all closed under substitution and finite.

· Necessitation(RN): {({φ},□φ)|φ ∈L□}

· Uniform substitution(US): {({φ},φσ)|φ ∈L□,σ is a substitution in L□}.

In the tradition of abstract algebraic logic (e.g.[20,p.20]),instead of a subset of℘(L)×L,a rule in L is usually defined as an element in ℘(L)×L,so that({p,pq},q)and({q,qr},r)are two rules.In our definition,they are just two applications of the same rule,which is closer to the ordinary use.

2.2 Axiomatic systems

We redefine what an axiomatic system is,distinguishing two kinds of rules in it.

Definition 2(Axiomatic systems).An axiomatic system for L is a tripleS=(AxS,),where AxS⊆L is the set of axioms ofS,⊆℘+(L)×L is the set of inference rules ofSsuch that=Ø.Elements inare called local rules ofS;elements inare called global rules of ofS.

Intuitively,a local rule can be applied to assumptions (or premises),whereas a global rule can only be applied to axioms and theorems.The difference between them is clear in semantics,though often blurred in axiomatic systems.Normally,an axiomatic system for a propositional language contains at least one local rule,namely modus ponens,and at least one global rule,namely uniform substitution.

With the new definition of axiomatic systems,we can define three kinds of extensions of an axiomatic system.

Definition 3(Extensions).LetS=be an axiomatic system for L,Γ a set of formulas in L,and R a set of rules in L.

1.SΓ=is called an axiomatic extension ofS;

2.SR=is called a local extension ofS;

3.SR=is called a global extension ofS.

When Γ= {φ} and R= {R} are singletons,we writeSφ,SR,andSR,respectively,instead ofS{φ},S{R},andS{R}.Of course,the three kinds of extensions can be combined arbitrarily together,so that we have axiomatic and local extensions,axiomatic and global extensions,local and global extensions,and finally,axiomatic,local and global extensions,which will be simply called extensions.

By Definition 2,an axiomatic system for classical propositional logic can be represented by({PC1,PC2,PC3},{MP},{US}),where PC1–PC3 are listed below.

We denote it byPC.The minimal normal modal logic can now be represented byPCRNK,an axiomatic and global extension ofPC,namely

2.3 Deductive consequence

Before defining the deductive consequence of an axiomatic system,we define the set of theorems of it first.

Definition 4(Theorems).Given an axiomatic systemS=φ is a theorem ofS,if there exists a formal proof of φ inS,i.e.,if there is a finite sequence of formulas φ1,...,φnsuch that φn=φ and for each i ≤n,

· either φi∈AxS,or

· there exist Γ ⊆{φ1,...,φi－1}and an inference rulesuch that(Γ,φi) ∈R,i.e. φiis obtained from proceeding formulas in the sequence by applying an inference rule(either local or global)ofS.

We denote by Th(S)the set of all theorems ofS.The following proposition is straightforward from Definition 4.

Proposition 5.LetSandS′be two axiomatic system for L such that AxS= AxS′andThen Th(S)=Th(S′).

The proposition says that whether a rule of an axiomatic system is local or global does not affect its theorems.This may be the reason why they were not distinguished by early mathematicians like Hilbert,since they care more about theorems than about consequence.Proposition 5 does not hold for deductive consequence,which is defined below.

Definition 6(Deductive consequence).LetS=be an axiomatic system.We say that φ is derivable from Γ inS,or φ is a deductive consequence of Γ inS,denoted Γ ⊢Sφ,if there exists a formal derivation of φ from Γ inS,i.e.,if there is a finite sequence of formulas φ1,...,φnsuch that φn=φ and for each i ≤n,

· either φi∈Γ,or

· φi∈Th(S),or

· there exist Δ ⊆{φ1,...,φi－1}and a rulesuch that(Δ,φi)∈R,i.e.,φiis obtained from proceeding formulas in the sequence by applying a local rule ofS.

We call this way of defining deductive consequence segregated definition,emphasizing that local rules and global rules are segregated in an axiomatic system and treated differently in derivations.

We write ⊢Sφ if Ø ⊢Sφ.In some definitions,theorems are defined as a special case of deductive consequence,which makes ⊢Sφ just a different notation of φ ∈Th(S).Here,theorems are defined first,and deductive consequence is defined based on theorems.Thus the equivalence of the two notations needs a proof.

Proposition 7.LetSbe an axiomatic systems for L.For all φ ∈L,⊢Sφiffφ ∈Th(S).

LetSandS′be two axiomatic systems for L.We say thatSis a subsystem ofS′,orS′is a supersystem ofS,denotedS≤S′,if ⊢S⊆⊢S′.They are equivalent,denotedS≡S′,if bothS≤S′andS′≤S,namely, ⊢S= ⊢S′.In general,even if Th(S)=Th(S′),they may not be equivalent.

2.4 Rules revisited

Distinguishing local and global rules in an axiomatic system may shed new light on the notions of derivable and admissible rules.First,let us recall the definitions of them.

Definition 8.A rule R

1.is derivable inS,if for all(Γ,φ)∈R,Γ ⊢Sφ;

2.is admissible inS,if for all(Γ,φ)∈R,⊢SΓ implies ⊢Sφ.

In most textbooks,since a rule is taken to be a pair(Γ,φ)rather than a relation consisting of such pairs,substitution has to be used to define admissible rules,i.e.,(Γ,φ)is admissible if for all substitutions σ,⊢SΓσimplies ⊢Sφσ.This may cause some confusion for students,since the definition for derivable rules usually does not use substitutions,which produces a weird non-symmetry.This is caused because substitution is actually a part the rule rather than a part of admissibility.Treating a rule to be a relation will not only dispense the need of substitution in defining admissibility,but also make it more general,since it can apply to those rules that are not substitution closed.

Even if we do not distinguish local and global rules in an axiomatic system,the difference between derivable rules and admissible rules still remains.So why not reflect the difference in an axiomatic system in the first place,which will make the distinction between derivable rules and admissible rules more natural.In fact,local and global rules have an intrinsic connection with derivable and admissible rules,respectively.First,all finite local rules of an axiomatic system are derivable in it,and all finite local rules and global rules of an axiomatic system are admissible in it,as given by Proposition 9,whose proof is straightforward.

Proposition 9.LetSbe an axiomatic system for L.Then

1.all finite local rules ofSare derivable inS;

2.all finite local and global rules are admissible inS.

Second,derivable rules can be used as both additional local rules and additional global rules,and admissible rules can be used as additional global rules without changing the derivability of an axiomatic system,as given by Proposition 10.

Proposition 10.LetSbe an axiomatic system,D a set of derivable rules ofS,and A a set of admissible rules ofS.Then

(i)S≡SD;(ii)S≡SD;(iii)S≡SA;(iv)S≡(v)S≡SD∪A.

Traditionally,since both adding derivable rules and adding admissible rules as additional rules do not increase the theorems of an axiomatic system,it may cause beginners to wonder what the real difference between the two kinds rules is.By distinguishing local and global rules in an axiomatic system,the different effect of derivable and admissible rules can be articulated easily by Proposition 10 and the following proposition.

Proposition 11.SSA,for some axiomatic systemSand some set of admissible rules A ofS.

But we havePC≡PCA,for any set of admissible rules A ofPC,since all admissible rules ofPCare derivable in it.

2.5 The deduction theorem revisited

We say that an axiomatic systemSfor L admits the deduction theorem,if for all Γ ∪{φ,ψ}⊆L,Γ,φ ⊢Sψ implies Γ ⊢Sφψ.

The following proposition says that axiomatic and global extensions ofPCdo not destroy the deduction theorem.

Proposition 12.For any Γ ⊆L and any set of rules R in L,PCRΓ admits the deduction theorem.

The following corollary concerning the deduction theorem for modal logics is straightforward.

Corollary 13.All axiomatic and global extensions of ltKadmit the deduction theorem.

One interesting phenomenon is that most(if not all)axiomatic systems have only one local rule,namely,modus ponens.A possible explanation may be that any new local rule of the formcan be replaced equivalently by the corresponding axiom φψ.However,this is not always true,as the following example shows.

Example 1

Theorem 14.Let R be a rule in L andSan axiomatic system for L with modus ponens a local rule of it.Let

be the set of corresponding axioms for R.Then

1.SR≤S[R];

2.S[R]≤SR,ifSRadmits the deduction theorem;

3.SRadmits the deduction theorem,ifS[R] ≤SRand Th(S)contains PC1 and PC2.

Easily obtained from Theorem 14,the following corollary connects local rules and their corresponding axioms with the deduction theorem.Note thatPCcan also be replaced by intuitionistic logic.

Corollary 15.For any rule R,PCR≡PC[R]iff PCRadmits the deduction theorem.

3 Unifying the Concept of Logical Consequence

We show how the new segregated definition can be used to unify different consequences in modal and predicate logic.First,we show that various semantic consequences in modal and predicate logic can be unified into one notion.

3.1 Unifying semantic consequence

In modal logic,two truth consequences and two validity consequences can be defined:local truth consequence,global truth consequence,local validity consequence,and global validity consequence(cf.[30,p.37],[25,p.92],and[4,pp.31–32]).But validity consequences on standard Kripke frames are too strong to be axiomatized.So we consider general frames for them in the sequel.Let ⊩ltdenote the standard satisfaction relation in modal logic.

Given a class of framesF,

· φ is a local truth consequence of Γ inF,denoted Γφ,if for all framesF∈F,for all valuations V onF,for all worlds w inF,F,V,w ⊩ltΓ impliesF,V,w ⊩ltφ,whereF,V,w ⊩ltΓ meansF,V,w ⊩ltψ for all ψ ∈Γ;

· φ is a global truth consequence of Γ inF,denoted Γφ,if for all framesF∈F,for all valuations V onF,F,V ⊩gtΓ impliesF,V ⊩gtφ,whereF,V ⊩gtΓ meansF,V ⊩gtψ for all ψ ∈Γ,andF,V ⊩gtψ meansF,V,w ⊩ltψ for all w inF.

Given a class of general framesG,

· φ is a local consequence by validity of Γ inG,denoted Γφ,if for all general framesG∈f,for all worlds w inG,G,w ⊩lvΓ impliesG,w ⊩lvφ,whereG,w ⊩lvΓ meansG,w ⊩lvψ for all ψ ∈Γ,andG,w ⊩lvψ meansG,V,w ⊩ltψ for all admissible valuations V forG;

· φ is a global consequence by validity of Γ inG,denote Γφ,if for all general framesG∈F,G⊩gvΓ impliesG⊩gvφ,whereG⊩gvΓ meansG⊩gvψ for all ψ ∈Γ,andG⊩gvψ meansG,V,w ⊩ltψ for all admissible valuations V forGand all worlds w inG.

In predicate logic,two consequences can be defined(cf.[30,p.38]and[1]).Let|=ldenote the standard satisfaction relation in classical predicate logic.Fixing a predicate language L,

· φ is a local consequence of Γ,denoted Γ ⊢lφ,if for all modelsMfor L and all assignments g inM,M,g |=lΓ impliesM,g |=lφ,whereM,g |=lΓ meansM,g ⊩lψ for all ψ ∈Γ;

· φ is a global consequence of Γ,denoted Γ ⊢gφ,if for all modelsMfor L,M|=gΓ impliesM|=gφ,whereM|=gΓ meansM|=gψ for all ψ ∈Γ,andM|=gψ meansM,g |=lψ for all assignments g inM.

All the six logical consequences can be unified into one notion:preserving certain semantic value within certain domain.We formalize this idea as follows.The main idea is that we can squeeze the differences between various semantic consequences into semantics,while keeping the notion of consequence invariant.

Definition 16(Semantics).A semantics for L is a pairS=(DS,⊩S),where DSis the domain ofSand ⊩S⊆DS×L is the semantic value of L.We write m ⊩SΓ if m ⊩Sφ for all φ ∈Γ.

Definition 17(Semantic consequence).Given a semanticsS=(DS,⊩S)for L,the semantic consequence ofS,denoted ⊨S,is a subset of ℘(L)×L such that Γ ⊨Sφifffor all m ∈DS,m ⊩SΓ implies m ⊩φ.

Now all the above semantic consequences can be unified by ⊨S,withSa variant parameter corresponding to each semantic consequence.For instance,is now denoted ⊨ltF,indicating that it is a(unified)consequence indexed by the semantics ltF.The six semantics,including ltFF,are specified in Table 1.

It is easily seen that ⊨ltF⊆⊨gtF,⊨lvf⊆⊨gvf,and ⊨lPre⊆⊨gPre.

3.2 Unifying deductive consequence

Now we show how various deductive consequences corresponding to the above semantic consequences can also be unified into one notion,using segregated definition.The main idea is that we can squeeze the differences between various deductive consequences into axiomatic systems,while keeping the notion of consequence invariant.

Table 1:Semantics for 6 semantic consequences

Let us take the minimal normal modal logicKas an example to illustrate the application of our new definition of deductive consequence in modal logic.LetKbe the class of all frames andkthe class of all general frames.Then we have four semantic consequences ⊨ltK,⊨gtK,⊨lvk,and ⊨gvk.What are the deductive consequences for them,respectively? We do not need four notions of deductive consequence.Instead,we just need four axiomatic systems ltK,gtK,lvK,and gvK,which are specified by Table 2.

Table 2:Axiomatic systems for four consequences of K

In general,given any normal modal logicL(namely,a set of formulas that contains PC1,PC2,PC3,K and is closed under MP,RN,and US),supposeLis generated from Ax using the rules in R,including MP,RN,and US.This can always be achieved,for instance,letting Ax=Land R={MP,RN,US}.Now we define four axiomatic systems ltL,gtL,lvL,and gvLsimilarly by Table 3.

By Proposition 5,the four systems have the same set of theorems.But their deductive consequences are not the same in general.System gvLis stronger than gtLand lvL,which are stronger than lvL,as formalized by the following proposition.The proof is straightforward.

Proposition 18.For any normal modal logicL,

1.⊢ltL⊆⊢gtL⊆⊢gvL

2.⊢ltL⊆⊢lvL⊆⊢gvL

Table 3:Four axiomatic systems of L

For any Γ ⊆L□,let □ωΓ= {□nφ | φ ∈Γ,n ≥0},where □0φ=dfφ and□n+1φ=df□□nφ.For any φ ∈L□,let φ*= {φσ| σ is a substitution in L□}andThe following proposition says that all the other three systems can be reduced to ltL,and gvLcan be reduced to all the others.

Proposition 19.For any normal modal logicL,for any Γ ∪{φ}⊆L□,

1. Γ ⊢gtLφiff□ωΓ ⊢ltLφ;

2. Γ ⊢lvLφiffΓ*⊢ltLφ;

3. Γ ⊢gvLφiffΓ*⊢gtLφiff□ωΓ ⊢lvLφiff□ωΓ*⊢ltLφ.

SupposeLis sound and strongly complete with respect to the class of framesF.We will first show that the axiomatic systems ltLand gtLcorrespond respectively to the semantics ltFand gtF,in the sense that they determine the sames logical consequences.

3.2.1 Deductive consequence for local truth consequence

Let ⊢Lbe the deductive consequence defined by

which is the most popular definition in modal logic.We will discuss it in more detail in Section 4.The following lemma says that ⊢ltLis just the standard deduction consequence in modal logic.

Lemma 20.For any normal modal logicL,⊢ltL=⊢L.

The following corollary and theorem are immediate from Lemma 20.

Corollary 21.For any normal modal logicLand any Γ ∪{φ}, Γ ⊢ltLφ implies□Γ ⊢ltL□φ.

Theorem 22.For any normal modal logicLand any class of framesF,ifLis sound and strongly complete with respect to the class of framesF,then ⊢ltL=⊨ltF.

3.2.2 Deductive consequence for global truth consequence

The following lemma connects global truth consequence with local truth consequence.

Lemma 23.LetFbe any class of frames that is closed under point generated subframes.Then for any Γ ∪{φ}⊆L□,Γ ⊨gtFφiff□ωΓ ⊨ltFφ.

Now we can prove that the axiomatic system gtLcorresponds to the semantics gtF.

Theorem 24.LetLbe any normal modal logic andFany class of frames that is closed under point generated subframes.If ⊢ltL=⊨ltFthen ⊢gtL=⊨gtF.

We make two more comments on the deductive consequence ⊢gtL.In[16]and[17],global deductive consequence ofK45andKD45are given respectively for axiomatizing informational consequence advocated in[33]and[5].The global deductive consequenceforLis defined by

where ⊢Lis defined by(*).This makes one wonder which axiomatic system is the‘correct’one for informational consequence? In fact,bothK45andKD45are correct.And so isS5,as we have the following fact.

Fact 2For any Γ ∪{φ}⊆L□,□Γ ⊢K45□φiff□Γ ⊢KD45□φiff□Γ ⊢S5□φ.

I leave the check of the fact to the reader.The point is that if we use standard definition of axiomatic systems in which local and global rules are not distinguished together with (**)to define deductive consequence for informational consequence(which is intrinsically a global consequence by truth),then multiple non-equivalent axiomatic systems or logics are available,for we haveThis seems undesirable.If we use our segregated definition ⊢gtS5instead,however,the multiple correspondence disappears,as the following fact shows.

Fact 3Since RN is treated as a local rule in gtL,it seems that for ⊢gtL,assumptions play the same role as axioms.This was reflected in [32],wherewas used for the deductive consequence of the logic with Λ the set of axioms such that RN can be applied to assumptions.The author claimed that,compared with standard local consequencecannot distinguishφ fromφ,since both are equivalent toWe have to be very careful here.If Λ is a set of axiom schemas,i.e.,a set of axioms closed under substitution,then the claim is correct.If Λ is only a set of axioms,then it is not,since uniform substitution can be applied to axioms,but they cannot be applied to assumptions inIn this case,Λ1φ andφ are not equivalent.Compared toour definition ⊢gtLwould cause less confusion,since in it local and global rules are delimited clearly,and uniform substitution is treated as an explicit rule rather than hidden in axiom schemas.More formally,we have the following result.

Proposition 25.For any substitution closed Σ ⊆L□,for any Γ∪{φ}⊆L□,Γ ⊢gtKΣφiffΓ ∪Σ ⊢gtKφ.

The proposition does not hold if Σ is not substitution closed,for we have ⊢gtKpq but p ⊬gtKq.When gtKis replaced by gvK,the substitution closed condition can be removed(cf.Proposition 28).

LetG(L)be the class of general frames forL,i.e.,G(L)= {G|G⊩gvL}.Now we show that the axiomatic systems lvLand gvLcorrespond to the semantics lvG(L)and gvG(L),respectively.

3.2.3 Deductive consequence for local validity consequence

Let|φ|be the set of all maximal consistent sets ofLcontaining φ.LetGL=(FL,AL)be the canonical general frame forL.In particular,AL={|φ||φ ∈L□}.Thus for any admissible valuation V forGL,for each atom p,there exists ψpsuch that V(p)=|ψp|.In particular,the canonical valuation VLwith V(p)=|p|for each atom p is admissible forGL.

Lemma 26.Let V be any admissible valuation forGLsuch that V(p)= |ψp| for every atom p.For any w inGLand any φ ∈L□,

1.GL,V,w ⊩ltφiff GL,VL,w ⊩ltφδ,where δ is the substitution defined by δ(p)=ψpfor every atom p;

2.ifGL,VL,w ⊩ltφ*thenGL,w ⊩lvφ;

3.GL⊩gvL.

Now we can prove that the axiomatic system lvLcorresponds to the semantics lvG(L).

Theorem 27.For any normal modal logicL,⊢lvL=⊨lvG(L).

3.2.4 Deductive consequence for global validity consequence

In deductive consequence for global consequence by validity,premises play the same role as axioms,as the following proposition shows.The proof is straightforward:for all rules are local,whenever they are applicable to axioms,so are they to premises.

Proposition 28.For any Γ ∪Σ ∪{φ}⊆L□,Γ ⊢gvKΣφiffΓ ∪Σ ⊢gvKφ.

So for this deductive consequence,there is no need to consider axiomatic extensions ofK,as all of them can be reduced toK.However,other(local or global)extensions ofKare still worthy of study.

The following theorem states that the axiomatic system gvLcorresponds to the semantics of gvG(L).

Theorem 29.For any normal modal logicL,⊢gvL=⊨gvG(L).

Now all four semantics consequences in modal logic have their corresponding deductive consequences,which can be defined uniformly by segregated definition.For the two semantic consequences of predicate logic,we can do the same.For local consequence,we let the rule of generalization to be a global rule in the axiomatic system; for global consequence,we let the rule of generalization to be a local rule,keeping the notion of deductive consequence invariant.We leave the details to the reader.

4 Comparison to Other Definitions

Now we review various known definitions for deductive consequence of axiomatic systems in modal and predicate logic.

The first definition ignores derivation from assumptions and considers only theorems.We call it omitted definition,which is adopted by[18,p.25]and[31,Definition 5.3.1]in modal logic.As shown by Proposition 5,if only theorems are considered,there is no need to distinguish local rules and global rules.Also,since it cares only about theorems of a system,it considers only weak soundness and weak completeness.Though such a treatment is simple and clean,it lacks some generality,since there are logics that have no theorems but their logical consequences are not empty,for instance,Kleene’s three-valued logic(cf.[1]).In such cases,a logic defined by omitted definition would not be sufficient to reflect its semantics.Moreover,without derivation from assumptions,it lacks usability in proving theorems,since the deduction theorem is not available to simplify proofs.

The second definition follows the standard definition of deductive consequence for classical propositional logic,so that φ is a deductive consequence of Γ inS,if there is a formal derivation from Γ to φ,using assumptions in Γ,axioms schemas and all rules ofS.We call it classical definition,which is adopted by[11,p.126],[6,p.84]and[10,p.54]in modal logic,and by[19,p.87],[15,Def.4.2],[23,pp.79–80],and[21,Def.2.2.1]in predicate logic.In classical definition,just like modus ponens,necessitation in modal logic and generalization in predicate logic can be applied to assumptions without constraints.Unlike omitted definition,uniform substitution in modal logic is not treated as an inference rule any more;otherwise,we may drive any φ from p using the rule,which is obviously undesired.The major flaw of classical definition is that strong soundness generally fail under this definition(assuming standard local consequence).In modal logic in particular,in any axiomatic system with the rule of necessitation, □p would be a deductive consequence of p.But semantically □p is not entailed by p in general.Similarly,in classical predicate logic,∀xPx would be a deductive consequence of Px,whereas ∀xPx is not entailed by Px.This also fails the deduction theorem.Instead,a restricted or nonstandard version of the deduction theorem holds.The general failure of strong completeness means that the deductive consequence cannot reflect the semantic consequence fully.If logical consequence instead of theorems is what we care about,then classical definition is rather undesirable for modal logic and predicate logic.

The third one reduces the notion of derivation to proof,so that φ is a deductive consequence of Γ inS,if there is a formal proof of ∧Δφ for some finite Δ ⊆Γ.We call it reduced definition,which is adopted by[27,pp.9–10],[22,p.16],[7,Def.2.14],[13,Def.1.1.2],and [4,Def.4.4]in modal logic.Interestingly,though reduced definition is the most popular one in modal logic,it is rarely seen in predicate logic.Since derivations are reduced to proofs,there is no need to distinguish local and global rules under reduced definition.All rules,including uniform substitution in modal logic are treated as deriving new valid formulas from old ones.The deduction theorem holds almost trivially,and so does strong soundness.A drawback of reduced definition is that the deduction theorem becomes useless,since to prove φψ,we can no longer assume φ and apply inference rules to it to prove ψ.By reduced definition,we have to prove φψ directly.Another drawback is that the definition depends on the object language,which makes it not general enough for all logics.If the language of the logic does not contain material implication,which cannot be defined in the logic from other logical constants either,then we can no longer define deductive consequence in this way.So it lacks some generality.

The fourth definition hides the rule of necessitation(in modal logic)and generalization(in predicate logic)in axioms,so that all axioms are prefixed by any finite sequences of boxes in modal logic,and by any finite sequences of universal quantifiers in predicate logic.We call it deflationary definition,which is adopted by [3,pp.108–109],[9,pp.111–112],and [26,p.122]in predicate logic.Contrary to reduced definition,though it is popular in predicate logic,and has been suggested in provability logic by[28],according to[14],it has never been widely taken in modal logic.With the rule of necessitation/generalization hidden in axioms,both strong soundness and deduction theorem hold.Unlike reduced definition,the deduction theorem is of practical use now.Like classical definition and unlike reduced definition,uniform substitution also has to be hidden in axioms in modal logic.A drawback of deflationary definition is that when it is applied to non-normal modal logics,the rules for modality can no longer be hidden in axioms,but have to be stated as explicit rules for the set of axioms.For instance,for monotonic non-normal modal logics,we have to add the rule that if φψ is an axiom then □φ□ψ is an axiom.In that case,they are used essentially the same as global rules in segregated definition.

The fifth definition follows classical definition but restricts the application of the rule of necessitation/generalization in derivations.We call it bounded definition,which is adopted by [14,Def.1]in modal logic,and by [8,p.196],[24,Def.III],and [2,p.31]in predicate logic.In a derivation under this definition,the rule of necessitation/generalization can only be applied to those formulas that are derived without assumptions.Note that the restriction on the rule of generalization can be easily made wrong.In[8],the restriction is that the variable generalized cannot be be free in assumptions.As pointed out in[24],this is incorrect,since by this definition,∀x(AxAx)cannot be derived from Ax.When correctly restricted,both strong soundness and the deduction theorem hold.Like classical definition,uniform substitution is not treated as an inference rule in modal logic.A drawback of bounded definition is that the rule of necessitation/generalization has to be used very carefully in formal derivations,which makes it lack some usability.The drawback,however,can be easily removed by delimiting the use of necessitation/generalization more clearly.This is what we do in segregated definition,where treated as global rules,they can only be applied in proving theorems.

All the five definitions above lack uniformity.They cannot deal with validity consequence in modal logic.Among them,omitted definition is too coarse-grained to distinguish local and global consequence.Treating necessitation/generalization the same as modus ponens,classical definition is basically a global (truth)consequence.Restricting the use of necessitation/generalization in various ways,reduced definition,deflationary definition,and bounded definition are basically local(truth)consequences.

The sixth definition due to Fitting([12,Def.3.3.1])is rather unique,which integrates local and global truth consequence into one notion.We call it ternary definition.It separates assumptions of a derivation into two parts:a local part and a global part.Semantically,given a point model(M,w),global assumptions are taken to be true in all worlds ofM,whereas local assumptions are take to be true at w.Syntactically,a derivation from global assumptions Γ and local assumptions Λ now consists of two parts:a global part and a local part,with the global part coming first.In the global part,both modus ponens and necessitation can be applied to proceeding formulas and those in Γ;in the local part,only modus ponens can be applied to proceeding formulas and those in Λ.In this way,the deductive consequence becomes a ternary relation.Fitting denote it by Γ ⊢LΛφ,when there is such a derivation of φ inLfrom global assumptions Γ and local assumptions Λ.It is easily seen that when Γ=Ø the ternary definition becomes local consequence by truth,and when Λ= Ø,it becomes global consequence by truth.But treating deductive consequence to be a ternary relation seems a bit unorthodox.Moreover,it cannot deal with validity consequence either.

Segregated definition we proposed in Section 2 has all the properties we desire.Both strong soundness and the deduction theorem hold(for local consequence).Uniform substitution is an explicit rule in modal logic.It is usable and can be generalized to other logics.Most importantly,it unifies the six consequences in modal and predicate logic.The comparison is summarized by Table 4.

Table 4:Comparison of seven definitions of deductive consequence

5 Conclusion and Future Work

We propose a new definition of deductive consequence for modal logic and predicate logic,by distinguishing two kinds of rules in an axiomatic system.We show how the definition may shed new light on the distinction between derivable and admissible rules,as well as the deduction theorem.A key feature of the new definition is that,it can unify all six consequences in modal and predicate logic.

Distinguishing two kinds of rules in the context of axiomatic systems is not a new idea.For example,in [29],Sundholm distinguished rules of inference and rules of proof.In[1],Avron distinguished pure rules and impure rules.What we do is to take the distinction more seriously and make use of it to distinguish axiomatic systems,in order to obtain a uniform notion of deductive consequence of axiomatic systems.

Future work can be done both in theory and in application.In theory,we may explore the connection between the new definition and deductive consequence defined in other types of proof systems.For example,Fitting also distinguishes local and global rules in tableau systems for modal logic.What is the connection between Fitting’s rules and ours? In natural deduction systems and sequent calculi,a rule is treated as a relation between derivations rather than between formulas as in axiomatic systems.Can local and global rules also be distinguished there? In application,we may explore how the new definition can be applied to other logics,including nonnormal modal logics and substructural logics.

Appendix:Proofs

Proof of Proposition 7.The direction from right to left is obvious by Definition 6.The other direction is by induction on the length of the proof of φ.The only interesting case is that φ is obtained from φ1,...,φnby applying a local rule ofS.By inductive hypothesis,every φi∈Th(S),for 1 ≤i ≤n.Let πibe a formal proof of each φiinS,then(π1,...,πn,φ)is a formal proof of φ inS.Hence,φ ∈Th(S).

Proof of Proposition 10.

(i)The directionS≤SDis obvious.ForSD≤S,we first show that Th(SD) ⊆Th(S),by induction on the length of the formal proof of φ ∈Th(SD).The only interesting case is that φ is obtained from φ1,...,φnusing one of the rules in D.Then φ1,...,φn⊢Sφ,i.e.,there is a formal derivation δ of φ from{φ1,...,φn}inS.By inductive hypothesis,each φi∈Th(S)and thus has a formal proof πiinS.Now (π1,...,πn,δ)consists of a formal proof of φ inS.Hence,φ ∈Th(S).Now we show by induction on the length of the formal derivation of φ from Γ inSDthat Γ ⊢SDφ implies Γ ⊢Sφ.The only interesting case is that φ is obtained from φ1,...,φnusing one of the rules in D.Then φ1,...,φn⊢Sφ.Thus,there is a formal derivation δ of φ from{φ1,...,φn}inS.By inductive hypothesis,Γ ⊢Sφifor 1 ≤i ≤n.For each 1 ≤i ≤n,let δibe a formal derivation of φifrom Γ inS.Now(δ1,...,δn,δ)consists of a formal derivation of φ from Γ inS.Hence,Γ ⊢Sφ.

(ii)The directionS≤SDis obvious.ForSD≤S,notice that no local rules are added toS.Thus it suffices to show that Th(SD) ⊆Th(S).The proof is the same as that for Th(SD)⊆Th(S)above.

(iii)The directionS≤SAis obvious.ForSA≤S,it suffices to show that Th(SA) ⊆Th(S).By induction on the length of the formal proof of φ ∈Th(SA).The only interesting case is that φ is obtained from φ1,...,φnusing one of the rules in A.Then ⊢Sφifor 1 ≤i ≤n implies ⊢Sφ.By inductive hypothesis,we have φi∈Th(S)for 1 ≤i ≤n.By Proposition 7,⊢Sφifor 1 ≤i ≤n.By the admissibility of the rule, ⊢Sφ.By Proposition 7 again,φ ∈Th(S).

(iv)Straightforward from(i)and(iii).

(v)Straightforward from(ii)and(iii).

Proof of Proposition 12.Since PC1 and PC2 are available,and MP is the unique local rule,the proof for the deduction theorem ofPCis reusable forPCRA.

Proof of Proposition 11.ConsiderS=PCRN.By Proposition 9,RN is an admissible rule ofS.We show thatSSRN,in particular,p□p but p ⊬S□p.The former is obvious.For the latter,consider the standard relational semantics for modal logic.Since all axioms inSare valid,all local rules ofSpreserve local truth,and all global rules ofSpreserve validity,if p ⊢S□p then p ⊨K□p,where ⊨Kis the standard semantic consequence of the modal logicK.But p ⊭K□p.Hence,p ⊬S□p.

Proof of Example 1.Consider the standard relational semantics for modal logic.LetFbe any frame in which there is a world accessible from another(different)world.Then p□p is not valid inF.On the other hand,all the axioms ofPCRNare valid inF,and all the rules ofPCRNpreserve validity inF.Supposep□p,then p□p will also be valid inF,contradiction!

Proof of Theorem 14.For (i),suppose Γφ.First,we show that Th(SR) ⊆Th(S[R]),by induction on the length of the proof of the theorem ofSR.The only interesting case is that the theorem ψ is obtained from previous formulas φ1,...,φnin the proof using the rule R.Then by inductive hypothesis,adding the axiom φ1(φ2···(φnψ)···)and applying modus ponens n times will obtain ψ inS[R].Now we prove by induction on the length of the derivation of φ from Γ inSR.The only interesting case is still that ψ is obtained from previous formulas using the rule R.The proof goes in the same way.

For(ii),supposeSRadmits the deduction theorem.Suppose Γ ⊢SaRφ.First,we show that Th(S[R]) ⊆Th(SR).The only interesting case is that ψ is an axiom φ1(φ2···(φnψ)···)such that({φ1,...,φn},ψ)∈R.SinceSRadmits the deduction theorem,it suffices to show that φ1,...,φnψ,which is a direct application of the rule R.

For (iii),supposeS[R] ≤SR, Th(S)contains PC1 and PC2 and Γ,φψ.We prove by induction that Γφψ.SinceS[R] ≤SR,it suffices to show Γ ⊢S[R]φψ.The only interesting case is that ψ is obtained from φ1,...,φnby using the rule R.Then φ1(φ2···(φnψ)···)is an axiom ofS[R].Applying PC1,PC2 and modus ponens,it is easily shown that for any α,β,γ,

By inductive hypothesis,Γ ⊢S[R]φφifor 1 ≤i ≤n.Then by using n times of(*),PC2 and modus ponens,we obtain Γ ⊢S[R]φψ,as required.

Proof of Lemma 19

1. ⇒)By induction on the length of the formal derivation of φ from Γ in gtL.The only interesting case is that φ= □ψ is obtained from ψ by RN.By inductive hypothesis,□ωΓ ⊢ltLψ.It follows that □□ωΓ ⊢ltL□ψ.Noting that □□ωΓ ⊆□ωΓ,we have □ωΓ ⊢ltLφ.⇐)By induction on the length of the formal derivation of φ from □ωΓ in ltL.The only interesting case is that φ=□nψ for some ψ ∈Γ.Since RN is a local rule of gtL,we have ψ ⊢□nψ and hence Γ ⊢gtLφ.

2. ⇒)By induction on the length of the formal derivation of φ from Γ in lvL.The only interesting case is that φ= ψσis obtained from ψ by US.By inductive hypothesis,Γ*⊢ltLψ.It follows that(Γ*)σ⊢ltLψσ.Noting that(Γ*)σ⊆Γ*,we have Γ*⊢lbLφ.⇐)By induction on the length of the formal derivation of φ from Γ*in ltL.The only interesting case is that φ= ψσfor some ψ ∈Γ and substitution σ.Since US is a local rule of lvL,we have ψ ⊢lvLψσand hence Γ ⊢lvLφ.

3.The first two ‘iff’s are prove similarly as in (i)and (ii).The third ‘iff’ then follows from(i)or(ii).

Proof of Lemma 20.Since ltLandLhave the same set of axioms and rules,Th(ltL)=L.Now for ⊢ltL⊆⊢L,suppose Γ ⊢ltLφ.The only interesting case is φ ∈Γ.Since φφ is provable inL,we are done.

For ⊢L⊆⊢ltL,suppose Γ ⊢Lφ.Then there exists finite {φ1,...,φn} ⊆Γ such that φ1∧···∧φnφ ∈L.By the property of classical propositional logic,we have φ1(φ2···(φnφ)···) ∈L.Since Th(ltL)=L,we have⊢ltLφ1(φ2···(φnφ)···).By repeating applying the rule of modus ponens in ltL,it follows that Γ ⊢ltLφ.

Proof of Corollary 21.Immediate from Lemma 20,since for any normal modal logicL,Γ ⊢Lφ implies □Γ ⊢L□φ.

Proof of Lemma 23.⇒)Suppose □ωΓ ⊭ltFφ.Then there exist a frameFinF,a valuation V onF,and a world w inFsuch thatF,V,w ⊩lt□ωΓ butF,V,w ⊮ltφ.Let(F′,V′)be the submodel of(F,V)generated by w.ThenF′,V′,w ⊩lt□ωΓ andF′,V′,w ⊮ltφ.From the former,it follows thatF′,V′⊩gtΓ,since all worlds inF′are either w or accessible from w in finite steps.From the latter,it follows thatF′,V′⊮gtφ.SinceFis closed under subframes,F′is also inF.Thus,Γ ⊭gtFφ.

⇐)Suppose Γ ⊭gtFφ.Then there exist a frameFinFand a valuation V onFsuch thatF,V ⊩gtΓ butF,V ⊮gtφ.From the latter,it follows that there exists a world w inFsuch thatF,V,w ⊮ltφ.From the former,it follows that every ψ ∈Γ is true at all worlds inF.Thereby,it can be easily verified by induction on n that □nψ is true at all worlds inFfor all ψ ∈Γ and n ∈N.In particular,F,V,w ⊩lt□ωΓ.Hence,□ωΓ ⊭ltFφ.

Proof of Theorem 24.Suppose ⊢ltL=⊨ltF.For soundness,it suffices to show that the new local rule RN in gtLpreserves the semantic value ⊩gtof gtF,i.e.,for any modelMbased on any frame inF,for any φ ∈L□,ifM⊩gtφ thenM⊩gt□φ,which is straightforward.

For completeness,suppose Γ ⊨gtFφ.By Lemma 23, □ωΓ ⊨ltFφ.Since ⊢ltL=⊨ltF,it follows that □ωΓ ⊢ltLφ.By Proposition 19(i),we have Γ ⊢gtLφ,as required.

Proof of Proposition 3.First,we show ⊢gtS5Suppose Γ ⊢gtS5φ.Then we have □ωΓ ⊢ltS5φ.By Lemma 20,we have □ωΓ ⊢S5φ.By the proof property of normal modal logic,□□ωΓ ⊢S5□φ.Note that inS5for all n ≥1,□nφ is equivalent to □φ.It follows that □Γ ⊢S5□φ.

The two inequalities are obvious,since they have different sets of theorems.

Proof of Proposition 25.⇒)It suffices to show that if φ ∈Th(gtKΣ)then Σ ⊢gtKφ.By induction on the length of the formal proof of φ.If φ ∈AxgtKΣ,then either φ ∈AxgtKor φ ∈Σ.In either case,we have Σ ⊢gtKφ.If φ is obtained by MP or RN,then it can be easily verified by inductive hypothesis that Σ ⊢gtKφ,since MP and RN are local rules of gtK.If φ= ψσis obtained from ψ by US,then by inductive hypothesis,Σ ⊢gtKψ.It can be easily by induction that Σσ⊢gtKψσ.Since Σ is substitution closed,Σσ=Σ.Thus,Σ ⊢gtKφ.

⇐)By induction on the length of the formal derivation of φ from Γ ∪Σ in gtK.The only interesting case is that φ ∈Σ.But since gtKΣ has Σ as axioms,obviously Γ ⊢gtKΣφ.

Proof of Lemma 26.For(i),we prove by induction on φ.If φ=p is an atom,then

The other cases are immediate by inductive hypothesis.

For (ii),supposeGL,VL,w ⊮lvφ.Then there exists an admissible valuation V forGLsuch thatGL,V,w ⊩lt¬φ.By (i),it follows thatGL,VL,w ⊩lt(¬φ)δ.Hence,GL,VL,w ⊮ltφ*.

For(iii),noting that for any u inGL,L⊆u,we haveGL,VL,u ⊩ltLby the truth lemma.By(ii),it follows thatGL,u ⊩lvL,asLis closed under substitution.Since u is arbitrary,we haveGL⊩gvL.

Proof of Theorem 27.For soundness,it suffices to show that the new local rule US of lvLpreserves the semantic value ⊩lvof lvG(L),i.e.,for any general frameG∈G(L)and any w inf,for any φ ∈L□and any substitution σ in L□,ifG,w ⊩lvφ thenG,w ⊩lvφσ.We prove the contrapositive.SupposeG,w ⊮lvφσ.Then there exists an admissible valuation V forGsuch thatG,V,w ⊮ltφσ.Define V′such that for all atoms p, V′(p)=〚σ(p)〛G,V.Note that V′is also admissible forG.It can be shown by induction on φ thatG,V,w ⊩ltφσiff G,V′,w ⊩ltφ.Hence,G,V′,w ⊮ltφ,which implies thatG,w ⊮lvφ,as required.

For completeness,suppose Γ ⊬lvLφ.By Proposition 19(ii),Γ*⊬ltLφ.Then Γ*∪{¬φ} isL-consistent.By Lindenbaum’s Lemma,it can be extended a maximalL-consistent set Γ+.By the truth lemma,GL,VL,Γ+⊩ltΓ*∪{¬φ}.ThusGL,VL,Γ+⊩Γ*andGL,VL,Γ+⊮ltφ.By the latter,GL,Γ+⊮lvφ.By the former and Lemma 26(ii),GL,Γ+⊩lvΓ.By Lemma 26(iii),GL∈G(L).Hence,Γ ⊭lvG(L)φ,as required.

Proof of Theorem 29.For soundness,it suffices to show that the new local rules RN and US of gvLpreserve the semantic value ⊩gvof lvf.Since RN preserves ⊩gt,it also preserves ⊩gv.Since US preserves ⊩lv,it also preserves ⊩gv.

For completeness,suppose Γ ⊬lvLφ.By Proposition 19(iii), □ωΓ*⊬ltLφ.Following the proof of Theorem 27,we haveGL,Γ+⊩lv□ωΓ andGL,Γ+⊮lvφ,and henceGL⊮gvφ,where Γ+is the maximalL-consistent set containing □ωΓ*∪{¬φ}.Letbe the general subframe ofGLby Γ+.It follows fromGL,Γ+⊩lv□ωΓ that⊩gtΓ.By Lemma 26(iii),we also have⊩Land thus∈f.Hence,Γ ⊭gvG(L)φ,as required.