On 12/2/2013 7:39 AM, Patrick Browne wrote:
> I am trying to understand the distinction between terms 'axiom' and
> 'definition' in an ontological and logical context. (01)
The practice by mathematicians and logicians for over 2000 years is
based on Euclid, who tried to follow Aristotle's recommendations as
far as he could. But he had to use more logic than A's syllogisms. (02)
But there are many variations and recommendations about the details. (03)
General principles for any language or logic L that has associated
reasoning methods. They can be syntactic methods, which are called
*rules of inference*, or they can be semantic (i.e., model theoretic)
*entailments*. For first-order logic, the syntactic and semantic
consequences are equivalent. (04)
1. Every statement is a sentence in L. (05)
2. A theory T is a set of sentences in L that is deductively closed:
Any sentence implied (or entailed) by any subset of sentences in T
is also in T. (06)
3. Axioms and definitions are sentences that are assumed to be true
of some domain or universe. Their deductive closure is a theory. (07)
4. A hypothesis is a sentence that might not be true, and its
consequences are analyzed in terms of the axioms and definitions
of some theory. (08)
In some logics, such as Common Logic, there is no formal distinction
between axioms and definitions. But many mathematicians and logicians
since Aristotle have used special forms for definitions. In CL, the
typical form for a definition is an equivalence statement. The
following sentence defines a relation R in terms of some sentence
that may refer to names that are mentioned in other sentences. (09)
(forall (x y z)
(iff (R x y z)
( /* some sentence that uses x, y, and z */ ) )) (010)
The conventions that Patrick cited in his note (copied below) are
reasonable, and many people have found them useful. They could be
adopted as constraints on the CL sentence that defines R. (011)
John (012)
== 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. (013)
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] (014)
== 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 (015)
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. (016)
== 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] (017)
== 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)) . (018)
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. (019)
_________________________________________________________________
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 (020)
|