Case Studies in Constructive Mathematics
Erik Parmann · NORA - Norwegian Open Research Archives · 2016
The common theme in this thesis is the study of constructive provability: in particular we investigate aspects of finite sets and Kan simplicial sets from a constructive perspective. There are numerous definitions of finiteness which are classically equivalent but not constructively so. In other words, constructive mathematics is able to distinguish between more notions of finiteness. We start by investigating some relationships between several ways of defining finiteness for sets of natural numbers. As a new result, we give strictly bounded a precise placement in a hierarchy of definitions of finiteness. We also investigate streamless sets, which constitutes another notion of finite- ness. Streamless sets require neither decidable equality nor that the set is a subset of an enumerable set, and they are as such more general than strictly bounded sets. It is an open problem whether the Cartesian product of two streamless sets is itself streamless. We show that this holds if at least one of the sets has decidable equality or is of bounded size. The problem remains open for the case where both streamless sets have undecidable equality and fail to be of bounded size. We also show that—in certain constructive systems—the addition of function extensionality makes equality within streamless sets decidable. Another notion of finiteness is Noetherian. Both streamless and Noetherian can be generalized to properties of binary relations, whereby such sets are those where equality is respectively streamless or Noetherian. We provide a proof that all Noetherian relations are streamless—notably, in a type system without inductively defined equality. This result immediately entails that all Noetherian sets are streamless within that type system. We proceed to investigate aspects of Kan simplicial sets, a notion coming from topology. Kan simplicial sets have recently caught the eye of the type theory community since they can be used to build models of Martin-L¨of type theory that validate the Univalence axiom. All known proofs of the following well-known theorem use classical logic: if simplicial sets X and Y are Kan simplicial sets then Y X is also a Kan simplicial set. This theorem plays an important role in the Kan simplicial set model of type theory. We investigate whether this theorem also holds constructively. The classical definition of the Kan property has at least two non-equivalent constructive interpretations, and we provide countermodels showing the constructive non-provability of the classical theorem above for both of these definitions of Kan simplicial sets.