Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Constructive mathematics and computer programming (1979) [pdf]

cs.cornell.edu

Post reply on HN
Print view View original

11–20 of 23 posts

Re: Constructive mathematics and computer programming (1979) [pdf]

#11

Post by btilly »

ex3xu wrote: post #5

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 thi…

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.

Re: Constructive mathematics and computer programming (1979) [pdf]

#12

Post by intuitionist »

ex3xu wrote: post #5

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 thi…

Martin-Löf has a whole paper on the axiom of choice in constructive mathematics: https://pdfs.semanticscholar.org/68d6/790cdbfda26cf71311e137...

Re: Constructive mathematics and computer programming (1979) [pdf]

#13

Post by pfortuny »

tines wrote: post #10
ex3xu wrote: post #8

Earlier quoted context omitted.

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 a…

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]

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.

Re: Constructive mathematics and computer programming (1979) [pdf]

#14

Post by ex3xu »

btilly wrote: post #11
ex3xu wrote: post #5

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 thi…

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 p…

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...

Re: Constructive mathematics and computer programming (1979) [pdf]

#16

Post by auggierose »

r00tanon wrote: post #3

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

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.

Re: Constructive mathematics and computer programming (1979) [pdf]

#17

Post by ukj »

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".

Re: Constructive mathematics and computer programming (1979) [pdf]

#18

Post by ukj »

ex3xu wrote: post #5

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 thi…

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.

Re: Constructive mathematics and computer programming (1979) [pdf]

#19

Post by jhedwards »

AnthonBerg wrote: post #2

Per Martin-Löf writes so beautifully. 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…

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.

Re: Constructive mathematics and computer programming (1979) [pdf]

#20

Post by intuitionist »

jhedwards wrote: post #19
AnthonBerg wrote: post #2

Per Martin-Löf writes so beautifully. 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…

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 Engli…

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...

Post reply on HN