Enrico and Alex, (01)
I agree with your comments. But the issues raised by Pat B
show that we need a glossary or reference manual that addresses
these issues at several levels: (02)
1. Short, simple, general, but accurate definitions that are
sufficiently underspecified that they are true for the many
versions of logic we have been discussing. (03)
2. More detailed specializations of the definitions in #1 for
each version of logic and/or ontology. (04)
3. Theoretical analyses (with citations) that get into the very
detailed and sometimes thorny issues implied by #1 and #2. (05)
To illustrate the kinds of issues, consider Enrico's point: (06)
EF
> A special case is the "explicit" definition, when the defined predicate
> is explicitly stated to be logically equivalent to a formula including
> only the defining predicates. This is expressed in FOL as a universal
> bi-implication (mentioned by John), or in OWL as a definition statement
> in a TBox. Otherwise the definition is called "implicit". (07)
In mathematics, explicit definitions are also called 'closed form'.
See http://en.wikipedia.org/wiki/Closed-form_expression (08)
For example, you can write (09)
f(x) = x + 1. (010)
Then any occurrence of f with any value for x can be replaced
by the expression on the right with x replaced by that value. (011)
But when f occurs on the right, you have a recursive function,
which cannot be eliminated by a simple substitution: (012)
f(n+1) = n * f(n). (013)
In logic, explicit or closed-form definitions are also called
'conservative' extensions because any theorem that can be proved
by using them does not add significant information. They are just
abbreviations or "notational variants" that can always be eliminated. (014)
But in some recent discussions about the Common Logic standard,
a question came up about the meaning of 'conservative'. For
example, the following statement introduces a new name 'f': (015)
(forall (x) (= (f x) (+ x 1))) (016)
In Common Logic, quantifiers can range over functions and relations.
Therefore, any use of a new name, such as f, implies the following: (017)
(exists (f) (forall (x) (exists (y) (= y (f x)) (018)
This statement is also true in first-order logic. However, pure FOL
is not sufficiently expressive. Therefore, you can't write this
statement in pure FOL. (019)
As a result, some people have claimed that FOL is conservative, but
CL is not. But I claim that CL is just as conservative as FOL because
the statement is just as true for FOL as it is for CL. The fact that
FOL can't express it doesn't mean that it's false. (020)
John (021)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (022)
|