Re: [ontolog-forum] Axioms and definitions

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

John & All,

may be it's a good idea to wake up https://sites.google.com/site/definitionsportal/home and https://groups.google.com/forum/#!forum/definitionsportal

created by Selja Seppala this summer?

Alex

2013/12/3 John F Sowa <sowa@xxxxxxxxxxx>

Enrico and Alex,

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:

  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.

  2. More detailed specializations of the definitions in #1 for
     each version of logic and/or ontology.

  3. Theoretical analyses (with citations) that get into the very
     detailed and sometimes thorny issues implied by #1 and #2.

To illustrate the kinds of issues, consider Enrico's point:

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".

In mathematics, explicit definitions are also called 'closed form'.
See http://en.wikipedia.org/wiki/Closed-form_expression

For example, you can write

    f(x) = x + 1.

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.

But when f occurs on the right, you have a recursive function,
which cannot be eliminated by a simple substitution:

    f(n+1) = n * f(n).

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.

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':

    (forall (x) (= (f x) (+ x 1)))

In Common Logic, quantifiers can range over functions and relations.
Therefore, any use of a new name, such as f, implies the following:

    (exists (f) (forall (x) (exists (y) (= y (f x))

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.

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.

John

_________________________________________________________________
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

_________________________________________________________________
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    (01)