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? Sin

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.