Will Crichton

I really like this blog post from @hillelogram because it touches upon something I’ve been thinking about a lot lately that didn’t make it into my most recent blog post: how constructive approaches have a really hard time capturing *negative* information.https://twitter.com/zayenz/status/1294172678161674245 …

Is this somehow linked with intuitionism and law of excluded middle? Whereby you can’t prove existence by claiming the inverse to be true?

Yes. Intuitionistic logic is also known as “constructive logic,” which is not a coincidence. And the Curry-Howard correspondence, which is also deeply related, connects computation to intuitionistic logic.

Thanks for the explanation. It has me wondering, would this mean certain predicative structures would be inexpressible in constructive logic? Or are their extensional domains equivalent?

This is a really good question. It’s possible for the predicate to be undecidable, in which case it can’t be captured constructively, but that isn’t very interesting—any useful validation predicate will be decidable. And in that case, I’m not sure I know the answer!

I just spent the better part of an hour thinking about it, and I feel like I *should* know the answer (i.e. it feels like something I should be able to deduce from things I already know), but I’m afraid I don’t have the mathematical knowledge to say. Maybe @hillelogram does?

This has been a question I have been mulling over for quite some time now, but I am trying to improve my knowledge of the mathematical machinery/context needed to precisely arrive at a good delineation of what separates these approaches/schools of thought.