logoalt Hacker News

smj-edisonyesterday at 4:22 PM1 replyview on HN

Ah, so if you had ¬p, and you negated it, you could technically construct ¬¬p in intuitionist logic, but only in classical logic could you reduce that to p? Since truth in classical logic means what you said here, where you didn't actually construct what p is, so you can't reduce it in intuitionistic logic.


Replies

ted_dunningtoday at 12:24 AM

Yes.