Hacker News new | past | comments | ask | show | jobs | submit login

Are you referring to constructivism in terms of education? Or in terms of proving the existence of an object in mathematics? Traditionally, it is not necessary to construct an object to prove its existence. One can simply assume the object does not exist and prove a contradiction. Requiring constructive proofs does not seem to provide tangible benefits, but it does unnecessarily hinder mathematical thinking.

> Requiring constructive proofs does not seem to provide tangible benefits, but it does unnecessarily hinder mathematical thinking.

Not true. I recommend Five Stages of Accepting Constructive Mathematics:


Constructivism/intuitionism seems to have culminated into modern-day finitism/ultrafinitism. In the likes of Doron Zeilberger (crank or genius - you decide).

Par for the course for computer scientists - if we had infinite time/space we wouldn't have to optimise anything.

This paper [1] by Ed Nelson presents a brilliant analysis on the difference between classical logicians and intuitionists.

It starts with a crucial distinction in semantics.

Assuming ∀x¬A and arriving at a contradiction not a proof for ∃xA.

And yet, simply on the grounds of utility, the intuitionist perspective is far more useful to me as an every-day philosophy simply because "incomplete communications" is a mental model of how human systems/interactions work and how information flows in general. That which we call knowledge is socially constructed [2] and is always incomplete.

[1] https://web.math.princeton.edu/~nelson/papers/int.pdf

[2] https://en.wikipedia.org/wiki/Constructivist_epistemology

Mathematics of course. Theorem provers work nicer with constructive mathematics.

You won't convince anyone of this until they start working heavily in a theorem prover. With constructive proofs you can introduce certain automation that is not possible otherwise; until then, when we are working on pen and paper, it is a limitation on your proof techniques.

But you are are aware of this already, I'm just writing it out.

I'm surprised by this statement. Most of the research in automatic theorem proving (including for first and higher order logics) is based on classical logic, because it's much easier to reduce to a search for false, than to try and prove an arbitrary formula. The automatic provers able to do intuitionistic proofs generally do it by encoding the intuitionistic logic into a classical logic first.

Look at these provers, they're almost all based on classical logic, and even on proofs by contradiction: http://www.tptp.org/CASC/27/SystemDescriptions.html

Even Isabelle/HOL, which is quite user friendly and has a lot of automation (like Sledgehammer, which can call to the automatic provers mentioned above) is based on classical logic with choice.

Hmm, I was more thinking about proof translation across isomorphisms. I'm not speaking from my own experience here, just that I have seen people grumble about it.


:-). I agree. Sure constructive proofs are sometimes longer, but it's the computer doing most of the work.

But you also end up with proofs that are much, much shorter.

I guess it's all about the degree of uncertainty. Constructive mathematics reduces the degree of uncertainty, which grows exponentially as you get in the higher level proofs.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact