Sheaf Semantics in Constructive Algebra and Type Theory

Abstract

In this thesis we present two applications of sheaf semantics. The first is to give constructive proof of Newton-Puiseux theorem. The second is to show the independence of Markov's principle from type theory.

In the first part we study Newton-Puiseux algorithm from a constructive point of view. This is the algorithm used for computing the Puiseux expansions of a plane algebraic curve defined by an affine equation over an algebraically closed field. The termination of this algorithm is usually justified by non-constructive means. By adding a separability condition we obtain a variant of the algorithm, the termination of which is justified constructively in characteristic 0. To eliminate the assumption of an algebraically closed base field we present a constructive interpretation of the existence of the separable algebraic closure of a field by building, in a constructive metatheory, a suitable sheaf model where there is such separable algebraic closure. Consequently, one can use this interpretation to extract computational content from proofs involving this assumption. The theorem of Newton-Puiseux is one example. We then can find Puiseux expansions of an algebraic curve defined over a non-algebraically closed field K of characteristic 0. The expansions are given as a fractional power series over a finite dimensional K-algebra.

In the second part we show that Markov's principle is independent from type theory. The underlying idea is that Markov's principle does not hold in the topos of sheaves over Cantor space. The presentation in this part is purely syntactical. We build an extension of type theory where the judgments are indexed by basic compact opens of Cantor space. We give an interpretation for this extension of type theory by way of computability predicate and relation. We can then show that Markov's principle is not derivable in this extension and consequently not derivable in type theory.