Dissertation, Carnegie Mellon University (2019
Inductively defined structures are ubiquitous in mathematics; their specification is unambiguous and their properties are powerful.
All fields of mathematical logic feature these structures prominently: the formula of a language, the set of theorems, the natural numbers, the primitive recursive functions, the constructive number classes and segments of the cumulative hierarchy of sets.
This dissertation gives a mathematical characterization of a species of inductively defined structures, called accessible domains, which include all of the above examples except the set of theorems.
The concept of an accessible domain comes from Wilfried Sieg's analysis of proof-theoretic practices, starting with his dissertation.
In particular, he noticed the special epistemological character of elements of an accessible domain: they can always be uniquely identified with their build-up.
Generally, the unique build-up of elements justifies the principles of induction and recursion.
I use category theory to give an abstract characterization of accessible domains.
I claim that accessible domains are all instances of initial algebras for endofunctors.
Grounded in the historical roots of Sieg's discussions, this dissertation shows how the properties of initial algebras for endofunctors and accessible domains coincide in a satisfying and natural way.
Filling out this characterization, I show how important examples of accessible domains fit into this broad characterization.
I first characterize some accessible domains by relatively simple functors (e.g. finite, polynomial, those that preserve certain colimits) where we can see how iterating the functor can produce the accessible domain.
Then I describe accessible domains that result from more involved specifications (e.g. ordinals and segments of the cumulative hierarchies associated with CZF, IZF, and ZF) by relying heavily on algebraic set theory.
I end with a discussion of some of the methodological features of category theory in particular that helped characterize accessible domains.