9 ms·
The weird and wonderful world of constructive mathematics (2017) [pdf]
- adamnemecek 8y agoConstructive mathematics is the way forward. It's connected to linear logic via Chu spaces [0] (https://arxiv.org/abs/1805.07518 https://arxiv.org/abs/1805.07518). This correspondence is unreal as constructive mathematics / linear logic unlocks the door to several key advantages such as being closer to computation, probability theory, type theory, Lie groups, a generalized topology, optimization, “differentiable Turing machines”, all the quantum shit, game theory etc the list goes on. [0] https://en.wikipedia.org/wiki/Chu_space https://en.wikipedia.org/wiki/Chu_space Linear logic is fundamentally about formulating computation as an adversarial relationship between two parties. It's also the foundation of e.g. the Rust ownership system (I know, I know, affine types). It's also the foundation of the min-max algorithm which in turn is the foundation of Generative adversarial neural networks. Ironically, this idea isn't exactly new. It's directly related to Dialectics (https://en.wikipedia.org/wiki/Dialectic https://en.wikipedia.org/wiki/Dialectic) which has been present in Western philosophy since Aristotle through Kant, Hegel and Marx (it's a funny story).
- gbhn 8y agoInteresting! Do you have a book on the subject to recommend?
- adamnemecek 8y agoRead the wiki on every term you aren't familiar with and then do pairwise google searches for papers containing any two of the words in the set, so e.g. "probability" "Lie groups". If you have specific question I can maybe answer them or provide a link at least.
- aportnoy 8y agoNo offense, but that is really handwavy. In what way does constructive mathematics unlock the door to being closer to all the quantum shit?
- adamnemecek 8y agoAsk specific questions. Like I have a papers backing up most of my claims. Sometimes you need to take a leap of faith but you don’t need to draw every line in the connect the dot puzzle to see that it’s a fucking elephant. https://arxiv.org/pdf/0805.2859.pdf https://arxiv.org/pdf/0805.2859.pdf Page 14. But do a google search “constructive mathematics” “quantum” or “linear logic” “quantum”, a lot has been written.
- fmap 8y agoI am not sure what the parent meant specifically, but yes, there is quite a lot of work on quantum physics and logic, with regular conferences (https://arxiv.org/html/1701.00242 https://arxiv.org/html/1701.00242) and some truly fascinating models for intuitionistic logics (https://arxiv.org/abs/0909.3468 https://arxiv.org/abs/0909.3468). Not being a physicist I have no idea whether this is "the way forward" for quantum physics or anything, but the results that I do understand are non-trivial so there seems to be something there...
- joppy 8y agoHow is constructive mathematics closer to Lie groups than regular mathematics? From what I read in that presentation, a bunch of basic assumptions in calculus (such as the intermediate value theorem) no longer hold, and the theory of Lie groups is built on manifolds/calculus/real analysis etc.
- adamnemecek 8y agoGood question. I don’t have a direct answer answer but fundamentally the connection has something to do with adjoints. Google for adjoints and constructive mathematics and Lie groups and adjoints. This particular pair I understand only indirectly, I somewhat understand the relationship between linear logic and Lie groups and constructive mathematics and linear logic and this is a transitive relationship. Edit: in the presentation they mention “In constructive mathematics, there can also be numbers† d such that d^2 = 0 but not necessarily d = 0.”. They are talking about alternarivity, one of the three requirements for a Lie algebra https://en.m.wikipedia.org/wiki/Lie_algebra https://en.m.wikipedia.org/wiki/Lie_algebra
- joppy 8y ago“Something to do with adjoints” is hopelessly vague, and what do you mean by transitive? In regular mathematics there can be nonzero numbers whose square is zero (for example, the “dual numbers”). But I don’t see how this has anything to do with constructive vs nonconstructive mathematics.
- adamnemecek 8y ago> hopelessly vague, You didn’t do the reading so hold your horses with hopelessly. From the slides “In constructive mathematics, every function is continuous”. (From the presentation) Sounds like Lie groups to me. I’m aware of dual numbers funny that you bring them up as they correspond to Lie groups. I have been talking about dual quaternions nonstop on hn.
- mikorym 8y ago
- yantrams 8y agoI started teaching myself Racket recently and eventually ended up looking into the innards of lambda calculus formalism. It got me thinking about what the ramifications of embracing constructivism would be towards computability in general. Can you recommend any good introductory literature on constructivism ? I'm familiar with the foundational crisis and the whole formalism vs logicism vs constructivism debate but never really dug deeper. Thanks.
- adamnemecek 8y agoI would recommend starting with linear logic to be honest. Logic is very simple to understand, mathematics is hard. Analogously, linear logic is simpler than constructive mathematics. https://johnwickerson.github.io/talks/linearlogic.pdf https://johnwickerson.github.io/talks/linearlogic.pdf I know this might not be what you were looking for but to be honest Linear logic is the simplest to understand of all of these. I’m still struggling with these ideas, but all the signs are pointing towards this being the case.
- deleted 8y ago[deleted]
- mikorym 8y ago> Constructive mathematics is the way forward. This sweeping assumption leads to my sweeping assumption that you are "a programmer".
- adamnemecek 8y agoDid you read the presentation? Did you read this? http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-... No, you are just closing your eyes and clinging to the sense of security that mathematics claims to provide. Your comment wasn’t very specific and concentrated in the peripheral part of my claim rather than the central.
- cscurmudgeon 8y agoDid you read this? https://www.jstor.org/stable/30226269?seq=1#page_scan_tab_contents https://www.jstor.org/stable/30226269?seq=1#page_scan_tab_co...
- adamnemecek 8y agoI’m just reading it but I disagree as would most mathematicians.
- cscurmudgeon 8y agoAmazing that you are just reading but already know what most mathematicians think about it :) Realistically and honestly, most mathematicians agree with it. Most mathematicians consider constructivism to be useful AND a subset of normal mathematics. Also, it intellectually pains me to see proofs of meta theorems in intuitionistic logic use classical logic (not talking about object level proofs).
- alimw 8y agoPrevious discussion :) https://news.ycombinator.com/item?id=17641789 https://news.ycombinator.com/item?id=17641789
- adamnemecek 8y agoWhat about it?
- vladsotirov 8y agoThe remarks on computable and continuous functions can also be thought about as follows. The law of the excluded middle is only one non-constructive aspect of classical mathematics. Dropping it leaves you with what is usually called "intuionistic logic", and the characterization of constructive mathematics as broader than classic mathematics is literally correct in that every intuionistic theorem implies a classical theorem, and every classical theorem is equivalent to an intuionistic theorem. Another non-constructive aspect of classical mathematics, which remains non-constructive in intuionistic logic, are axioms whose conclusion involves the existential quantifier. In both classical and intuionistic logic, the inference rule, which governs how the existential quantifer may be used, looks as follows. > Asserting that "the existence of x such that phi(x) holds entails psi" where x is a variable bound by the existential quantifer and not occurring in psi, is equivalent to assering that "phi(y) entails psi" where y is a free variable not ocurring in psi. This inference rule (assembly language of logic) seems weird, so an example of its use might help. > "there exists x such that phi(x) holds entails that there exists x such that phi(x) holds" by tautological inference, and by the existential quantifier inference we have that "phi(y) entails the existence of x such that phi(x) holds" where y is a free variable not appearing in "exists x such that phi(x) holds". When doing classical or intuionistic mathematics, you would usually use axioms of the form "psi entails that there exists x such that phi(x) holds". But such axioms are non-constructive because the inference rule does not allow you to start with "there exists x such that phi(x) holds" and somehow construct an actual term t such that phi(t) holds. Now what Mike says in his slides is that it is consistent to modify intuionistic mathematics into a "fully constructive mathematics" by strengthening the existential quantifier so that "exists x such that phi(x) holds" would imply that we can (computably) come up with a specific term t such that phi(t) holds. As a consequence, any statement in fully constructive mathematics involving the existential quantifier as a conclusion is a stronger statement than such in classical mathematics, which is roughly why all functions end up being continuous: the definition of the notion of a function itself requires that the function be computable, i.e. that its values exist in the sense of the strengthened existential quantifier.
- tomsmeding 8y ago> every classical theorem is equivalent to an intuionistic theorem. I understand that every intuitionistic theorem implies a classical one: give the same proof, and see what theorem you end up with in the classical world. But how is every classical theorem equivalent to an intuitionistic one? Can we construct the equivalent intuitionistic theorem in a similar way from any classical one, or is this a nonconstructive proof?
- trhway 8y agothe constructive mathematics reminds me the state of math before calculus, i.e. Achilles and turtle. Such step back in power and expressiveness is probably a necessary first step before the some kind of "closure" technique, like the limit in calculus, can be developed.
- laichzeit0 8y agoAlways see this type of slide template used in mathematics. What do people use to build these slides? Is it a specific powerpoint template?
- joppy 8y agoIt’s called Beamer, which is a LaTeX template/package which generates a PDF slideshow rather than an academic-looking paper.
- deleted 8y ago[deleted]
- currycurry16 8y agoBeamer LaTeX. Here is a nifty overview: https://hartwork.org/beamer-theme-matrix/ https://hartwork.org/beamer-theme-matrix/
- dooglius 8y ago> we can assume powerful axioms that would classically be inconsistent Where could I find some explicit examples of this being useful? One idea I had is that this might actually be very useful for proving things about cryptography. Generally, if you want to formally prove something is cryptographically sound, you can only do so in terms of the asymptotics of families of functions, rather than proving anything specific regarding, say, SHA256. But if you could prove constructively a statement like (an adversary can break program P) -> (exists x,y: x != y and SHA256(x)=SHA256(y)) it seems that would serve as a proof that P is secure. Statements of this form are trivially provable classically since (exists x,y: x != y and SHA256(x)=SHA256(y)) can be proven on its own by the pigeonhole principle, regardless of the correctness of P, but it seems that in order to prove this constructively you would actually have to find a collision in SHA256.
- contravariant 8y agoI don't think you'll find much use for it when reasoning about a specific computable hash function because there's e.g. no clear distinction between using the pingeonhole principle and using the properties of the hash function itself. You could however reason about a 'generic' hash function and show that a particular program can only be broken if someone can find a hash collision. That doesn't really require constructionist reasoning though.
- man-and-laptop 8y agoNo. If a set A is finite, its elements are enumerable, and some property P is decidable, then (\forall x \in A) P(x) \vee ~P(x) is true even intuitionistically. A list of examples of "anti-classical" axioms: - All functions are continuous, and all sets automatically carry the "right" topology. This means, for instance, that constructing the Real numbers in the standard ways (Cauchy sequences or Dedekind cuts) also endows them with the desired topology (the Euclidean topology in this case). - All functions are computable. This axiom is called "Church's thesis". It's nice because it shows that a lot of Computability Theory is similar to classical set theory, but with the edition of Church's thesis, and the absence of LEM. - Some numbers in a set called the "smooth reals" square to 0... without being zero. This seems to create a universe in which every geometric object is "infinitesimally straight". I haven't fully grasped why this works. It's like the dual numbers, but somehow made all-pervasive.
- User23 8y agoWell I guess nearly all of the reals must not exist since we can't construct them.
- logicchains 8y agoBingo! From a computational perspective, the non-computable reals are objects that not only require an infinite amount of memory to represent a single one, but also require an infinite amount of memory to even describe an algorithm to produce a single one. How could such an object possibly be constructed?
- Koshkin 8y agoThe real numbers, infinity, etc. are abstractions. Being able to think abstractly is one of the things that make the humans different from other animals.
- sevensor 8y agoSo from that point of view, where the real numbers exist in the same way infinity exists -- they're not really numbers but ideas about numbers. Pi isn't a number but an idea about the circle, which isn't a shape but an idea about shapes. Is that where constructive math takes you? This is all quite fascinating but totally unfamiliar to me.
- Retra 8y agoThey can be numbers and abstractions. There's not really any definitive singular notion of what a number is, so it wouldn't be very useful to say something like pi isn't a number. (If you can do arithmetic on it, chances are it is a number, regardless of what else it represents)
- Koshkin 8y agoIndeed, numbers are abstractions. Even the number ‘5’ is an abstraction, let alone the numbers that cannot even be measured precisely - not even in principle. >idea about a circle As if a circle is a real thing. (Circles do not exist, either - or, rather, they ‘exist’ in a very particular sense of the word, as they are themselves abstractions; round things do.)
- jimhefferon 8y agoThere are a lot of folks here asking for a bit more. Here are two versions of the same well-done talk, from Andrej Bauer: a video https://www.youtube.com/watch?v=21qPOReu4FI https://www.youtube.com/watch?v=21qPOReu4FI, and a paper http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-... (sorry, the paper link may not work for everyone, but the video contains basically the same content.)
- ulucs 8y agoI’m a bit confused about the functions always being continuous. Step functions being ill-defined makes sense, but how about modulos? f(x) = x mod 1 should be trivially discontinuous. I should also be able to contruct the set of integers Z (using the unit 1 and succession operator) and identify the largest integer that is smaller than x by intersecting [x-1, x) with Z. Do I need to show the intersection always contain only one element?
- deleted 8y ago[deleted]
- alimw 8y agoI think your definition depends on being able to decide for every real x whether n ∈ [x-1, x), for which you need that n < x. According to the slides that is not generally possible in constructive mathematics.
- knappa 8y agoWell, x mod 1 is just x minus a series of Heaviside step functions, each of which are non-constructive. The core problem is determining if your real number x is equal to an integer. You might be able to prove that x is close to a particular n, but there may not be a constructive proof of either x<n, x=n, or x>n. Hence you don't know if x mod 1 should be x-(n-1) or x-n.
- andrewla 8y ago> In constructive mathematics, there can also be numbers d such that d^2 = 0 but not necessarily d = 0. In the footnote, it mentions that d is not a real number (which seems right). But I find this very confusing -- this seems to be using a deliberately non-constructible number to facilitate proofs in constructive mathematics? Regardless of whether this meets a formal criteria for being a tool in constructive mathematics, it does seem to be in direct opposition to the notion of intuitionalist mathematics, which has as a fundamental goal to dispense with axiom-of-choice-style proofs of things that are clearly ridiculous (like Banach-Tarski).
- xelxebar 8y agoWe can explicitly construct such numbers using 2x2 matrices. These are called "dual numbers"[0], and the matrix representation is essentially an analoge of the same for complex numbers. So if you accept the complex unit, i, as a reasonable algebraic thing, then the "dual unit" shouldn't be too much of a stretch. Anyway, all that is completely fine in standard foundations. The LEM contradictions only come in when we impose other axioms. For example, in Anders Kock's Sythetic Differential Geometry[1], we essentially start out by assuming that every function is differentiable. This seems sorta crazy at first blush, and it does give contradictions, but the interesting bit as that those problems hinge solely on LEM. Thus, in a way, we're left with chosing between universal differentiability or LEM. Kock explores what happens if we pick the former, and it turns out to be pretty deep, interesting and useful. [0]:https://en.wikipedia.org/wiki/Dual_number https://en.wikipedia.org/wiki/Dual_number [1]:http://home.imf.au.dk/kock/sdg99.pdf http://home.imf.au.dk/kock/sdg99.pdf