  The definition is a common form of human expert knowledge, a building block
of formal science and mathematics, a foundation for database theory and is
supported in various forms in many knowledge representation and formal
specification languages and systems. This paper is a formal study of some of
the most common forms of inductive definitions found in scientific text:
monotone inductive definition, definition by induction over a well-founded
order and iterated inductive definitions. We define a logic of definitions
offering a uniform formal syntax to express definitions of the different sorts,
and we define its semantics by a faithful formalization of the induction
process. Several fundamental properties of definition by induction emerge: the
non-determinism of the induction process, the confluence of induction
processes, the role of the induction order and its relation to the inductive
rules, how the induction order constrains the induction process and,
ultimately, that the induction order is irrelevant: the defined set does not
depend on the induction order. We propose an inductive construction capable of
constructing the defined set without using the induction order. We investigate
borderline definitions of the sort that appears in definitional paradoxes.
