A Note on Deduction Rules with Negative Premises

Ivan Kramosil Institute of Information Theory and Automation Czechoslovak Academy of Sciences Prague,Czechoslovakia

The so called frame Axioms problem or frame problem is well-known to anybody who is interested in automatic problem solving.Some information concerning this problem can be found in (1) or (2).In (2) the author proposes to eliminate the frame axioms in such e way that they are replaced by e new deduction rule denoted as UNLESS-operator.In fact,this operator is a rule enabling to derive that some­ thing concerning the environment is va­ lid at the present situation supposin~ it was valid in a past situation and 1t is not provable that a change concerning the validity of this statement has occur­ ed.For our reasons oply the formally lo­ gical aspect of this solution is intere­ sting as it leads immediately to a new and very interesting modification of the notion of formalized theory.

The aspect just mentioned consists in in the fact that in (2) the PUthor for­ malizes his UNL~SS-operator in the fol­ lowing form of a deduction rule: If a formula A is deducible and a formula B is not deducible 1 then a formula C is de­ ducible.Written 1n symbols

where, of course, "JlS21" and " 1- " are sym­ bols of an appropriate metatheory,not the investi~ated theory itself.

The use of a deduction rule of this type may involve some doubts whether we are justified to do so.The first objecti­ on arises from the fact that any deducti­ on rule,including those of the type (1), is an integral part of the definition of the notion "deducible formula",so this notion itself,neither in its negative form "not 1- B',is not allowed to occur in a dec1uction rule.It is a matter of fact that in "usual" formalized theories the deduction rules are also written in the fo rm using the symbol .,_ , e.g.

if the modus ponens rule is considered. However,it is a well-known fact that in this case the symbol 1-- can be elimina­ ted so that the definition of the notion "provable formula" should be correct.It is the goal of this paper to investigate the deduction rules of the type (1) in order to ·see,wheher a set of deduction rules,containing at least one rule of the type (1) and considered together with a recursive set of axioms defines unambiguously and correctly a set of de­ ducible formules.The second objection concerning the deduction rules of the type (1) arises from the fact that when a proof is constructed we have at our disposal in every step only a finite number of formulas proved already to be theorems,so we are never justified to apply a rule of the type (l).First of all,we shall investigate the first obje­ ction leaving the other one till the end of this paper.

Consider a formalized language 1 based on the first-order predicate calculus (FOPC).Let Ax be a set of axioms.This set is supposed-ro be recursive and,without any loss of generality,it may be also supposed to be finite end its elements to be closed formulas (i.e.not contain­ ing free indeterminates).

Moreover,consider a finite set of de­ duction rules.Deduction rule (generaliz­ ed :or purposes of this paper) is a me­ talanguage scheme

where B is a formula and every A. is either ... Ai or not r Ai tAi cL.Cfearly, ()) includes (l;-8nd (ZJ as special cases.Let us divide the deduction rules into two sets,R and §.

R contains the deduction rules in which every !i is of the form ~ Ai, i.e.

the "usual" deduction rules.Suppose,in the rest of this paper,that R contains all the deduction rules usual in the first-order theories (and,maybe,some other deduction rules der1ved from them).

S contains the deduction rules in which at least one A. is of the form L__ -1 !lQ.l r- Ai ·

Let us suppose,for a moment,that the set § is empty.In such a case the previous description coincides with the usual defi­ nition of formalized theories based on the FOPC.The set of provable formulas (theorems) is then defined as the smal­ lest set of formulas containing the set Ax and closed with respect to the dedu­ ction rules.To make this formulation precise the following pattern must be used.

Let P be the system o~ subsets o~ the set ~having the ~ollowing properties

1. i~ XeEo,then ~ e X,
2. let A 1 ,A 2 , ··· ,An be ~ormulas to which a deduction rule

~rom H is applicable,then A 1 ex,A 2 ex, ··· ,AneX implies BeX,

1. Eo contains all the sets satis~ying the conditions a) 8nd b).

Then the intersection

also setis~ies a) and b) end the set o~ theorems,denoted here by Cn(Ax/S),is de­ ~ined

Notice that the ~act that 0 fo e fo is the basic point assuring the correctness of the de~inition o~ £n(Ax/g).

Now,suppose that £ is not empty.De~i­ ne the system E o~ subsets of 1 as ~ol­ lows:

1. i~ Xe~, then Ax c X,
2. if Xe~, A 1 eX,A 2 ex, ··· ,AneX and the deduction rule (4) is applicable to the formulas A 1 ,A 2 , BeX. ,An' then
3. if Xef,i~ a rule o~ the type (3) is in £ and is applicable to ~ormulas A 1 ,A 2 , ··· ,An and i~ Ai e X in case when A 1 . is ~ A 1 . and A. e L - X in - 1 - case when !i is DQl ~Ai, then BeX,
4. P contains all the subsets o~ L satis~ying a),b) and c). -

It can be easily shown,now,that the qua~ruple <1,Ax,g,s > de~ines a ~or­ mal1zed theory i? an<! only i~ ()~ e ~·

In usual logical theories,where only the rules o~ the type (4) occur,all the deduction rules possess a property which is usually called the truth-preserving property.This property consists in the ~ollowing fact: i~ a rule o~ the type (4) is applicable to ~ormulas A 1 ,A 2 , ··· An

·and if these formulas are true in a model, then also B is true in this model.In ot­ her words the truth-preserving deduction rules do not lead outside the set o~ true ~ormulas.This property seems to be quite natura\and necessary for any deduction rule i~ the formalized theory is expected to have a relation to the real world,re­ presented by a model.In other case the formalized theory becomes just a pure play with ~ormulas.It is why we try to generalize this notion also for the de­ duction rules of a more general type,na­ mely (3).

A rule o~ the type (3) possesses the truth-value-translating property i~ ~or ~very n-tuple A 1 ,A 2 , ··· ,An o~ ~ormulas to which this rule is applicable the ~ollowing is valid : Supposing M is any model such that i~ !i is r Ai 7then Ai is true in !4 and i~ !i is JlQ.l r Ai, ~hen Ai is not true in !, them B is true 1n !·

Theorem 1. Let L,Ax,R,S 1 P ,P and £n (Ax/R) have the simemean1lii as above and let all deduction rules ~rom R U S possess the truth-value-translating pro­ perty.I~ the set Cn(Ax/R) is closed with respect to every deduction rule ~rom £, then

otherwise

Proo~. Clearly, 1 e f and i~ X e ~' then Cn(Ax/R) c X.Denote by A 0 the con­ junctiOn-of-all formulas ~rom !! .Con­ sider a ~ormula yc1 such that

where , y stands ~or the negation o~ y.

The ~act that , y e 1 - .Qn(Ax/S) means that A ~ , y is not a theorem of the FOPC. 0 A well-known theorem of ma­ thematical lo$ic states that this calcu­ lus is sement1celly complete.This yields that a formula is a theorem of the FOPC if and only i~ it is true in all modele. Hence,there exists a model in which A :::> , y is not true, so in this model, dinote it M (y), the ~ormula , (A :> , y) is true.The set Tr(M(y)) o~ al~ the ~or­ mules ~rom L whiCh are true in the model M(y) is closed with respect to the usual <!eduction rules of the propositional and first-order calculi.The equivalence

is a propositional tautologytso the ~act that ,(A 0 :> , y) e I,!:(_M(y) J implies that also A 0 &y and y itsel~ belong to Tr(M(y)).As the set Tr(M(y)) is a set o~ ?Ormulas true in a mO<Jei,no pair o~ con­ tradictory ~ormulae may occur in this set,so , y e 1- ~(!(y)).

It is a well-known fact that all the deduction rules in FOPC preserve the truth,i.e. if the premises are true in a model the same holds for the conclusions. However,the truth-value-translating pro­ perty assures that Tr(M(y)) is closed al­ so with respect to deduction rules from S.This fact should be immediately clear 7rom the definition,let us prove it for the rule (1).

Let the rule (1) be applicable to formulas A,B c L, let A e ~(M(y)), let B e L - Tr[M(y)T.Then,according to the truth-va!Ue=preserving property,C is also true in the model M(y),so C e Tr(M(y)). The way of generalizing this result to any rule from § is ~uite clear.

Hence,the set Tr(M(y)) c L 1 contains all the axioms from-Ax (since-1t contains A ) , contains y, does not contain ,y and ig closed with respect to all the deducti­ on rules from g u §.This gives that

and,immediately,we obtain

where

The set Cn (Ax/R) u B belongs to P if and only Tr ir-is close~ with respect to the rules from R u S.This is possible only if!! is empty~i.e7 only if

0 E = Cn(Ax/,R).

If this set is closed also with r espect ~o the rules from §,then it belongs toE, 1n all other cases tehe set (\ P does not belong to f.The theorem ia proved.

The r esult of this theorem is follo­ wing: the quadruple <1,,Ax,g,s > defines a formalized theory if and only if this theory is equivalent to that defined by the triple <1,[~25.tli> · In other words, the deduction rules from S,i.e.the rules with nei;r ti ve premises' are either useless or meaningless.This result agrees with our intuizive feeling that the rules of the type (1) are useless as we are never allowed to say that a formula is not de­ rivable having at our disposal only a fi­ nite number of formulas derived until no~ and not having at our disposal any meta­ theoretical assertions concerning the in­ vestigated theory as these assertions cannot be formalized and deduced before defining the notion of provabi lity.

In or der not to limit ourselves just to a criticism of the model suggested in (2) let us propose another way how to de­ fine a formalized theory using the deductive rules with negative premises.Re­ member that in usual formalized theories it is possible to define,first of all,the notion of formalized proof and then defi­ ne a formula to be theorem if and only if there exists a formalized proof proving this formula.Let us follow this pattern and define the set ~ of formalized proofs as follows,here x,y,A,B,etc.belong to 1·

1. If x e !!_,then <x > e ~·
2. Let < xl'x 2 , ··· ,xm) ~ ~,let y e A!_, then

1. Let (xl'x 2 , ··· ,~) e ~,consider a rule of the type (3) from .R u 2· If for any i ~ n such that !i is ~ Ai thP.re is a j ~ m such that Ai ~s xj and if,at the same time,for no i ~ n such that A; is not~ A. the -. - 1 formula Ai occurs in the sequence

1. ~is the smallest set satisfying a), b) and c).

Now,the set T of theorems can ~e de­ fined as follows!

Theorem 2. The definition of the set of theorems is logically correct.The set D of formalized proofs is recursive,the set I of theorems is recursively enumera­ ble.

Proof. Consider the intersection of all sets of. finite sequences of formulas satisfying a),b) and c).This intersection also satisfies a),b) and c),so Dis just this intersection and the definition of D is correct. For any finite sequence < xl'-

x 2 , · · · , xm ) of formulas we are able to decide,in an effective way,vthether it is a formalized proof or not,so the set D is recursive.The fact that the set I of theorems is recursively enumerable follows immediately .,from its defi':li tion and from the Kleene s Representat1on Theorem (see,e.g.,(3)).The theorem is proved.

It can be easily seen that this defi­ nition of deducibility does not capture the intention explained in (2),namely, there may be formulas in ! which should not be provable in the framework of.the model developed in (2).However,the 1nte­ ntions explained in (2) are not correct­ ly formalizable and we believe tha~ cer­ tain difference between the author s suggestion in (2) and our definition of the set T is a penalty the necessity of which follows from Theorem l.Certainly, it would be interesting to ask,whether Theorem 1 will be valid supposin~ the truth-value-preserving property 1s om­ mited or to ask for some more properties of the set T defined Above.However,both these ·uestions wo11ld be beyond the sco­ pe of the main probJem to which this paper has been devoted.

References:

• (l) P.J.Hayes: Frame problem and rela~ ted problems in artificial intelli­ gence. In: Artificial and Human Thinking (e<' itors A.Littlehorn and D.Jones),Elsevier 1973, pp.4559.
• E.Sandewall: An approach to the frame problem and its implementa­ tion. In: Machine Intelligence 7 (editors B.Meltzer and D.Michie), Edinburgh University Press, 1972, pp. 195 - 204.
• M.D8vis: Computability and unsolva­ bility. Me Graw- Hill Book Comp., New York - Toronto - London, 1958.