Barry, (01)
I agree with the basic idea, but I'd add a few
comments: (02)
> I note that there is a second way in which types can
> be represented in CL, which I am confident John will
> agree is possible:
>
> we introduce two sorts of individual variables,
>
> x, y, z ... for instances (particulars)
>
> u, v, w ... for types
>
> together with a two-place predicate instance_of to assert
> things like
>
> Fido instance_of dog. (03)
Yes. You could define instance_of and subtype by sentences
written in the untyped core: (04)
(forall (x y)
(iff (instance_of x y) (y x)) ) (05)
This says that x is an instance of y if and only if
y is a monadic relation that is true of x. Following
is a definition of subtype: (06)
(forall (x y)
(iff (subtype x y)
(forall z
(if (instance_of z x) (instance_of z y)) ))) (07)
> In this way we can quantify, harmlessly, over types,
> and yield (albeit trivially) some of the benefits of
> second-order logic. (08)
My only objection is to say that this is more than trivial,
since it supports all the common applications people want
when they ask for the ability to quantify over relations. (09)
The ability to quantify over the uncountable set of all
possible relations (including those that are not definable)
is important in mathematical studies of Cantor's hierarchy
of infinities. But for any ontology that is supposed to
be implemented on a digital computer, it's not possible to
define an undefinable relation, much less implement one. (010)
John Sowa (011)
_________________________________________________________________
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 (012)
|