


Overview
General Formal Ontology (GFO)

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 axiomaticdeductive 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 metatheoretical
properties. It is important that the axioms of a foundational ontology
are consistent,
because domainspecific and generic axioms will be built on them. Other
important metatheoretical 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
20061018

