Universals

Now to universals. How can a universal with situations as its instances be specified? What would have to be specified? A universal specifies certain properties and relations of its instances. This may only be done using relations where at least one argument, one role has to be filled by the individual that is the instance of the universal. For example, the universal $ Human_s$, human being as a social being, would have to be specified by the relations the instances of this universal have to other human beings. On the contrary, $ Human_b$, human being as a biological entity, would be described by its anatomical parts and their spatial position, and maybe the function of those parts. In general, every universal defines a theory about its instances.

Let us assume, this theory is defined in standard first order logic[*]. Then $ \Sigma=(F,R,C;ar)$ is the signature with a set of function symbols $F$, a set of relation symbols $R$ and a set of constant symbols $ C$, with $ C \subseteq F$. $ ar$ is a function $ ar:F\cup R \mapsto \omega$ and is called arity. The alphabet over $\Sigma$, $ Al(\Sigma)$ consists of a set of individual variables $ Var$, the symbols given by the signature $\Sigma$ $ F(\Sigma)$, $ R(\Sigma)$ and $ C(\Sigma)$, and the symbols $ \exists, \neg, \land, ),
($. The set $ Tm(\Sigma)$ of terms is the smallest set containing $ Var
\cup C(\Sigma)$ and closed under $ F(\Sigma)$ (that is, if $ t_1,\ldots,t_n \in Tm(\Sigma), f \in F(\Sigma), ar(f)=n$, then $ f(t_1,\ldots,t_n) \in Tm(\Sigma)$). An atom formula is a string of the form $ R(t_1,\ldots,t_n)$, where $ R \in R(\Sigma),t_1,\ldots,t_n
\in Tm(\Sigma), ar(R)=n$. The set $ Fm(\Sigma)$ of formulas is the smallest set of strings over $ Al(\Sigma)$ containing the atom formulas and being closed under the conditions: if $ A,B \in
Fm(\Sigma)$, then $ \{ \neg A, A \land B \} \subseteq Fm(\Sigma)$. If $ A(x) \in Fm(\Sigma)$ and $ x$ is free in $A$, then $ \exists x A(x) \in
Fm(\Sigma)$. Let $ T(\Sigma) \subseteq Fm(\Sigma)$, then $ T(\Sigma)$ is called a theory. If the signature is fixed, we omit $\Sigma$ and write just $T$ for theory.

An interpretation over a signature $ \Sigma=(F,R,C;ar)$ is a structure (called $\Sigma$-structure) $ \mathcal{A}=(U,(f^{\delta})_{f \in
F}, (R^{\delta})_{R\in R},(c^{\delta})_{c \in C})$ which is defined by a set of individuals $ U$, $ f^{\delta}:U^{ar(f)}\mapsto U$, $ R^{\delta}\subseteq
U^{ar(R)}$, $ c^{\delta}\in C$. Let $ \mu:Tm(\Sigma)\mapsto U$, $ \mu(t)\in U$ if $ t \in Var$, $ \mu(f(t_1,\ldots,t_n))=f^{\delta}(\mu(t_1),\ldots,\mu(t_n))$ otherwise.

A universal defines a theory and perhaps a signature. Therefore, we note a universal $ u$ by $ u=(\Sigma, T)$, where $\Sigma$ is a signature and $T$ a theory. $T$ has to fulfill the following condition: All formulas $ F \in T$ have at most one free variable, at least one formula has one free variable.

Let $ \Sigma_{Ont}$ be the signature of an ontology such as GFO, $ L(\Sigma_{Ont})$ be the ontological language and $T$ be a theory defined in the language $ L(\Sigma_{Ont}\cup
\Sigma_T \cup \Sigma_=)$, where $ \Sigma_T$ may contain additional symbols for relations and functions and $ \Sigma_==\{=\}$. Let $ Ax(Ont)$ be ontological axioms, such as the axioms of GFO, $ T\cup Ax(Ont)=S$. Let $ S^{\vdash}$ be the deductive closure of $S$. Then we do the following expansion: Let $ Univ$ be the set of all occurrences of a string of the form $ x::u$ in elements of the set $ S^{\vdash}$, where $ x$ is an individual and $ u_i=(\Sigma_{U_i},T_{U_i})$ is an universal, where $ z$ is the free variable in $ T_{U_i}$ (with $ 1 \leq i \leq \vert Univ\vert$). Then $ S^{\vdash}_U=S^{\vdash} \cup \bigcup\{\exists
z(\bigwedge T_{U_i} \land x=z) : 1 \leq i \leq \vert Univ\vert\}$.

Another way to achieve the same result is by extending the deduction relation $ \vdash \subseteq 2^{Fm(\Sigma)} \times Fm(\Sigma)$ by $ (\{A\},A')$, where the following obtains:

Sometimes this will lead to an infinite loop (if $ T_u$ contains itself a string of the form $ x::u$), 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 appropriate[*]entity 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 $ \exists$-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:

Definition 5.30 (Notation for universals)   A universal $ u=(\Sigma, T)$ is denoted as follows:

$\displaystyle u = [ x \vert P(x) ]
$

leechuck 2005-04-19