Ordinal analysis of the formal theory for noniterated inductive definitions

Abstract

We already frequently used inductive definitions during this lecture. We used it to define terms, formulas, derivations in formal and infinitary systems and also other concepts. Inductive definitions, however, are not only used in mathematical logic but are ubiquitous in mathematics. Whenever we define a set as the least set which comprehends a given set and is closed under certain operations, we use an inductive definition. One of the simplest examples is the subspace <A> of a vector space V generated by a set A⊂V. <A> is defined as the smallest set which comprehends A and itself is a vector space, i.e. is closed under addition and scalar multiplication. This does not look like an inductive definition as we are used to. But we also may put it into the more familiar form of a definition by clauses:

where K denotes the ground field.