SUO: Re: Language and Module Processing
Jon,
.> 1. What's actually in the boxes labelled
> "SUMO", "S_1", "S_1", "S_3", ...,
> "OpenCyc", "O_1", "O_2", "O_3", ...?
My assumption has been that these are unpopulated object-level ontologies
represented as FOL theories in the IFF. A FOL theory T = (L, A) has two
components: a FOL language L and a set of L-expressions A called axioms. A
FOL (sorted) language L consists of a set of entity symbols ent(L) (aka
sorts), a set of relation symbols rel(L), and a set of function symbols
ftn(L). Constant symbols are nullary functions, they have empty arity but
have a return of a certain sort, and are included in ftn(L), but could be
displayed as const(L) if desired. The principal semantic (and also
proof-theoretic) relation on theories is the binary entailment relation
between a theory and an expression. A theory T entails an expression e,
symbolized
T |- e
when any model for (the axioms of) T is also a model for e. Any expression
entailed by T is called a theorem of T. Derived from this is the lattice
order where two theories are ordered as T1 <= T2 when T1 entails all the
axioms of T2; this order is called entailment order. Two boxes or nodes T1
and T2 are displayed as linked
T2
|
T1
in a diagram for a library of modules when they are ordered T1 <= T2 in the
lattice order.
> 2. In order to think about order-flipping dualities (of the galois kind),
> it usually helps me to draw both of the lattices that are involved,
> so let me make an ascii stab at that:
>
> M_X = X T_L = L
> full set, full set,
> all models in space X. all "descriptors" in L.
> o o
> | . . |
> | . . |
> M_1 |_| M_2 o . . o T_1 |_| T_2
> / \ . . / \
> / \ . . / \
> / \ . . / \
> M_1 o o M_2 . T_1 o o T_2
> \ / . . \ /
> \ / . . \ /
> \ / . . \ /
> M_1 |^| M_2 o . . o T_1 |^| T_2
> | . . |
> | . . |
> o o
> M_0 = {} T_0 = trivial theory,
> null set, no information above
> no models. what's already given.
These two diagrams are projections out of the strictly presented truth
concept lattice. The diagram of closed subclasses of models on the left is
the extent projection, whereas the diagram of closed subsets of expressions
(aka closed theories) on the right is the flip (it is normally presented
flipped over) of the intent projection. In the strictly presented truth
concept lattice, each node is represented by a pair (M, T), where M is a
closed subclass of models and T is a closed subset of expressions (aka a
closed theory). As for any concept lattice, either aspect implies the other,
and since the extent-ional aspect is set-theoretically large in the case of
truth, the IFF only uses the intent-ional aspect, that is, it only uses
closed theories in the formal presentation of the truth concept lattice.
For any fixed FOL language L, the IFF represents both the truth concept
lattice tcl(L) and the lattice of theories lot(L). They are connected by the
restricted closure operator
clo(L) : lot(L) --> tcl(L)
where the closure of an L-theory T is the set-theoretically larger theory
consisting of all theorems of T.
The truth concept lattice tcl(L) can be derived from (actually is
categorically equivalent to) the truth classification tcls(L). Recall that a
classification is a binary relation on two collections, where the first
collection of things is regarded as a collection of instances, the second
collection of things is regarded as a collection of types, and when an
instance is related to a type it is regarded as being of that type or being
classified by that type. The truth classification for L is the large
classification of satisfaction between the models of L and the expressions
of L. An L-model M satisfies (or is a model of) an L-expression e,
symbolized by
M |= e
when all tuples of M satisfy e. The concept lattice tcl(L) generated by the
truth classification tcls(L) is called the truth concept lattice of L. As
mentioned above, when this is strictly presented it is set-theoretically
large, with each element having both a closed subclass of models and a
closed subset of expressions (a closed theory). But the IFF only uses the
closed theories in its presentation of tcl(L). That is, in the IFF the
tcl(L) is the complete lattice of closed L-theories whose order is reverse
subset inclusion on closed theories, whose joins are given by set-theoretic
intersection, and whose meets are given by the two-step process of
set-theoretic union followed by closure. In the IFF the lattice of theories
lot(L) is the complete preorder consisting of all L-theories whose order is
entailment order, whose meets are given by set-theoretic union.
Hope this helps.
Robert E. Kent
rekent@ontologos.org