Comment by ocfnash | Hacker News Reader

Comment by ocfnash | Hacker News Reader

For a long time, I used to dismiss intuitionism but more recently I've come to find it an attractive standpoint.

For one thing, you really only gain by trying to be constructive. If, in some logical system without LEM (law of excluded middle), you cannot find a proof of P without using LEM, you still have a result, namely you can prove LEM -> P. You haven't really lost anything! Furthermore, I have often been surprised just how far you can go without LEM. Very often in fact.

Finding constructive proofs can feel very much akin to removing an unnecessary dependency from a codebase. Also, even if ultimately, you do need LEM somewhere it is often possible to factor it into the "right" place in the proof rather than globally just sticking `LEM ->` at the front of the whole proof.

Also, if you care about, first order logic then in fact you should love intuintionistic logic: it is a finer logic that actually contains first order logic: https://en.wikipedia.org/wiki/Double-negation_translation

Lastly, though I have yet to understand this better, constructive proofs seem to be enjoy better computational properties under Curry-Howard.

Removing an unnecessary dependency is a good analogy. From a Curry-Howard perspective, intuitionistic proofs correspond to programs without side-effects, and classical proofs correspond to programs that can use continuation effects (for the unfamiliar think of a more principled version of GOTO), so in a real sense intuitionistic proofs are more direct. The double-negation translation then corresponds to implementing continuations in a pure language using continuation-passing style.

This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!

You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert).

Practically, intuitionistic logic has a lot of applications to computer science thanks to Curry-Howard.

Philosophically, soundness of LEM depends on where one originates the source of mathematics. If you're like Kant (or Brouwer) then LEM would make little sense since the source of mathematics, just like any other cognitive ability, is human cognition which exists independent of abstractions of the outer world. But, even without being a Platonist (like Godel) if mathematics has any sort of external source (e.g. abstracting the world or being a good abstraction of the world) then it's really hard to argue against LEM, although some epistemological arguments exist.

   soundness of LEM depends on 
   where one originates the 
   source of mathematics

I disagree!

One of Goedel's many great contributions was the double-negation translation (later refined by others), and what it does is show that (simplifying a bit) intuitionistic logic and classical logic are equiconsistent! In other words: any contradiction you can derive in classical logic, you can convert into a contradiction in intuitionistic logic. (The reverse direction is trivial because all intuitionistic proof principles are also classical.)

> You can construct basically the entire undergrad algebra (vector space, group, ring, field, Galois, module theories) without LEM. LEM shines in algebraic geometry though (thanks to Hilbert).

Just wanted to chime in regarding the last sentence: There are right now ongoing efforts to eliminate any uses of LEM in algebraic geometry.

We do this not only out of academic curiosity, in order to create a more elegant setup and to be able to extract algorithms from proofs, but also to carry out a program called "relativization by internalization". The idea is that we can automatically derive some results for "relative schemes" if we have proven them for ordinary schemes without using LEM or the axiom of choice.

This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop?

Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic.

And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there.

But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively.

The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)

> The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it!

This sounds more like a motivation than like a trouble.

> classical linear logic embeds into intuitionistic.

Wait, really? As I understand it there are things provable in LL that can't be proved in ILL. Can't find the citation though.

It should be noted that double negation translations are more complicated at the proof level even though they capture provability.

Reply on news.ycombinator.com