Hi John, (01)
I haven't followed what came earlier but, in this exchange, it seems
to me Barry's suggestion truly is an alternative to your types as
'monadic relations', more in response below. (02)
On 1/21/06, John F. Sowa <sowa@xxxxxxxxxxx> wrote:
> > 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.
>
> Yes. You could define instance_of and subtype by sentences
> written in the untyped core:
>
> (forall (x y)
> (iff (instance_of x y) (y x)) ) (03)
Although I gather that if the original motivation is ontological the
idea is that instance_of is a primitive (that would not ask for a
definition). But the main point might just be that the types are
individuals. That point only should make the definition you're
suggesting fail, because (y x) would either yield non--sense or in the
best case falsehood. (04)
> 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:
>
> (forall (x y)
> (iff (subtype x y)
> (forall z
> (if (instance_of z x) (instance_of z y)) )))
>
> > In this way we can quantify, harmlessly, over types,
> > and yield (albeit trivially) some of the benefits of
> > second-order logic.
>
> 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. (05)
(I don't understand the objection but nevermind.) (06)
> The ability to quantify over the uncountable set of all
> possible relations (including those that are not definable) (07)
But that's beyond the point, the types in question do not come up as
predicates but individuals. There's no worry nor bother with sets
(extensions of predicates). It's not about quantifying over classes. (08)
Best,
Pierre (09)
> 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.
>
> John Sowa
>
>
> _________________________________________________________________
> 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
> (010)
_________________________________________________________________
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 (011)
|