In this chapter, we discuss the mathematical principles of recursive definitions; while such definitions are less prominent in classical mathematics, they pervade many areas of computer science and thus deserve special attention. We start with a simple logical characterization of recursion that neither determines a unique function nor guarantees its existence.We then discuss the form of “primitive recursion” that always guarantees the existence of a unique solution but is of limited expressiveness. The main part of this chapter is then dedicated to a general theory of recursion based on the concept of “least/greatest fixed points” of certain higher-order functions that arise from recursive definitions. We show how this theory gives rise to “inductive” and “coinductive” definitions of relations and functions and finally discuss the principles of proving properties about the entities defined in this way.