GFO Part I Basic Principles
  ontomed Theories Concepts Applications  

Onto-Med >> Theories >> GFO Part I Basic Principles


2.2 The Axiomatic Method

A formal theory is a set of formalized propositions. The axiomatic method comprises principles used for the development of formal knowledge bases and reasoning systems aiming at the foundation, systematization and formalization of a field of knowledge associated with a part or dimension of reality.

The axiomatic method deals with the specification of concepts, and is motivated by a number of considerations. On the one hand, a formal knowledge base contains primitive notions and axioms, on the other hand, it includes defined notions and definitions. Moreover, proofs show the logical validity of theorems. It would be ideal if one were able to explain explicitly the meaning of every notion, and then to justify each proposition using a proof. When trying to explain the meaning of a term, however, one necessarily uses other expressions, and in turn, must explain these expressions as well, and so on. The situation is quite analogous for the justification of a proposition asserted within a knowledge base, for in order to establish the validity of a statement, it is necessary to refer to other statements, which leads again to an infinite regress.

The axiomatic-deductive method contains the principles necessary to address this problem. If knowledge of a certain domain is to be assembled in a systematic way, one can distinguish, first of all, a certain small set of concepts in this field that seem to be understandable of themselves. We call the expressions in this set primitive or basic, and we employ them without formally explaining their meanings through explicit definitions. Examples for primitive concepts are identity and part.

At the same time we adopt the principle of not employing any other term taken from the field under consideration, unless its meaning has first been determined using the basic terms and expressions whose meanings have been previously explained. The sentence which determines the meaning of a term in this way is called an explicit definition.

How, then, can the basic notions be described; how can their meaning be characterized? Given the basic terms, we can construct more complex sentences that can be understood as descriptions of certain formal interrelations between them. Some of these statements are chosen as axioms; we accept them as true without establishing their validity by means of a proof. The truth of axioms of an empirical theory may be supported by experimental data. By accepting such sentences as axioms, we assert that the interrelations described are considered to be valid and at the same time we define the given notions in a certain sense implicitly, i.e., the meaning of the basic terms is to some extent captured and constrained by the axioms. On the other hand, we agree to accept any other statement as true only if we have succeeded in establishing its validity from the chosen axioms via admissible deductions. Statements established in this way are called proved statements or theorems.

Axiomatic theories should be studied with respect to meta-theoretical properties. It is important that the axioms of a foundational ontology are consistent, because domain-specific and generic axioms will be built on them. Other important meta-theoretical properties are completeness, and the classification of complete extensions. If several theories are considered, their interrelationships must be studied which will lead to questions regarding the interpretation of one theory in another, and identifying the more comprehensive or expressive theory.

Robert Hoehndorf 2006-10-18


deutsch   imise uni-leipzig ifi dep-of-formal-concepts