Hacker News Reader

I've heard that propositional logic helps with this because you don't assume everything is either true or false, but rather look at what can be implied.

You can then decide if you want the law of the excluded middle or not. I'm paraphrasing a talk I watched but would love to hear from someone knowledgeable on this subject...

View on HN

You are probably thinking of intuitionistic logic versus classical logic. In the former, the law of excluded middle is not built in.

Yes that's the one. Thanks

If you have heard of the Curry-Howard equivalence, that programs and proofs are the same thing, the proofs in question are constructive, intuitionistic proofs.

I've been leaning towards intuitionism for exactly this reason. Sadly, it makes a lot of results harder to proof (and iirc it even makes some results impossible). I've been toying with the idea that these results are simply 'not useful'.

Reply on news.ycombinator.com