Consistency and Completeness of OMEGA, a Logic for Knowledge Representation

I Introduction

Omega is a description system developed for knowledge representation and reasoning [10). Omega is a calculus of descriptions rather then a calculus of predicates as ordinary logic. The concept ol description in logic, and in particular of delinite descriptions, can be traced back to the works by Frege and by Russell [15). Logicians have always been bothered by the semantic problema raised by definite descriptions when none or more then one individual meets the description. Therefore they have favored their elimination by showing how descriptions caA be contextually replaced by means of other constructs [16).

In Omega we deal with indefinite descriptions such as the description "(a Man)" . Omega then, has more the flavor of a naive set theory. Omega however allows many ways to build new objects, rather than the single set formation construct of set theory. Omega is a type free s~-stem , in the sense that a single logical type is admitted, the type of descriptions. With Omega we achieve the goal of an intuitively sound and consistent theory of classes which permits unrestricted abstraction within a powerful logic system. Description abstraction is a construct provided in Omega similar to set abstraction. Abstractions add considerable expressive power to a language, nevertheless such powerful constructs are likely to lead to inconsistencies or paradoxes. The rules for abstraction we present have been studied to avoid those problems. The proof of consistency that is provided in the paper is therefore significant to establish this claim.

The main goal of this paper is to present the logic theory Omega, to introduce its models, derive an axiomatization and finally to show the consistency and completeness of the system.

We consider the study of a knowledge representation system as a logic system to be of fundamental importance. In this way we isolate the basic deductive mechanisms from the intricacies of specific programming lslituto di Scienze dell'lnfurmqzione Corso ltalia 40 1-56100 Pi sa, Italy languages or implernentations. The fundamental results obtained in this way can help us understand the basic mechanisms of reasoning on a knowledge base, and insure us of the soundness of the system.

This research was supported in part through a grantlromOiivelli to the Ar1WiCiattnteHigence Laboratory of MIT.

The second author has been SUWO<ted in part by a fellowship ol the Consiglio Nazlonele delle Rieerche.

As an alternative to symbolic logic, many knowledge representation systems use semantic networks [14) as their basic formalism. The term "semantic" in the name "semantic network" refers to the fact that the formalism was originally developed to represent the semantic information necessary to understand natural language. Despite their name, the semantics of semantics network has never been satisfactorily developed. In the work by Brachman (4), the ambiguities and inadequacies of semantics networks are investigated. A typical problem deals with the meaning and use of inheritance links.

In most cases the semantics of semantic networks is determined by the way the processing routines of application programs manipulate the information represented by nodes and links of the network. Many authors consider semantic networks as embedded into first order predicate calculus [9, 18), so the reasoning mechanisms are directly drawn from predicate logic. Semantic networks can then be considered a convenient notation (i.e. an alternative syntax) for expressing variable-free assertions of predicate calculus. The notation is convenient because it suggests an organization of the data base of assertions, highly suitable for mechanical manipulation. Kowalski in (7) adopts this point of view, and also proposes an extension to the notation of semantic networks in order to express a more general class of formulas, including universally quantified variables. The class he suggests is the class of Horn clauses, i.e. formulas of the kind:

where all A; are positive atomic formulas. For this class of formulas a uniform proof procedure based on resolution performs reasonably well. However the expressive power is still limited, mostly because of the restriction in the use of negation.

By drawing such connections between semantic networks and predicate logic, one can argue that a semantics has been provided for semantic networks. However, many of the fundamental aspects of semantic networks, such as inheritance, remain unexplained.

Other knowledge representation systems provide deductive mechanisms of their own, most often procedurally defined [8), [3), [5), [19) . Such deductive mechanisms are not formally investigated, so their logical soundness can be questioned. It is in fact the case that some of these systems perform unwanted or incorrect deductions. An example of this kind of problems is the so-called "copy confusion" effect reported by Fahlman about his NETLsystem.

In comparison with other knowledge representation systems, Omega has increased expressive power deriving from including:

• variables : this allows description of complex general relations. rather then isolated assertions;

· quantification: both over individuals and classes (descriptions);

• negation: this removes the major limitation of systems like PROLOG. based on the use of Horn clauses;
• abstraction : allows description of classes of individuals in terms of their properties. It is a very powerful construct, which allows for instance to define the concept of converse of a relation, that had to be given as primitive in [10).

We believe that recent proposals of parallel problem solving systems such as Ether [12] will be suitable for implementing the reasoning mechanisms demanded by a rich system such as Omega. For instance the ability to process concurrently proponents and opponents [12) of a same goal , is what is needed to appropriately deal with sentences containing negations. Conversely, it is the provision of negative facts what makes the proponents/opponents metaphor profitable and effective. So far the limitations on the use of negation seem to have been dictated mainly by considerations related to sequential proof algorithms.

In this paper we present and develop the description system Omega, as a logic system. The system we develop has some similarities with the one pre--...ented by R. Martin in [13), even though we started with different aims and motivations. Martin's system is proposed as a system of mathematical foundation, as an alternative to the classical theory of sets. However no result of completeness or consistency for that logic is presented.

A sound logical theory for Omega is necessary as a formal concise specification for the algorithms that will carry out the reasoning process. Results such as· the correctness or the completeness of such algorithms can be established only with respect to the theory. Properties and theorems about the theory can be exploited in the design of the proof procedure, as it was the case for the resolution algorithm in First Order Predicate Logic.

We are leavinq out from the present discussion other features of Omega such as the calculus of attributions and of metadescriptions.

A version of Omega has been implemented on the MIT LISP machine by the authors and has been used to describe the base of active knowledge supporting an experimental system of office forms [1]. A second ·implementation of Omega is currently under development by Jerry Barber. A subset of Omega is being used to describe two dimensional objects within the SBA system by Peter de Jong [6).

Our experience has proven that the axiomatization provides an extremely useful guideline in the process of implementation.

II Descriptions and Predications

This section is intended as an informal introduction to the theory Omega. For more exhaustive presentation and examples we refer to [10).

The simplest kind of description is the individual description, like: Boston

or

Paul

Here the names Boston and Paul are names describing individual entities.

An instance description is a way to describe a collection of individuals. Forinstance

(a Man)

represents the collection of individuals in the class of men.

The most elementary sentence in Omega is a predication. A predication relates a subject to a predicate by the relation is. For instance the predication

Paul is (a Man)

• is meant to assert that the individual named Paul belongs to the class of

men. Predication can be used to relate arbitrary descriptions. For instance the sentence:

(a Man) is (a Mortal)

states the fact that any individual of class man is also an individual of class mortal. A fundamental property of the relation is is transitivity, that allows for instance to conclude that

Socrates is (a Mortal)

from Soc rates is (a Man) and (a Man) is (a Mortal)

The description operators and, or and not allow us to build more complex descriptions, like in the following example:

(a Boolean) is (true or false)

More complex statements can be built by combining statements with the logical connectives A, V, ...., and =>, as in:

Note the difference between description operators and statement connectives in the following examples:

(true A false) is false (true and false) Is Nothing

where Nothing is our notation for " the null entity".

Ill Syntax

The language of the theory Omega is presented hero using the kind of notation which has become standard in logic and denotational semantics. We list first the syntactic categories of the language. For each of them we show our choice of metavariables ranging on the elements of that category, that we will use in the rest of the exposition.

1:	individual constants (1, 11, 12, 13 ... ), including the constants true and false
V:	variables(v, v1, v2, v 3 .. . )
C:	class constants (c, c1, c 2 , c 3 . ••• )
S:	statements (a, a1, a 2 , a 3 ... )
&.	descriptions (6, 6 1 , 6 2 , 6 3 .•• )

Descriptions and statements are built from constants and variables according to the following syntax:

Descriptions	Statements
I, Nothing, Something	true, false
v	v
(a c)	(8 1 is 6 2 )
(Any v such that a)	Vv.a
(81 or8 2 )	(a1 Va2)
(61 and8 2 )	(a1 A a2)
(not 8l	(--.a)
a	(a1 => a 2 )

Nothing and Something are two special constants.

IV Semantics

We have followed in this work the method of defining validity in a semantic way. First we characterize a class of models for Omega and define the notion of truth in a model. This gives an intuitive and immediate semantic interpretation for our theory. Then we look for an axiomatization for valid formulas of the theory. The models defined earlier are useful in this stage for providing a guideline and a criterion for the suitability of the axiomatization.

By proving the completeness theorem, we show that the axiomatization is adequate. Furthermore the completeness result tells that our theory is consistent if and only if it has a model. Therefore the existence of models presented in this section implies the consistency of Omega.

The structure of the interpretation is

where D is the domain of interpretation, a nonempty aet of individuals, ' is a mapping from individual constants into elements of D

and e is a mapping from class constants into subsets of D

A. Definition of Value of a Description

The value of a description can be defined as a mapping from descriptions and environments into subsets of D.

An environment defines an association between variables and subsets of D.

E:V-+t>

1. Value of constant descrlptlona:

The interpretation of the description abstraction Any is the aet of individuals which, substituted for v in the statement a, make the statement true. The notation

means that the statement o in the environment p is true relative to the structure ..t, and it is completely defined in the next section.

B. Definition of Truth Value

The truth of a statement relative to a structure ..( is defined as:

Definition 1: (Truth) I=..( olff V p F: ..( 8oDP

Given the definition of truth, validity is defined as follows:

Definition 2: (Validity) F: olff V M I=M o

V Axiomatlzatlon

The method that we followed in deriving the axiomatization, is besed on noting rules that preserve validity of formulae and making them into axioms or inference rules.

A. Axiom Schemata

We present the axioms of the system in the form of natural deduction inference rules [11). As a matter of notation we will use a double bar to indicate that a rule can be applied in both directions. The bar is omitted if the set of premises is empty.

Axioms for Statement·

51:

true

$2:

53:

..., fatae

o ~true

54:

55:

56:

57:

58:

59:

510:

$11:

512:

,.,,.~ (7

true~ t1 V ..., t1

o A ..., a ~ fatae

a 1 ~ a 2 , a 1 ~ a 8

at~ <7z A as

<7t ~ a3, tlz ~as

a1 V a2 ~as

a 1 ~ ·a 2

...,a2 ~ ...,a1

a~ ..., (...,a)

..., (...,a)~ a

a ~ a Ia true

513:

..,a~ ula fatae Note that this axiom set is not minimal, since lor instance S1·S2, S3· S4 arid.SS·S6 are pairwise derivable from one another. (A similar remark applies to the axioms lor descriptions presented below).

'p[x/v) Is the ume environment a& p but lor variable · to which n 8180Cietea x.

The notion of "sameness" between descriptions is defined as follows:

Definition 3: (Sameness)

We will also need the following abbreviation:

Definition 4 : {Individuality) lndlvldual(c5] stands for -.(8 is Nothing) 1\ 't:J v . (v Is 8) ~ (8 is v) V (v Is Nothing)

Axioms tor Description·

D1:	81 is 62 = 't:J v. lndlvldual[v] 1\ vIs 61 ~vIs 8 2
D2: lndlvldual(l)	The ordinary rule of Modus Ponens can be derived from transitivity
D3: 8 Is Something	by letting a 1 be true.
D4: Nolhlngls8	Standard rules can be used lor ~ introduction, 't:J introduction
D5: Something Is (6 or (not8))	(generalization) and 't:J elimination (instantiation).
06: (8 and (not 8)) Is Nothing 81 Is 82, 81 Is 8 3	The rules lor description abstraction require more careful
	examination. The most obvious formulation of the abstraction rule lor descriptions would be:
D7: 8 1 is (8 2 and 8 3 ) 81 Is 83, 82 /s 83	a[c5]	A1
08: (81 or6 2 ) Is 8 3	8 Is (Any v such that a[v)}
	and the corresponding concretion rule:
09: 81 /a 82 not 82 Is not 81	8 is (Any v such that a[v)) a[ c5]	C1
010: 011: not (not 8) Is 8 8 Is not (not 8)	Unfortunately, these unrestricted forms lor the	abstraction and

• 4 . (6 1 end 6 2 ) same (Any v such I hal (v is 6 1 ) 1\ (v is 6 2 ))

5. (not 8) same (Any v such thai ..., (v Is 6))

Actually these statements could have as well been given as an alternative axiomatization lor description operators. We prefer however the set of axioms presented above since they do not involve explicitly description abstraction. The inference rules lor description abstraction are rather complicated. With the axioms we have chosen, the use of abstraction rules and extentionality (axiom 01) can often be avoided.

B. Inference Rulea

It is easy to verily that these two transitivity rules preserve the truth according to our interpretation:

Unfortunately, these unrestricted forms lor the abstraction and concretion rules lead to contradiction. Consider lor example

John Is (e Man)

With (a Man) lor 8, by A 1, we get:

(e Man) Is (Any v such that (John Is v))

but if also Paul is (e Man)

then by transitivity:

Paul Ia (Any v such that (John Is v))

and byC1 :

(John Is Paul)

which might not be true.

A restricted form of the abstraction principle that avoids such problems is the following:

Similar problems arise with an unrestricted concretion rule. Let a[v] · lndividual(v] and suppose lor instance:

lndlvlduai(John]

lndlvlduai(Paul)

The notion of individual, as it is formally defihed, corresponds in our interpretation to the set consisting of a single element, or singleton. Axiom D1 then corresponds to the following version of the axiom of extentionality for aets:

Axiom D2 states the fact that individual constants are individuall.

We have chosen this set of axioms so that there is an almost complete symmetry between the axioms for statements and the axiome for descriptions. In this way any theorem abou1 descriptions has a corresponding dual theorem about statements. A single proof procedure will work for both desCriptions and statements.

There is another strong correspondence between statements and descriptions, which is expressed in the following

Lemma5:

1. Nothing same {Any v such that false)
2. Something same (Anyv such that true)
3. (6 1 or 6 2 ) seme(Anyv such thet(v Is 81) V (vIs Bz»

then by A2

John is (Any v such that lndlvldual(v]) Paul is (Any v such that lndlvldual(v])

From the axiom 06, which introduces the or description, we get:

(John or Paul) is (Any v such that lndivldual(v]l and from this and C1:

lndlvlduai(John or Paul)

We solve this problem by restricting C1 analogously to what we did for A 1:

With this restriction to individuals, it is easy to verify that the abstraction and concretion rules are sound.

Note that with this form of the concretion principle Rusaell's paradox is avoided. Suppose we call z the following description:

11 we allow C1, since z is z is true by reflexivity of is, we would derive the paradoxical consequence:

..,(z is z)

We can show however that:

z same Nothing

because

(Any v such thai .., (v is v)) same (Any v such thst false) ·same Nothing

Therefore rule C2 cannot be applied because Nothing is not an individual.

The complete set of inference rules is summarized in the following table.

Inference Rules

Statements	Descriptions
	81 is 82, 82 is 83 81 is 83
(J	17[8] 1\ Individual[&)
v v. 17 provided vis not free in any assumption on which a depends V v. u[v)	8 is (Any v such that u[v]l
17[8]	Sis (Any v such thai 17[v]l 1\ lndlvlduai(S) u[S]

As it can be seen from the formulation of the rules of abstraction

VI Soundness and Completeness

The first result to be proved about the axiomatization is its soundness:

Theorem 6: (Soundness)

For every closed statement A, f 1- A => f I= A

We are using the notation r 1- A as an abbreviation for:

The derivability relation 1- is defined in a standard way, so that f 1- 17 means that the statement a can be derived from the statements in r and from the axioms by applying the rules of inference.

The soundness theorem states that whenever a statement can be derived from the set of premises r then it is true in every model that satisfies the statements in f. We omit here the proof since the argumentation is straightforward.

We next turn to prove the completeness theorem for the theory presented above.

The completeness theorem gives us a measure of the adequacy of our axiornatization. In fact it asserts that the set of valid formulas coincides with the set of theorems 91 our theory. So it provides a bridge between what is established as semantically valid, and what is established by symbolic manipulations.

More important, this result is the fundamental step in showing the consistency of our formal theory.

The completeness theorem can be formulated as follows:

Theorem 7: (Completeness)

For every closed statement A, f I= A <=> f 1- A

Proof: We follow a Goedei·Henkin argument [17] . The implication f 1- A => f I= A corresponds to the soundness theorem. The other direction of the implication is equivalent to saying:

If A cannot be derived from f then there exists a model that satisfies f but not A. So we can prove the result by building a model .A\,, possibly in dependence from A, such that:

In order to do that, for any given closed formula A, we build a complete Henkin extension of theory f, called f A· having the following additional properties:

Since fA is a complete Henkin extension of f, it also satisfies the following properties:

fA iS built as the limit Of an induCtive sequence Of theories, starting from r. For the details of the construction we refer to [2).

Next we prove the following lemma in order to prove that fA has a model:

The proof is outlined in the next section. Let .A\, be such a model for fA. Assuming now that f If- A, it follows that fA If- A and then f A II= .A\, A

Since a model of r A is also a model of r. we have proved that:

and the completeness theorem.

A. Proof of Main Lemma

We will prove the lemma by building a model .A\, such that:

.A\, will be a term model built out of syntactic material. More precisely equivalence classes of individual descriptions will be the elements of the domain of interpretation. Let us define the equivalence relation - as:

We will denote as 181 the equivalence class of 8 according to-.

We will call lnd = (8 E A I r 1- Individual[&]}. The domain of interpretation is the quotient ol the set lnd with respect to the relation - .

The model .A\, is defined as: .A\, · <lnd/-, 3, C> where

This model has the following significant property:

This property establishes the connection between the semantics (value of descriptions) and the syntax (derivability of predications). Because Omega allows statements as special cases of descriptions, this property is all is needed to establish the main lemma, as the following result shows:

Proof: Assume first that rA 1- a. By axiom S12, it is also fA 1- (o is true). Using this fact and transitivity in the premise of the lemma, we have

But by the definition off:

On the other hand, if we assume that r A I= .A\, a then

This means that r A 1- (true is o). Since r A is complete, then either fA 1- o or fA 1- -, a. But the latter case is impossible because, by applying axiom S13, we would get r A 1- (o is false), and by transitivity r A 1- (true is false), which contradicts the consistency assumption lor rA.

Proof: The proof is done by induction on the structure of descriptions. We give the flavor of the proal presenting a few of the cases.

1. 8::1.

since I E lnd by axiom 02. Note that this case takes care also of the individual constants true and false.

2. 8 = (81 or 82).

rna, or &2D = rna,) u fU82D ..

{by induction hypothesis)

{18118 E lnd and rA 1- (81s 8 1 )} U {18118 E lnd and rA 1- (81s 82)} .. {18118 E lnd and rA 1- (8/s 8,> or rA 1- (6 is 62)} = (by prop. 2) {18118 E lnd and rA 1- (6/s 81) V (81s 82)} = (by Lemma 5.6) {16118 E lnd and rA 1- (8 is (8, Or~))}

3. a = (81 Is 62).

rna,)~ ttY {18118 E lnd and rA 1- (81s 8 1 )}!;;	{Assumption)
{18118 E lnd and r A 1- (61s 82)}	(by ind. hyp.)
8 E lnd and r A 1- 8' Is a, = r A 1- 8' Is 82 rA 1- 81 1s~ rA 1- (6,1s82) Is true {18118 E lnd and rA 1- (81s (81 Is 62))} ~ 081 I E	(by axiom 01)
	{by axiom S12)
8 lnd and r A 1- (8 Is true)} {18118 E lnd and rA 1- (6/s true)} = {llruel}	.. (by transitivity)
rn 8, Is 82)	(by definition of " ·

rn 8, Is 82) (by definition of " · The proof is similar under the hypothesis that: -,rna,) ~ f(&J

rA I= .A\, a, or rA I= .AI. a2 rAI-a,orrAI-a2 rA 1- (a, v a2) fA 1- (a, V 02) Is true (Assumption) (by ind. hyp. and lemma 9) {by property 3 of r,.) {by axiom S12) {18118 E lnd and r A 1- (81s (a, v a2))} ~ {1.511 8 E lnd and r A 1- (8 Is true)} (by transitivity) (18118 E lnd and rA 1- (8/s true)} = {ltruel) ,. rna, v a2) (by definition of,

The proof is similar under the hypothesis that r A Jib .A\, a 1 and rA !Ito A, a2

Once lemma 10 has been established we can prove the main lemma. In fact from lemma 9 we can deduce the following:

The main lemma follows from this and lemma 10.

VII Consistency

The consistency of Omega can be established by means of the following result:

Theorem 11 : If an Omega theory r has a model, then it is consistent.

Proof: Suppose r has a model M. Then r li=M false. From the Completeness result it follOWS that r lf-M false whiCh proves the consistency of r .

VIII Omega and other Formal Logic Theories

Omega is not a First Order Predicate Logic, since it includes a variable binding operator, namely the Any construct, which is not present nor expressible in First Order Predicate Logic. In this sense Omega is more similar to set theory, which includes set abstraction, besides universal and existential quantifiers.

The version of Omega presented here is a first order theory. We are investigating extending the axiomatization to higher orders. In [10] we presented examples of the use of higher order capabilities.

Omega is a Set Theory. However Omega relies on constructors for building new descriptions. In set theory, pairs for instance are built by means of set formation alone. In Omega a Pair constructor can be used to describe pairs of objects. A Pair of two individuals will be an individual itself, therefore separating the inheritance relationship from the component relationship. Omega is a constructive set theory and has no axiom corresponding to the powerset axiom of classical set theory. The constructive nature of Omega implies that it is poSSible to usa the proof of a statement to determine a description ·which meets some requirements or is the answer to a question.

IX Conclusion

The results of this paper provide us with a solid base on which to build a theory of knowledge representation.

The system presented is powerful enough to express arithmetic, by following the construction of [13). The use of attributions as in [10) however increases the naturalness of the notation. There are a number of problems regarding attributions to be addressed such as: interaction between attributions, merging and inheritance; functional dependencies between attributions; contrasting uses of attributions (lor instance attributions have been used to expre"..s part/whole relationships as well as to express n-ary relations). In [10) a preliminary set ol axioms lor attributions was presented. A set theoretical model along the lines ol the present work has to be defined in order to obtain a satisfactory lull axiomatization ol attributions. Such axiomatization will appear in a forthcoming paper [2).

Another important construct allowed in Omega is the A-abstraction. The axiomatization lor this construct is similar to the axiomatization of the ><·calculus. This construct interacts nicely with the inheritance mechanism of Omega, allowing the same notation to be used for describing the type of a function as well as lor defining ita values.

We have also investigated the problems arising from allowing sell· reference in the language. In order to avoid logical paradoxes like the liar paradox. it is necessary to give up the rules ol excluded middle (axiom S5) and contradiction (axiom 56). This allows models where the value of a sentence can be neither true nor false. Such solution follows the lines ol the one suggested by Visser in [20) . The logic can still be proved to be complete, but the proofs by hypothetical reasoning become more cumbersome.

Acknowledgments

Carl Hewitt has been the leading force behind the developement of Omega and its axiomatization. Luca Cardelli and Giuseppe Longo have thoroughly discussed our ideas in the early stages ol this work. William Clinger has provided constructive criticism and encouragement. We had several suggestions from Jerry Barber, who is involved in implementing Omega, about the basic rules ol deduction.