[Haskell-cafe] haskell-curry, classical logic, excluded middle
lrpalmer at gmail.com
Sun Oct 14 17:20:46 EDT 2007
On 10/14/07, Tim Newsham <newsham at lava.net> wrote:
> I've been struggling with this for the last day and a half. I'm
> trying to get some exercise with the type system and with logic by
> playing with the curry-howard correspondence. I got stuck on
> the excluded-middle, and I think now I got it almost all the way
> there, but its still not quite right. Is this error I'm getting
> (inline at the end) easily fixed, and what exactly is going on?
I'll admit this is a cursory response, but (to my understanding)
excluded middle doesn't hold in the Curry-Howard correspondence. It
is an isomorphism between *constructive* logic and types; excluded
middle is a nonconstructive axiom.
More information about the Haskell-Cafe