Case Studies in Constructive Mathematics
Not peer reviewed
MetadataShow full item record
The common theme in this thesis is the study of constructive provability: in particular we investigate aspects of ﬁnite sets and Kan simplicial sets from a constructive perspective.
There are numerous deﬁnitions of ﬁniteness which are classically equivalent but not constructively so. In other words, constructive mathematics is able to distinguish between more notions of ﬁniteness. We start by investigating some relationships between several ways of deﬁning ﬁniteness for sets of natural numbers. As a new result, we give strictly bounded a precise placement in a hierarchy of deﬁnitions of ﬁniteness.
We also investigate streamless sets, which constitutes another notion of ﬁnite- 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 ﬁniteness 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 deﬁned 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 deﬁnition 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 deﬁnitions of Kan simplicial sets.
Paper I: Erik Parmann. Strictly Bounded Sets. Manuscript. The article is not available in BORA.
Paper II: Erik Parmann. Investigating Streamless Sets [Par15]. In 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 187–201. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015. The article is available at: http://hdl.handle.net/1956/11725
Paper III: Erik Parmann. A proof that Noetherian relations are streamless in a type theory without identity. Manuscript. The article is not available in BORA.
Paper IV: Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets [BCP15]. In 13th International Conference on Typed Lambda Cal- culi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 92–106. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015. The article is available at: http://hdl.handle.net/1956/11729
Paper V: Erik Parmann. Functional Kan Simplicial Sets: Non-Constructivity of Exponen- tiation. Submitted to 21th International Conference on Types for Proofs and Programs (TYPES 2015). Manuscript. The article is not available in BORA.