Constructive mathematics and computer programming (1979) [pdf](cs.cornell.edu)
cs.cornell.edu
Constructive mathematics and computer programming (1979) [pdf]
http://www.cs.cornell.edu/courses/cs6180/2017fa/notes/week4/lecture8/Martin-Lof-ConstructiveMathematicsAndComputerProgramming
22 comments
Out of curiosity as someone less mathematically inclined but very interested in mathematics: what do you do with the equations in books like this?
Do you look at them and already intuitively know what they mean so you don't have to dig deeper? Do you slowly go over each element individually and then grasp the whole thing afterwards? Or are you so used to them that you can read them more or less the way you read English? I really want go deeper into this stuff but when I look at these books I feel like I would need years of specialized training to understand them.
Do you look at them and already intuitively know what they mean so you don't have to dig deeper? Do you slowly go over each element individually and then grasp the whole thing afterwards? Or are you so used to them that you can read them more or less the way you read English? I really want go deeper into this stuff but when I look at these books I feel like I would need years of specialized training to understand them.
Written mathematics is quite informationally dense and, in general, reads much more slowly than typical English prose. Sometimes you do have to go over an equation symbol-by-symbol; sometimes you have to convince yourself of the truth of a sentence with no symbols at all.
In this particular case, though, you're in luck, as Martin-Löf gave a less technical and more philosophical series of lectures on the same subject, which are a much easier read: http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the...
In this particular case, though, you're in luck, as Martin-Löf gave a less technical and more philosophical series of lectures on the same subject, which are a much easier read: http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the...
Disclaimer: I am a self taught pleb, not a mathematician.
The pdf blows up my phone but the first equations look like basic calculus, and the rest seem to be in the form of logical judgments where above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. I've seen Godel's T (System T) used in this style, and it seems this pdf is using set theory (again, my shit phone explodes and can't load half the pages) though I would imagine these would be done in category theory these days.
To "understand" math, (scare quotes because again, I'm just a pleb), you really need to know what field, or set of axioms, or universe you're working in. The rational numbers are the easiest imho, when you get into the reals you're dealing with mathematical objects that may not even be possible to be represented as numbers (as I understand it) so if you can understand symbolic programming ala Sussman Lisp/Scheme you can understand math just you're unfamiliar with the notation, and unfamilar with whatever the rules of this particular abstraction are, that's all. By axioms I mean somebody has merely stated "I created this universe, here are the axioms that rule this abstract universe" meaning they often will not be congruent with any kind of other fields/axioms, in my experience as a plebmatician.
If you want to understand there's a guy from here who wrote a book https://pimbook.org/ and to get into Per Martin-Löf you'll probably need some logic courses, professor Robert Harper or Frank Pfenning both have 'intuitionistic' constructivist math resources you can read/learn from if you google.
The pdf blows up my phone but the first equations look like basic calculus, and the rest seem to be in the form of logical judgments where above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. I've seen Godel's T (System T) used in this style, and it seems this pdf is using set theory (again, my shit phone explodes and can't load half the pages) though I would imagine these would be done in category theory these days.
To "understand" math, (scare quotes because again, I'm just a pleb), you really need to know what field, or set of axioms, or universe you're working in. The rational numbers are the easiest imho, when you get into the reals you're dealing with mathematical objects that may not even be possible to be represented as numbers (as I understand it) so if you can understand symbolic programming ala Sussman Lisp/Scheme you can understand math just you're unfamiliar with the notation, and unfamilar with whatever the rules of this particular abstraction are, that's all. By axioms I mean somebody has merely stated "I created this universe, here are the axioms that rule this abstract universe" meaning they often will not be congruent with any kind of other fields/axioms, in my experience as a plebmatician.
If you want to understand there's a guy from here who wrote a book https://pimbook.org/ and to get into Per Martin-Löf you'll probably need some logic courses, professor Robert Harper or Frank Pfenning both have 'intuitionistic' constructivist math resources you can read/learn from if you google.
I had exactly the same question. Until just last year. (I’m 39.)
We’re all different, especially in how we process abstract concepts. I process them quite visually. Among my friends it seems there is some correlation between having a maths degree and thinking directly in the math symbols.
What I have tried to do is just to power through. Scanning and jumping over the paper I try to construct a mental model that the equation is a blueprint for. This is this. This is that. There’s a relation here. What is it. Ah yes it’s just that here. And that is then ... yes.
Usually when i get the equation it’s much simpler than I assume at first. It’s just the ideas in a couple of paragraphs put together in an unambiguous way.
So I just kind of power through! And it can and does take some time! But once through it tends to stick. it’s quite cool.
We’re all different, especially in how we process abstract concepts. I process them quite visually. Among my friends it seems there is some correlation between having a maths degree and thinking directly in the math symbols.
What I have tried to do is just to power through. Scanning and jumping over the paper I try to construct a mental model that the equation is a blueprint for. This is this. This is that. There’s a relation here. What is it. Ah yes it’s just that here. And that is then ... yes.
Usually when i get the equation it’s much simpler than I assume at first. It’s just the ideas in a couple of paragraphs put together in an unambiguous way.
So I just kind of power through! And it can and does take some time! But once through it tends to stick. it’s quite cool.
As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research?
I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
One exciting new development is "Cubical Type Theory: a constructive interpretation of the univalence axiom" [0], a constructive version of homotopy type theory.
The "axiom of choice" in this context is not really an axiom, just a provable theorem whose proof in this setting is given by Martin-Löf. The reason, I believe, is that constructive mathematics has a different meaning for the exists (∃) quantifier. In a constructive context, existence is "stronger" since you have to specify a witness of existence; this makes the hypothesis of the "axiom" of choice stronger, allowing for a proof.
Here's a stab at a very informal version of this. Suppose you have a set composed of "slices". The "axiom" of choice says that "IF for every slice (x in A) there exists a good element of that slice (y in B_x, and 'good' is defined by satisfying property C), THEN there exists a function which takes a slice and returns a good object of that slice." But the very definition of the (constructive) word "exists" in the hypothesis means you already have to specify, as input, a way of finding one good object of each slice. With this, finding a function that provides a good object of each slice is a tautology.
[0] https://arxiv.org/abs/1611.02108
The "axiom of choice" in this context is not really an axiom, just a provable theorem whose proof in this setting is given by Martin-Löf. The reason, I believe, is that constructive mathematics has a different meaning for the exists (∃) quantifier. In a constructive context, existence is "stronger" since you have to specify a witness of existence; this makes the hypothesis of the "axiom" of choice stronger, allowing for a proof.
Here's a stab at a very informal version of this. Suppose you have a set composed of "slices". The "axiom" of choice says that "IF for every slice (x in A) there exists a good element of that slice (y in B_x, and 'good' is defined by satisfying property C), THEN there exists a function which takes a slice and returns a good object of that slice." But the very definition of the (constructive) word "exists" in the hypothesis means you already have to specify, as input, a way of finding one good object of each slice. With this, finding a function that provides a good object of each slice is a tautology.
[0] https://arxiv.org/abs/1611.02108
Thank you, this helps my understanding.
Constructivist mathematics does not depend on the axiom of choice.
That said, when you only admit a universe of mathematical objects that admit of a finite construction, it is not unreasonable that you can have a computer program that, at least in principle, will enumerate all possible constructions and proofs of statements about them. Given that, you can create a construction which is literally for each set Y, the primary x in Y is the first x which in that enumeration a statement of the form "x is in Y" is proved.
This construction give a choice function of the kind that the Axiom of Choice says exists. However that said, the bizarre consequences of the Axiom of Choice that you find in classical set theory can't be proven for other reasons.
That said, when you only admit a universe of mathematical objects that admit of a finite construction, it is not unreasonable that you can have a computer program that, at least in principle, will enumerate all possible constructions and proofs of statements about them. Given that, you can create a construction which is literally for each set Y, the primary x in Y is the first x which in that enumeration a statement of the form "x is in Y" is proved.
This construction give a choice function of the kind that the Axiom of Choice says exists. However that said, the bizarre consequences of the Axiom of Choice that you find in classical set theory can't be proven for other reasons.
Thank you for the clarification. Following up on this, I found a blog post [0] that explains why you don't get bizarre consequences like the Banach-Tarski paradox this way:
> [The constructivist method] avoids the basic problem with the axiomatic problem. You can’t have something ridiculous like the set of all sets that don’t include themselves, because the only way to show that a set exists is to show a process to create it – and there’s no way to create a paradoxical set! You don’t get nonsense like [the Banach-Tarski paradox], because the division of the spherical topological space into the non-metric subspaces is impossible: you can’t show a process that produces it. In the world of intuitionism and constructivism, existence proofs that don’t produce concrete examples don’t exist!
[0]: http://www.goodmath.org/blog/2014/08/18/the-constructivist-r...
> [The constructivist method] avoids the basic problem with the axiomatic problem. You can’t have something ridiculous like the set of all sets that don’t include themselves, because the only way to show that a set exists is to show a process to create it – and there’s no way to create a paradoxical set! You don’t get nonsense like [the Banach-Tarski paradox], because the division of the spherical topological space into the non-metric subspaces is impossible: you can’t show a process that produces it. In the world of intuitionism and constructivism, existence proofs that don’t produce concrete examples don’t exist!
[0]: http://www.goodmath.org/blog/2014/08/18/the-constructivist-r...
Read Robert Harper's blog for everything in the constructivist, type theory state of the art: https://existentialtype.wordpress.com/2018/01/15/popl-2018-t...
There's also the OPLSS lectures if you're interested: https://www.cs.uoregon.edu/research/summerschool/summer16/cu...
There's also the OPLSS lectures if you're interested: https://www.cs.uoregon.edu/research/summerschool/summer16/cu...
Martin-Löf has a whole paper on the axiom of choice in constructive mathematics: https://pdfs.semanticscholar.org/68d6/790cdbfda26cf71311e137...
For me (intuitively, conceptually and abstractly), the AC is just a particular case of Hilbert's Entscheidungsproblem.
It doesn't matter what the AC states. All that matters is that you interpret it as a proposition. And then it's sufficient to assume that some algorithm can be constructed, or some Oracle can be consulted to determine the truth-value of the proposition.
Like, for example. I can construct you an Oracle which evaluates the "Law" of Non-Contradiction as true.
https://repl.it/repls/GiftedHumiliatingProcess
This is the fundamental (only?) difference between mathematics and programming. Mathematics assumes pure functions.
It doesn't matter what the AC states. All that matters is that you interpret it as a proposition. And then it's sufficient to assume that some algorithm can be constructed, or some Oracle can be consulted to determine the truth-value of the proposition.
Like, for example. I can construct you an Oracle which evaluates the "Law" of Non-Contradiction as true.
https://repl.it/repls/GiftedHumiliatingProcess
This is the fundamental (only?) difference between mathematics and programming. Mathematics assumes pure functions.
I think you have it backwards? From a mathematical perspective, the constructivist framework is defined as "provable without the axiom of choice." Constructivists are very concerned with avoiding the axiom of choice.
You're right. Wikipedia mentions that Voevodsky's model is considered to be non-constructive since it uses the axiom of choice in an ineliminable way.
> The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory.
I'm getting confused because Martin-Lof writes at the end of this paper:
> I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice...
Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.
> The problem of finding a constructive interpretation of the rules of the Martin-Löf type theory that in addition satisfies the univalence axiom and canonicity for natural numbers remains open. A partial solution is outlined in a paper by Marc Bezem, Thierry Coquand and Simon Huber[17] with the key remaining issue being the computational property of the eliminator for the identity types. The ideas of this paper are now being developed in several directions including the development of the cubical type theory.
I'm getting confused because Martin-Lof writes at the end of this paper:
> I shall construct an object of this type, an object which may at the same time be interpreted as a proof of the axiom of choice...
Thus (Az)((..tx)p(z(x)), (lx)q(z(x))) is the sought for proof of the axiom of choice.
I'm confused then because the paper linked in the OP states:
> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]
> The true source of uncomputeable functions is not the axiom if choice (which is valid intuitionistically) but the law of the excluded middle and indirect proof [emphasis original]
It is choice in constructible mathematics: something “totally different” from “zf” choice. Existence means “can construct”, essentially. There are “less” things in constructible mathematics than in zf.
This is a rough explanation.
Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today.
I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper. https://lamport.azurewebsites.net/tla/tla.html
I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper. https://lamport.azurewebsites.net/tla/tla.html
Nah, no! Leslie Lamport is quite far away from constructive mathematics. You will for example see his explanation of logic in the TLA+ video lectures is entirely classical.
Thanks, I'll copy this to my tablet so I can carry it around with me.
Looking forward to being impressed (hopefully) that it is still relevant today.
Looking forward to being impressed (hopefully) that it is still relevant today.
That paper is still the future, it looks like to me.
Few years ago I joined some metaphysical dots between "construction", "constructivism", "creation" and "creationism" in my head, which is what led me on to explore 100 years of history/theory behind computational trinitarianism, intuitionistic logic, Curry-Howard isomorphism etc.
This conceptual understanding of Monist metaphysics was the end of my militant atheism.
The expression of knowledge is the creation of knowledge.
It pleases me to see that Per Martin-Löf joined the same dots in his paper "A path from logic to metaphysics".
This conceptual understanding of Monist metaphysics was the end of my militant atheism.
The expression of knowledge is the creation of knowledge.
It pleases me to see that Per Martin-Löf joined the same dots in his paper "A path from logic to metaphysics".
Here’s more: https://github.com/michaelt/martin-lof
Here’s another one - this one is wonderful: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo...
As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory
Intuitionism in math is beautiful imo: https://en.wikipedia.org/wiki/Intuitionism