In my usual way of drawing on what I recollect from many years ago, I will risk getting this wrong.
In formal logic languages, there is an important distinction between ‘equivalence’ and ‘substitution’.
“Definitions” are associated with substitution: wherever there is an occurrence of X it can be replaced by the “definition of X”. But when X is a predicate
that has arguments, the set of substitution rules can be complex, because you have the “lambda calculus” problem of substituting the actual arguments in the reference to X for the appearances of parameters within the “definition” (formula) of X, and you have
to be sure this does not cause differences in the interpretation of the substituted “symbols”, if you do that substitution symbolically. (It is possible that you have some smarter mechanism for substitution, but then you have to define that mechanism.)
“Equivalences” are associated with inference: if two formulas are related by equivalence, and you can prove one of them, you can infer the other. In that
case, the only ‘substitution’ rules you have are those of your inference engine, which is part of the specification of the logic language itself – the model theory explains the interpretation of the equivalence when the arguments to a predicate refer to specific
individual things in the UoD. So (iff (P x y z) <formulation involving x, y, and z and other predicates>) does not involve any new substitution ideas; it only requires interpretation of the <formulation...>.
This is a poor man’s explanation, but the point is that ‘definition’ and ‘equivalence’ are NOT the same thing in formal languages. 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.
And OBTW, an OWL “definition” is an equivalence axiom, not a substitution rule. The OWL language does not have a notion of ‘argument’; even properties are
about sets of pairs.
-Ed
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx]
On Behalf Of Alex Shkotin
Sent: Tuesday, December 03, 2013 8:21 AM
To: [ontolog-forum]
Subject: Re: [ontolog-forum] Axioms and definitions
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.
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)
|