Dear Matthew and Barry, (01)
Let me start with Matthew's remark, which gets to the
heart of my proposal: (02)
MW> The level above whether you are 3D or 4D is about
> foundations. What set theory do we use, or do we use
> Category theory or Type Theory. And what about number
> theory (we do want numbers don't we?) The reality that
> I see is that you are no more certain or free of
> controversy at what ever level you operate at. (03)
For the past five years on SUO list, the most heated
arguments have been about foundations. Therefore, I
propose that we eliminate *all* foundations. The type
Set and the type Number, will indeed be in the unified
framework (which I'll refer to as UF), but neither
Peano's axioms nor the axioms of any version of set
theory will be in UF. (04)
The point is that UF is primarily intended as a framework
for communication among potentially (or actually) incompatible
systems. The major inconsistencies arise at the level of
axioms, which none of these systems would accept from one
another. But they can usually accept lower-level facts
without creating any conflict. (05)
Therefore, UF should be very rich in types, but very, very
poor in axioms. But any serious inferencing (which may be
logic based, statistical, computational, or whatever) will
require much more. But every system that adds more does
so in ways that are incompatible with some other system. (06)
Any axiom that causes a conflict with any major system shall
be deleted from UF, but there may also be a large number of
microtheories (as in Cyc) or modules (as in the following
remark) which could be very rich in axioms expressed in
very rich versions of logic. (07)
BS> BFO has two modules, one 3-D (defined for representing
> continuants), one 4-D (designed for representing processes),
> together with relations between them. Users are welcome
> to use either both modules together, or just one of them,
> according to preference. (08)
That's an excellent principle. Any axiom that is deleted
from UF will not go away, but it will be available in
modules or microtheories that could be used as needed
by various systems. In effect, the topmost levels of most
ontologies are the most controversial. Therefore, UF
should have a highly impoverished top level. (09)
As I said before, UF should resemble a cleaned up version
of WordNet with all the errors corrected and with a major
influx of new vocabularies. But nobody likes the WordNet
top level, and most people who use WN ignore it. Therefore,
UF should have an extremely simplified top level, with all
the complexity moved to modules or microtheories. (010)
Basic principle: It should be possible to import any
subset of UF into any of the major systems such as Cyc,
SUMO, Dolce, etc., without any fear of inconsistencies
caused by conflicting axioms. It may be necessary to
do some alignment of terminology, but after that has
been done, the axioms should not conflict. (011)
BS> ... though we will need a bit more
> than the syllogism if we are to deal adequately with the
> distinction between instances (Toronto) and types (city).
> The fact that this distinction has not been dealt with
> adequately flows in part from the fact that people were
> assuming that something like syllogistic would be adequate
> for their needs. (012)
I certainly agree with the first point, but I'd like to
throw in a good word for Aristotle and the Scholastics,
who were very clear about the distinction between types
and instances. (013)
In any case, I used the term "syllogism" to indicate the
very limited level of logical expressivity required for
the core UF. I would assume that the tools used to support
UF would enforce the distinction between types and instances. (014)
John Sowa (015)
_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config:
http://colab.cim3.net/mailman/listinfo/ontac-forum/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki:
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG (016)
|