Re: SUO: type equivalence
Robert E. Kent said:
> I am currently contemplating quotients of "logical languages" via type
> equivalence, and would be interested to know what has been done on this
> subject. The central axiom would seem to be that relational type
> equivalence implies the type equivalence of its signature. To wit: (
> where == means type equivalence)
> if rho_1 == rho_2 then arity(rho_1) = arity(rho_2) and
> sign(rho_1)(x) == sign(rho_2)(x) for all x in arity(rho_i), i = 1, 2.
> This of course can easily be framed in KIF. Are there other obvious
> axioms?
I would like to know what you think a signature is.
In my starter structural ontology, the distinction is made between
the instance-of and the subclass-of relations on an argument to a
relation.
This means that if you know the argument to a relation is
an instance of CLASS, you must further specify which class it is a
subclass of. I would also argue that you need to deal with
inter-argument dependencies as well as only intra-argument definitions.
A separate issue is specifying how propositions that use the relation
are constrained. For some relations, it doesn't make sense to have two
propositions that are true at the same time.
As an (admittedly flawed) example, if you had a 'COLOUR' relation
which related automobiles to a single member of the set {RED,YELLOW,BLUE},
it would be a useful part of the signature/definition of the COLOR
relation to say that if you have (COLOUR AUTO-9876 RED) that you
cannot have (COLOUR AUTO-9876 BLUE) as well.
These are some of the structural relations that I am trying to define
for version 3 of the Starter Structural Ontology.
David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116