Partiality and Choice : Foundational Contributions

Sammanfattning: The subject of the thesis is foundational aspects of partial functions (Papers 1, 2 & 4) and some choice principles (Papers 3 & 4) in the context of constructive mathematics.Paper 1 studies the inversion functions of commutative rings. The foundational problem of having them only partially defined is overcome by extending them to total functions. This cannot be done constructively unless the rings themselves are extended at the same time. We study such extensions, called wheels. It is investigated how identities for wheels relate to identities for commutative rings.Paper 2 studies the foundations of partial functions in Martin-Löf's type theory according to the view of subsets as propositional functions, in particular in connection with equivalence relations that the functions are supposed to preserve. The first and second isomorphism theorems of algebra are verified, showing that our approach is flexible enough for some natural mathematical proofs to be carried out.Paper 3 shows that the difference between the principles of intensional and extensional choice can be described as the principle of excluded middle plus a certain mild extensionality principle, which follows from the principle that functions are identical if they are identical at every point.Paper 4 studies a constructive calculus of indefinite and definite descriptions. It has the property that it can be interpreted straightforwardly in type theory with all terms referring to individuals. In this respect it differs from other constructive calculi of descriptions, which are known to be conservative extensions of description-free calculi but for which descriptions cannot be interpreted as referring to individuals in general.The appendix includes a predicative version of Birkhoff's theorem. It states that if a class of algebras is closed under homomorphic images, subalgebras and products and contains a set-indexed family of algebras that satisfies the same identities as the class, then the class can be axiomatized by a set of equations.