Re: [ontolog-forum] Axioms and definitions

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

John,

we have a lot of exciting and subtle examples of definitions and axiomatic theories in math, but what about natural sciences and technologies (NSaT)?

This what I have asked  about Hilog at webinar (see): do they have ontologies (texts) on Hilog of NSaT knowledge? They say "yes". Then next question - where?

And this is a question to CL, λProlog, OWL2 and other great formal languages. Even Pat's example is from math logic (mereology).

From other hand Barry Smith in "Introduction to the Logic of Definitions" (see) analized real definitions in biology even before formalization.

On the middle we (see) have got some formal definitions of rock types in petrology. I hope formula on slide 29 is a CL one:-)

Axioms and formal definitions of NSaT this is a deal.

Alex

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

Ed and Alex,

EJB

> ‘definition’ and ‘equivalence’ are NOT the same thing in formal languages.

That is true.  Another way to summarize the issues:

     A definition is assumed to be true "by definition".  But
     an equivalence (which uses if and only if) can be false.

In fact, Common Logic uses the following "trick" to avoid paradoxes:

  1. CL has no special syntax for a definition statement.

  2. Therefore, no sentence in CL is forced to be "true by definition".

  3. For example, the following "definition" creates the famous
     contradiction in set theory that was discovered by Cantor, but
     attributed to Bertrand Russell (because BR had better PR):

     Define S as the set of all sets that are not members of themselves.

  4. But if you use an equivalence to specify a relation named BigSet,

     (forall (x Set)
        (iff (BigSet x)
             (forall (y Set) (iff (in y x) (not (in y y))) ))

  5. There is no x that can satisfy the last line.  Therefore,
     BigSet happens to be true of nothing.  There's no paradox.

EJB

> It is much safer in logic languages to treat all predicate symbols
> as first-class primitives and define their relationships axiomatically,
> because then you only need a model theory for interpreting the axioms.

That's effectively what CL does:  Avoid a distinction between axioms
and definitions.  If there is a contradiction, then the theory happens
to be unsatisfiable.  It's not a paradox.

AS
> maybe it's a good idea to wake up ... created by Selja Seppala this summer?

For the record, following is a list of workshops and articles organized
by and written by Selja S:  http://seljaseppala.wordpress.com/page/4/

They are worthy and respectable additions to the thousands of other
workshops and articles organized and written on this and related topics.

For anybody who has had 30+ years of attending workshops and writing
articles on such topics, it's nice to know that there are still people
who get excited about such things.

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)