Timeline for Contrasting theorems in classical logic and constructivism
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 11, 2021 at 19:27 | history | made wiki | Post Made Community Wiki by Stefan Kohl♦ | ||
| Aug 26, 2020 at 7:43 | comment | added | Andrej Bauer | It is "essentially known" that the vast majority of mathematics is constructive, or can be constructivized. Specifically, there should be no trouble with one-point compactifications. You're a bit off there with HA and PA, as those are not strong enough to talk about analysis. You'd want a richer formalism. | |
| Aug 26, 2020 at 4:12 | comment | added | Turbo | @AndrejBauer In Riemannian geometry we add a point at infinity to compactify the plane. Is it known that proofs that essentially utilize compacitification are non-constructive and cannot be constructivized? That is there is no proof in the sense that HA cannot prove it but PA can if we cannot avoid compactification? | |
| Mar 30, 2020 at 16:19 | comment | added | Andrej Bauer | If you want to do classical analysis, then it's best to use classical logic. You can do classical analysis constructively, but it will be clumsy and unnatural. The situation is symmetric: you can do constructive math in classical logic by "simulating" then using models, but that's a lot of overhead. | |
| Mar 30, 2020 at 16:16 | comment | added | Andrej Bauer | Perhaps a reasonable analogy can be take from topology: let $R_d$ be the reals with the discrete topology and $R_e$ the reals with Euclidean topology. The identity map $\mathrm{id} : R_d \to R_e$ is a continuous injection, so $R_d$ is a "subspace" of $R_e$ (not what topologists would say). It's this sort of thing that's going on. | |
| Mar 30, 2020 at 7:38 | comment | added | Monroe Eskew | @AndrejBauer Is this the right way to understand it? If you want to treat classical analysis (or just undergrad calculus) in a way that doesn’t diverge too dramatically from common notions, but is still faithful to constructivism, then you do a kind of calculus of partial functions, where the domains tend to shrink as you introduce more information about the definitions of the functions. So classical analysis is about “something” that is just a lot harder to describe from the constructivist standpoint? | |
| Mar 29, 2020 at 22:38 | comment | added | Andrej Bauer | @BenCrowell: I think physicists tend to use something closer to nilpotent infinitesimals of synthetic differential geometry (SDG), rather than non-standard analysis. They say things like "we may ignore $dx^2$", which directly translates to "$dx$ is a square-nilpotent" in SDG. (Of course, there's still a lot of similarity with non-standard analysis.) | |
| Mar 29, 2020 at 22:34 | comment | added | Andrej Bauer | @BenCrowell: I think your criticism is not entirely fair. Of course one can never draw a completely accurate graph of a discontinuous function – but the same holds for any graph, because pencils are not infinitely thin. As Monroe says, it's better to just bite the bullet and try to understand how it's possible to have a proper subset $D \subseteq \mathbb{R}$ such that $\mathbb{R} \setminus D = \emptyset$. Once you get over that hurdle, a lot fo constructive math starts to make more sense. | |
| Mar 29, 2020 at 22:31 | comment | added | Andrej Bauer | @MonroeEskew: a piecewise continuous map, say $f(x) = \mathsf{if}\; x < 0 \;\mathsf{then}\; 0 \;\mathsf{else}\; 1$ has as its domain the set $D = \{x \in \mathbb{R} \mid x < 0 \lor x \geq 0\}$. The strange thing is, that constructively $D$ is a proper subset of $\mathbb{R}$, even though $\mathbb{R} \setminus D = \emptyset$. It's a phenomenon that is difficult to explain classically. It's not that $D$ has fewer points than $\mathbb{R}$. Rather, the points of $D$ have more information. Each point of $D$ comes with information on whether it is negative or non-negative. | |
| Mar 29, 2020 at 16:32 | comment | added | user21349 | [Physicists] don't have the necessary formal training to use [infinitesimals] properly (because they were taught ϵδ proofs), but they rely on their intuitions quite reliably. The type of reasoning you see in these calculations is all first-order logic, so it's correct by the transfer principle, or can be made so by trivial changes such a changing "neglecting $dx$..." to "taking the standard part..." | |
| Mar 29, 2020 at 16:27 | comment | added | user21349 | What would you say to the typical high school math teacher who says many of these statements can be disproven by drawing a picture? You can't really draw a discontinuous, total function, for example. No matter how accurately you try to draw it, you'll either leave a gap in the domain or make the pieces overlap, so that it's not a function. They are so antithetical to geometric and physical intuition. My physical intuition differs from yours. My physical intuition is that any time I see a discontinuous function, it's an idealized mathematical fiction, not physical reality. | |
| Mar 29, 2020 at 11:13 | comment | added | Monroe Eskew | It seems like you have to bite the bullet. A lot of things I can draw on the board that are usually meant to represent geometrical shapes or functions on $\mathbb R$ cannot represent the “real” mathematical things according to constructive math (i.e. discontinuous but piecewise continuous functions, or anything inducing such a function like a Euclidean shape). Pedagogically this sounds like a nightmare. Or maybe if people are interested in studying things corresponding to “classical” intuition, then you have to convince them to study finitary surrogates for those? | |
| Mar 29, 2020 at 9:40 | comment | added | Andrej Bauer | Just briefly, here is an alternative high-school explanation of why all maps are continuous: motion is continuous, obviously, since if I want to get from $A$ to $B$ I cannot just teleport (despite many sci-fi movies). Therefore, all functions $\mathsf{Time} \to \mathsf{Space}$ are continuous. We can also have teleportation, but then we need to modify $\mathsf{Time}$ to account for it. | |
| Mar 29, 2020 at 9:35 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
spelling
|
| Mar 29, 2020 at 9:33 | comment | added | Andrej Bauer | And by the way, it's not always about logic and foundations. One can change define "space" (in ZFC) in such a way that Banach-Tarski goes away and all subspaces of $\mathbb{R}$ are measurable, and the definition is arguably simpler than the usual definition of topological space (but of course one needs to get used to it, as is usual with new math). See for instance this paper by Alex Simpson. | |
| Mar 29, 2020 at 9:28 | comment | added | Andrej Bauer | Perhaps the closest we get in practice to alternative geometric intuitions is when engineers and physicsts, despite having been taught $\epsilon\delta$ proofs, insist on using infinitesimals. They don't have the necessary formal training to use them properly (because they were taught $\epsilon\delta$ proofs), but they rely on their intuitions quite reliably. | |
| Mar 29, 2020 at 9:27 | comment | added | Andrej Bauer | They are only antithetical to geometric and physical intuition under one understanding of "space" and "continuity" – the one you are aware of. It is entirely possible to develop different kinds of intuition (speaking from first-hand experience and having taught PhD students the alternatives) that let you "internalize" these statements. So, it's really the high-school teachers who determine what kind of intuitions the young minds will develop. In the current educational system there is only one kind. The resulting uniformity of thought gives the illusion of absolute truth. | |
| Mar 29, 2020 at 5:44 | comment | added | Monroe Eskew | What would you say to the typical high school math teacher who says many of these statements can be disproven by drawing a picture? They are so antithetical to geometric and physical intuition. | |
| Mar 28, 2020 at 23:23 | comment | added | Andrej Bauer | Oh, there's another topos (a model of intuitionistic bounded Zermelo set theory) that would interest applied mathematicians. In it all maps are differentiable and nilpotent infinitesimals exist, so you get to do analysis engineering-style, with $dx$'s and $dy$'s that are very small and whose squares are negligible. | |
| Mar 28, 2020 at 23:18 | comment | added | Andrej Bauer | I don't think they know about them, or at least I never got a reaction. There's a positive side to all of this, too. For example, in the effective topos everything is computable (in a precise sense). I'd imagine at least some applied mathematicians would appreciate that. In general, I find computer scientists will take anything that helps them solve their problems, even if it's outrageous. Mathematicians are more hung up on value judgements and respecting traditions. | |
| Mar 28, 2020 at 22:14 | comment | added | Monroe Eskew | What do the applied mathematicians say about these outrageous statements? | |
| Mar 28, 2020 at 16:31 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 85 characters in body
|
| Mar 28, 2020 at 16:13 | history | answered | Andrej Bauer | CC BY-SA 4.0 |