Let us assume, this theory is defined in standard first order
logic. Then
is the signature with a set of
function symbols
, a set of relation symbols
and a set of
constant symbols
, with
.
is a function
and is called arity. The alphabet over
,
consists of a set of individual variables
, the symbols given by the signature
,
and
, and the symbols
. The set
of terms is the smallest set containing
and closed under
(that is, if
, then
). An atom formula is a string of
the form
, where
. The set
of formulas is the
smallest set of strings over
containing the atom
formulas and being closed under the conditions: if
, then
. If
and
is free in
, then
. Let
, then
is
called a theory. If the signature is fixed, we omit
and write
just
for theory.
An interpretation over a signature
is a structure
(called
-structure)
which is defined
by a set of
individuals
,
,
,
. Let
,
if
,
otherwise.
A universal defines a theory and perhaps a signature. Therefore, we note a
universal by
, where
is a signature and
a theory.
has to fulfill the following condition: All formulas
have at most one free variable, at least one formula has one
free variable.
Let
be the signature of an ontology such as GFO,
be the ontological language and
be a theory defined in the language
, where
may contain additional symbols for
relations and functions and
. Let
be
ontological axioms, such as
the axioms of GFO,
. Let
be the
deductive closure of
. Then we do the following expansion:
Let
be the set of all occurrences of a string of
the form
in elements of the set
, where
is an individual and
is an universal, where
is the free
variable in
(with
). Then
.
Another way to achieve the same result is by extending the deduction
relation
by
, where the following obtains:
Sometimes this will lead to an infinite loop (if contains itself
a string of the form
), which does not
concern us at this time. A more detailed explanation of universals
and how they are specified will be developed soon by the GOL-Group.
We, however, believe, that any such explanation will have to satisfy at
least the formalism described above.
There will be certain properties which the theories specified by universals
will have to fulfill, for example, that the free variable in those
theories can only occur as the argument in such relations, that take
an appropriateentity as its argument. There may be more restrictions imposed on
those theories, either because it is necessary from an ontological
perspective or from a computational. For example, we may assume, that
all theories defined by universals are
-theories
. We may even impose
restrictions on the theory, for example when we
want to assert, that one and only one relation is used in it. Again, a
further analysis will be left open to the GOL-researchers.
When the signature is known, clear from the context or unimportant, we will denote universals as follows:
leechuck 2005-04-19