- From: Dave Reynolds <der@hplb.hpl.hp.com>
- Date: Wed, 13 Jun 2001 16:50:56 +0100
- To: Drew McDermott <drew.mcdermott@yale.edu>
- CC: www-rdf-logic@w3.org
This is not my area so apologies if this is just noise ...
When I recently attempted to explain description logics and T-box/A-box
distinctions, a colleague likened them to the "=df" notation
("definitionally equal") in mathematical logic. He suggested that, at
least as logic used to be taught over here, you distinguished notationally
between three forms of equality, viz. "equal in one particular model",
"provably equal in all models, bi-equivalence" and "definitionally equal".
The distinction between the latter two affects how you construct your
proof theory even though for a given set of models you can't distinguish
between a tautology and a definition. The "not allowed to be false" nature
of T-boxes seems at least analogous.
Dave
Drew McDermott wrote:
> [Pat Hayes]
> As far as I know, there is no *mathematical* way to distinguish
> definitions and assertions.
>
> Correct me if I'm wrong, but don't logic textbook mention the case
> where a definition is simply an equality or if-and-only-if? E.g., you
> might write (bachelor ?x) <=> (and (male ?x) (not (married ?x))). Now
> take a theory involving the term "bachelor," and you can easily
> convert it to a theory that doesn't mention the term anywhere. This
> two-stage process neatly captures the idea of the definition "not
> being allowed to be false." By the time you catch a contradiction,
> the definition is nowhere to be seen.
>
> Of course, this won't work for recursive definitions, which may be why
> people like Russell didn't trust them. My knowledge of the history of
> logic is a bit shaky at this point.
>
> -- Drew McDermott
Received on Wednesday, 13 June 2001 11:51:08 UTC