|
|||||
|
With Peter LeFanu Lumsdaine. Abstract: The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not [...] I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$. Continue reading Constructive gem: an injection from Baire space to natural numbers As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together. Using Berardi-Bezem-Coquand functional, or alternatively, for giving a [...] Jens Blanck and I presented a paper at Computability and Complexity in Analysis 2009 with a complicated title (I like complicated titles):
which has been published in Volume 16, Issue 18 of the Journal of Universal Computer Science. I usually just post the abstract, but this time I would like to explain the general idea informally, the way one can do it on a blog. But first, here is the abstract: Abstract: We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others. Download paper: effalg.pdf or directly from JUCS I think I am getting addicted to Coq, or more generally to doing mathematics, including the proofs, with computers. I spent last week finalizing a formalization of Gödel’s functional interpretation of logic, also known as the Dialectica interpretation. There does not seem to be one available already, which is a good opportunity for a blog post. Already a while ago videolectures.net published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also gave [...] With Davorin Lešnik. Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces [...] In the last constructive gem we studied the exponential $2^\mathbb{N}$ and its isomorphic copies. This time we shall compute the double exponential $2^{2^\mathbb{N}}$ and even write some Haskell code. Continue reading Constructive gem: double exponentials Constructive gems are usually not about particular results, because all constructive results can be proved classically as well, but rather about the method and the way of thinking. I demonstrate a constructive proof which can be reused in three different settings (set theory, topology, computability) because constructive mathematics has many different interpretations. I promise I will post a constructive gem soon. This constructive stone came up as a reaction to the cardinality of finite sets stone. I show that inhabited sets of natural numbers need not have minima, constructively. Continue reading Constructive stone: minima of sets of natural numbers |
|||||
|
|
|||||
