Re: [ontolog-forum] Axioms and definitions

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

Pat, 

sometimes it's useful to build axiomatic theory of application area (3D-shapes in space logic in your case?). 

We need to get primary ("primitive") set of terms and write axioms of application area.

Definition is a way to introduce new "secondary" term in such a way that it may be eliminated from the formulas.

In your case if "part" is primary and properPart is secondary then D8 is a definition. But if "properPart" is primary too then D8 is an axiom.

Alex

2013/12/2 Patrick Browne <patrick.browne@xxxxxx>

Hi,
I am trying to understand the distinction between terms 'axiom' and 'definition' in an ontological and logical context.
Do the terms have the same meanings in logic and as they do in an ontological context?
Are the terms really distinct in their respective contexts?
Below is my background research and a fragment of BFO that I am currently working on.
I appreciate that the knowledge level of contributors to this forum is extremely high.
So, if my above questions and the research below are naive perhaps there is a beginners level forum that I could use.

Regards,
Pat Browne

== From philosophy ==
According Joseph[1] a definition “makes explicit the intension of a term, the essence it represents”.
 Joseph lists two types of logical;
 1)logical definition expresses the essence of a species in terms of its proximate genus and its specific differentia,
 2)definitions definition by property. 
Other types of definition described by Joseph are: causal definitions,descriptive definition, definition by example.

An axiom is a statement for which no proof is required Flew[2]
A definition is a process or _expression_ that provides the precise meaning of a word or phrase. Flew[2].
An axiom may be thought to constitute an implicit definition of the terms it contains or to contribute to such definitions. Flew[2]
 
== From Mathematics ==
Definitions are only required to be understood, they do not assert the existence or non-existence of anything. (Heath[3] page 119)
According Hunter[3] formal system S is a formal language L with deductive apparatus given by
1) laying down by fiat that certain formulas of L are to be axioms.
2) laying down by fiat a set of transformation or inference rules

Necessary features from of a good mathematical definition from VanDormolen & Zaslavsky[8] are as follows
Criterion of hierarchy: According to Aristotle, any new concept must be described as a special case of a more
general concept a square is a quadrilateral (general concept) with four congruent sides and one right angle
(special case).
Criterion of existence: Also required by Aristotle this criterion demands proof that at least one instance of the newly defined concept exists.
Criterion of equivalence: If one gives more than one definition for the same concept, one must prove that they are equivalent.
Criterion of acclimatization: A definition must fit into and be part of a deductive system.


== From Ontology/Knowledge Representation ==
In the OWL language the term defined class means a class that has necessary and sufficient conditions for membership.
The  “necessary” part alone is required for the semantics of IS-A that permits generalization or specialization.
Definitions in terms of primitives ultimately derive from Aristotle's mode of definition of genus and differentiae Sowa[5]
Three views on definition: classical, probabilistic, prototype, definitions can specify type(104) Sowa[5]
Types of definitions constructive, non-constructive, implicit, explicit, extensional, intensional, recursive Sowa [6]

== From my own research ==
This example represents my efforts to represent parts of BFO[7] in equational logic using loose semantics
Equations labelled with A indicates that the formula is an axiom, ‘D’ that it is a definition.
Mereology equations, variables A5-D8 are universally quantified, D9 has one existential quantifier
eq  [A5] : part(x, x) = true .
ceq [A6] : part(x, z) = true if (part(x, y) and part(y, z))  .
eq  [A7] : (x = y) = if (part(x, y) and part(y, x)) then true else false fi .
eq  [D8] : properPart(x, y) = (part(x, y) and  not(x = y)) .
-- Skolem functions are named using the variable in the BFO manual and axiom number
op  z9 : Entity Entity -> Entity
eq  [D9] :  overlap(x, y) = (part(z9(x,y), x) and part(z9(x,y), y)) .



 References
[1] Joseph, S. M. (1937). The Trivium: The Liberal Arts of Logic, Grammar, and Rhetoric, Dry Books.
[2] Flew, A. (1979). A Dictionary of Philosophy, Pan Books.
[3] Heath, T., Ed. (1925). Euclid: The thirteen books of the elements., Dover (1956).
[4] Hunter Geoffrey Metalogic: An Introduction to the Metatheory of Standard First-Order Logic,, University of California Press, 1971
[5] Sowa, J. F. (1984). Conceptual structures: information processing in mind and machine, Addison-Wesley Longman Publishing Co.
[6] Sowa, J. F. (2000). Knowledge Representation : Logical, Philosophical and Computational Foundations Brooks/Cole.
[7] Grenon and Smith SNAP and SPAN : Towards Dynamic Spatial Ontology
[8]Van Dormolen, J., & Zaslavsky, 0. (2003). The many facets of a definition: The case of periodicity. Journal of Mathematical Behavior, 22, 91-196.

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