On Mon, Jul 29, 2013 at 6:27 PM, Alex Smith <[email protected]> wrote: > How do you define "iff" (in the rules) in the absence of the law of > excluded middle? It may not be the same way that the rules themselves > do.
Ah, yes. That makes sense. ((a -> b) <-> a) -> b holds intuitionistically, but (((a -> b) -> a) & (~(a -> b) -> ~a)) -> b does not. The rules say the latter, including the rule about security.
