Indeed category theory is a mathematical formalism which is being used for
ontology, even in cases where the users are unaware of it. The reasons are
straight forward. A category is really a directed graph with a path
composition operation and possibly other language constructions. Many
applications in science and engineering make heavy use of directed graphs,
including John’s bridge example in more ways than one. (01)
Benzene is a good example test case for an ontology language. The idea is to
give an axiom set in a logic for the class of benzene molecules. Then use
automated reasoning answer questions about the structure of benzene
molecules. For example, one would like to ask in the ontology language the
question “whether any benzene molecule has a carbon ring? “ Automated
reasoning can give the correct answer only when all of the benzene molecules
in any valid interpretation have the structure such as is shown in the
diagram :
image:
http://media1.picsearch.com/is?8Pu5G3VX2yKV0e-u-4aq4q12Q8DGv_UKZslfRR_RSLM&height=254
Reasoning on DL axiom sets cannot answer this question correctly, as the DL
axioms will always have a tree structured model which does not conform to
this picture. Remember, the diagram and the axiom set are description
templates, rather than descriptions of a specific molecule. (02)
However, one can give first order axioms for Benzene which constrain all the
models to consist of molecules which only have the correct shape. This is
not a trivial result. I repeat the comment that approach separates the
logical language used to express the axioms from the logic’s term language
which is the ontology language. The logical langauge is classical first
order, the term language may or may not be classical (03)
A category theory can be used as an ontology language by giving FOL axioms
for the language constructions such as path composition. One needs a bit
more ontology language constructions than a directed graph for this example,
but not a lot. The axioms use two sorts, nodes and arrows. I will call them
types and maps. A category theory person would call them objects and maps.
Some of this was noted in some of the earlier exchanges with Alex. The
axioms for composition are of course partial, as has been commented on
before. But as the conditions for composition to be well defined are
decidable, there really is no problem with proof theory or model theory. (04)
The axioms for a category or directed graph with path composition can be
found in the Lambek and Scott book in the early pages. Of course a category
can be very large, but in engineering examples generally have finite models.
For example the benzene description with the right constructions generates
a category which has a canonical minimal finite model which looks like the
graphs one sees in Wikipedia. (05)
With regard to whether predicates are viewed as a form of classification, I
would say yes. But there is an important caveat. There are two logics
involved. One is the logic in which the axiom set is expressed which is
called the external logic. The other is that in a category with additional
structure such as a Cartesian close category or elementary topos, there is
an internal logic. These frameworks have a type constant symbol Omega. An
internal formula is a map q:X → Omega. If Omega reduces to {true,false}
then the internal logic looks like the external one. However, one can add
truth value constants in addition to true:X → Omega, and false:X → Omega
such as maybe:X → Omega. Then one gets a non-traditional logic. Type
theory, and rule systems such as Hilog, use this device of having an
internal representation of higher order logic as terms within a first order
presentation logic. The internal logic admits various generalization of
classical logic. The external predicates classify the terms, i.e.,
syntactic structures. The internal predicates classify things in the
interpretation. As an example of this idea, the external predicates allows
one to deduce that “the gun shot hit the target = maybe”. The statement is
an internal formulae and the equation is external. (06)
I would modify John’s comment slightly. If you have to ask what it is from
the viewpoint of ontology, the worst place to find out are standard text
books on category theory. The reason for this is it is usually presented as
a theory within set theory, rather than as a first order theory. Presenting
topos theory as a theory within set theory obviates ability to serve as an
ontology language. (07)
By the way, the signature of the Benzene axiom set, as I would do it, has 3
type symbol constants, Benzene, Hydrogen and Carbon. It also has 12 part
maps, and 12 type constructions, and 12 connection maps. I have not, of
course, indicated what the axioms are which are needed for the benzene axiom
set. (08)
Henson Graves (09)
-----Original Message-----
From: John F Sowa
Sent: Wednesday, July 09, 2014 12:01 PM
To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions
inontology (010)
Frank, Henson, and Ed, (011)
FG
> Given the discussions on Category Theory, I was curious if the
> community views Predicates as a form of categorization/classification. (012)
Two points: (013)
1. Category theory is a mathematical system that might be used for
ontology. But if you have to ask what it is, don't use it.
Brief summary: http://en.wikipedia.org/wiki/Category_theory (014)
2. Every class, type, or category in any ontology can be associated
with a predicate that is true of everything in the class, type,
or category and false of everything not in it. (015)
HG
> I believe the problem is that OWL axiom sets always have a tree
> model whether you want it or not. OWL axiom sets may have other
> models which are not trees. (016)
EJB
> Not quite 'trees' -- classification lattices, with 'property links'
> that produce more or less general semantic networks, including cycles. (017)
I agree with Henson. The OWL *classes* are organized in lattices.
But the *models* (in Tarski's sense) are limited to trees. (018)
For example, a benzene ring has a cycle. OWL cannot state the
critical properties that require a model of benzene to have a cycle. (019)
Just look at any bridge truss, and you'll find interconnected
triangles that create huge numbers of cycles. It's impossible
to find any complex artifact or biological system without cycles.
OWL cannot specify, analyze, or reason about those cycles. (020)
HG
> Where they have problems is in constructing OWL axiom sets for
> a molecule such as H2O which constrains the models to only consist
> of molecules with exactly three atoms. There are a lot of papers
> by Horrocks and Motik and students on this topic. (021)
I know Horrocks and Motik. They're intelligent, but they're
hopelessly *arrogant* to claim that they are qualified to tell
experts in every branch of science, engineering, and business
what models they're allowed to use, represent, and reason with. (022)
HG
> This has led them to try graph extensions of DL and logic
> programming extensions. (023)
Yes. And every one of those extensions adds more and more complexities
to an overly complex system. By comparison, the LP systems are easier
to learn and use and far more efficient for equivalent applications. (024)
Programmers and computer scientists have had far better methods
for controlling complexity and avoiding issues of undecidability.
They use various terms: structured programming, structured
analysis, design patterns, and knowledge compilers. (025)
When I wrote my article "Fads and Fallacies in Logic", the primary
fad I had in mind was OWL. And the primary fallacy was decidability
as the bogeyman: http://www.jfsowa.com/pubs/fflogic.pdf (026)
By the way, Jim Hendler was the editor of the journal in which it
was published. And he liked that article very much. (027)
John (028)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (029)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (030)
|