|
|||||
|
It was time I changed the old blog style to something a bit more modern. I hope you like it. Now I just have to figure out how to port 60 blog posts from ASCIIMathML notation to something a bit friendlier that can use MathML but does not require it. What is out there? I know about jsMath. I am open to suggestions. 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 a quick tutorial on Coq. 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 coincide if they do so for Baire space. In Russian Constructivism the match between synthetic and metric topology breaks down, as even a very simple complete totally bounded space fails to be compact, and its topology is strictly finer than the metric topology. In contrast, in Brouwer’s intuitionism synthetic and metric notions of topology and compactness agree. Download paper: csms_in_synthtop.pdf The following argument is often cited as an example of the necessity of the law of excluded middle and classical logic. We are supposed to demonstrate the existence of two irrational numbers `a` and `b` such that their power `a^b` is rational. By the law of excluded middle, `sqrt(2)^(sqrt(2))` is rational or not. If it is rational, take `a = b = sqrt(2)`, otherwise take `a = sqrt(2)^(sqrt(2))` and `b = sqrt(2)`. In either case `a^b` is rational. Let us think about this for a moment, from constructive point of view. Continue reading Constructive gem: irrational to the power of irrational that is rational In the last constructive gem we studied the exponential `2^NN` and its isomorphic copies. This time we shall compute the double exponential `2^(2^NN)` 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 Cardinality of sets in constructive mathematics is not as well behaved as in classical mathematics. Cardinalities of finite sets are not natural numbers, and cardinalities are not linearly ordered. Just like in real life, constructive stones are easier to find than constructive gems, so let me start the series with a stone about constructive finite sets. In various mathematical forums, mostly those of a logical flavor, I regularly see people asking basic questions about constructive mathematics. I also see misconceptions about constructive mathematics. I shall make a series of posts, Constructive Gems and Stones, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics. A constructive gem is something nice about constructive mathematics that makes you want to know more about it. In contrast, a constructive stone is a complication in constructive mathematics which does not exist in the classical counterpart. Here we go! The first one is about finite sets. |
|||||
|
|
|||||
