I am trying to understand the distinction between terms 'axiom' and 'definition' in an ontological and logical context.
In first-order logic, and in FOL-based ontologies, an axiom is an arbitrary closed formula, which basically restricts the set of models of your ontology.
A definition is an axiom (or a set of axioms) such that a predicate in the definition "is defined" from the other predicates in the definition. A predicate "is defined" from a set of predicates, iff for any two models of the ontology whenever the two models agree on the extension of the defining predicates then the two models agree on the extension of the defined predicate. In other words, the truth value of a defined predicate depends only on the truth value of the defining predicates and it does not depend at all from the non defining predicates.
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".
An example is the following:
∀x. PERSON(x) → (MALE(x) ∨ FEMALE(x)).
∀x. MALE(x) → PERSON(x).
∀x. FEMALE(x) → PERSON(x).
∀x. MALE(x) → ¬FEMALE(x).
In this ontology, each predicate is implicitly defined by the other two. Indeed, the ontology states that PERSON is partitioned exactly between MALE and FEMALE. If I know everything about MALE and FEMALE, I know everything about PERSON (it is their union); if I know everything about MALE and PERSON, I know everything about FEMALE (it is the difference between PERSON and MALE); If I know everything about PERSON and FEMALE, I know everything about MALE (it is the difference between PERSON and FEMALE).
The explicit definitions (which are entailed by the ontology) indeed are:
∀x. PERSON(x) ↔ (MALE(x) ∨ FEMALE(x)).
∀x. FEMALE(x) ↔ (PERSON(x) ∧ ¬MALE(x)).
∀x. MALE(x) ↔ (PERSON(x) ∧ ¬FEMALE(x)).
In FOL, whenever a predicate is definable, it is always possible to get constructively its explicit definition.
Whatever I said above was deeply studied in the 50’ies by Beth and Craig.
To read about that with a modern ontology twist :-) you can look at [1,2].
cheers
—e.
[1] Enrico Franconi, Volha Kerhet, and Nhung Ngo. Exact query reformulation over databases with first-order and description logics ontologies. Journal of Artificial Intelligence Research (JAIR), 48, 2013.
[2] Balder ten Cate, Enrico Franconi, and İnanç Seylan. Beth definability in expressive description logics. Journal of Artificial Intelligence Research (JAIR), 48:347–414, 2013.