The weird and wonderful world of constructive mathematics (2017) [pdf]
home.sandiego.edu
home.sandiego.edu
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.
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?
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).
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.
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.
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.
- An upper bound N on the size of the set.
- A surjection f:[1,N] -> S where [1,N] is the set of integers from 1 to N.
- Proof by induction that every set S where the above two ingredients can be found is decidable. The induction will be in N. This can be carried out internally in any intuitionistic system.
In the case of SHA-256, there is an upper bound N on the number of 256-bit inputs (which is equal to 2^256), and a surjection f which maps integers to corresponding bitstrings. Then the general lemma I described above is true, and you can prove that there must be a collision.
It doesn't entirely prove you wrong. (I need to do some real work). But almost certainly what you describe can't work. Some sort of induction will probably thwart what you're trying to do.
In this case, the point is that in a logic for cryptography, you would have a type "S" of "bit strings of arbitrary but unknown length" which is restricted in such a way that you cannot eliminate into discrete types (such as the natural numbers). In particular, there would be no way of proving "x != y" for x, y in S at all unless you assume that there was some function which established this.
One way to get a model for such a logic is to interpret types as (reflexive) graphs and functions as graph homomorphisms. The resulting category is a topos and hence gives you a model of type theory.
There is such a wealth of knowledge about building models for intuitionistic logic that it is difficult to say what can and cannot be done without a thorough literature review.
I don’t understand how it is possible to have such an axiom. Why can you not construct the function $f : x \mapsto I(x > 2)$ where $I$ is 1 for true, 0 for false. And then prove that the preimage of $(-1,0.5)$ is $(-\infty,2]$ which is not open?
In your case it is not provable that (x > 2 or x =< 2), that would require exactly the law of the excluded middle.
This is explained in one of the later slides.
Does it break down somewhere in the definition of continuity?
It's not the existence of the set of "smooth reals" that square to 0 without being 0 that creates the universe in which every geometric object is infinitesimally straight.
Rather, for any ring of "smooth reals" R, the set D={d in R:^2=0} allows us to construct a "dual ring" as follows. First, take the map RxR -> R^D sending a pair (a,b) of "smooth reals" to the linear function D->R given by d|->a+bd. Then induce a ring structure on RxR that would make the map into a ring homomorphism when R^D, the set of R-valued functions on D, is given the pointwise ring structure.
Explicitly, (a_1,b_1)+(a_2,b_2)=(a_1+a_2,b_1+b_2) since (a_1+b_1d)+(a_2+b_2d)=(a_1+a_2)+(b_1+b_2)d, and (a_1,b_1)(a_2,b_2)=(a_1a_2+a_1b_2+a_2b_1) since (a_1+b_1d)(a_2+b_2d)=a_1a_2+(a_1b_2+a_2b_1)d+d^2b_1b_2 and d^2=0.
Thus, we have the structure of a ring on the set of RxR, which is tradtionally denoted by R[e] where e(psilon) is a variable x assumed to square to zero, i.e. an indeterminate, so hypothetical, order 2 infinitesimal.
Now, Axiom 1 of synthetic differential geometry asserts that the map sending the ring of dual numbers to the ring of R-valued functions on D is a bijection. In other words, it restricts the domain of discourse so that, when it comes to functions on order 2 infinitesimals, we may only ever talk linear functions, and it also expands the discourse in requiring that we have distinct linear functions, one for every pair y-intercept,slope pair.
It is the second bit that forces every geometric object to admit "infinitsimally straight" approximations, because every geometric object is essentially contained in a copy of R^n (n-tuples of "smooth real numbers"), and so it is forced to have non-trivial linear functions from D.
---
One reference for the relationship to the dual numbers is the first few pages of Anders Kock's book Synthetic Differential Geometry, available from his web-site at home.imf.au.dk/kock/sdg99.pdf. Another, more readable reference, are Mike Shulman's notes available at http://home.sandiego.edu/~shulman/papers/sdg-pizza-seminar.p....
And if you are already taking P!=NP as an axiom, what difference it makes that constructivism takes out just another axiom that you assume to be true?
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.
Generally speaking, the ability to extended intuionistic mathematics by new axioms that are classically inconsistent is a bit of a misnomer. The real power is that these "axioms" allow you to easily and immediately specialize the generic language of intuionistic mathematics into a domain-specific language for various areas.
So that
1. adding the continuity axiom gives you a domain-specific language which can only describe continuous functions and no others
2. adding the differentiation axiom gives you a domain-specific language called synthetic differential geometry in which you can only talk about differentiable functions
3. adding the computability axiom gives you a domain-specific language in which you can only talk about computable functions.
4. adding the law of the excluded middle gives you the domain-specific language of classical mathematics.
Now, each of the first three can also be interpreted within classical mathematics (which is how we know the extensions are consistent with classical mathematics), but that's analogous to writing an interpreter in C versus merely adding new syntax to an existing language (e.g. how DSLs can be implemented in LISP).
>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.)
Well, yes, exactly. The thing that intrigues me about this discussion is that it seems like mathematicians have a much clearer idea than I do about what the differences between these kinds of abstractions are.
Let me highlight again that the question isn't whether they are useful, or a mathematically valid construction; there are all kinds of other mathematically valid constructions far stranger than the "reals". The question is whether they deserve such a fundamental place in mathematics and education. I do recall even in high school that truly understanding the real numbers even at that level was definitely a dividing point for the advanced math class; there are some who really got the quirks, and there are some who never really did and just parroted their way through the tests wondering how the question of "numbers" got so complicated... and it was still a very partial and somewhat ad-hoc introduction to the topic ("Dedekind" doesn't come up, etc.) just enough to try to motivate limits.
Though addition might not be defined on some of the reals, if represent it like that.
But Proof checkers like lean/coq all use Cauchy sequences to represent reals. So they are in effect constructible.
I'm not sure if this answer is relevant, but might as well mention it.
[0] 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) which has been present in Western philosophy since Aristotle through Kant, Hegel and Marx (it's a funny story).
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.
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...
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
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.
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.
Adjoints are everywhere [1]. Referencing adjoints is indeed pretty vague. You can't make a case for why things are interesting by quoting a bunch of resources of other people making cases why things are interesting. (I guess you can, but then, why make the argument at all if it is not yours?)
You don't even need funny names to get x^2=0. This is true for any of the two elements of the group of order 2.
Linear logic is indeed having a mini revival, but so is general category theory. I don't see the particular advantage for people to evangelise certain parts of mathematics, especially if the case being made is not clear.
[1] Not attributed to me.
That’s like your opinion, man.
You conveniently ignored the continousness of both constructive mathematics and Lie groups.
Did you read the paper on chu spaces and constructive mathematics? What did it say about adjoints?
That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.
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.
This sweeping assumption leads to my sweeping assumption that you are "a programmer".