Ya, it looks like I bungled the logic. Let 'Pr X' means 'X is provable'. Let A be your A. Really what I wanted to say is that: Pr A -> (~Pr ~Pr A) and thus,

Ya, it looks like I bungled the logic. Let 'Pr X' means 'X is provable'. Let A be your A. Really what I wanted to say is that: Pr A -> (~Pr ~Pr A) and thus, Pr a -> Pr ~Pr ~Pr A. Hence, ~Pr ~Pr ~Pr A -> ~Pr A Taking A to be ~Pr A, we get: ~Pr ~Pr ~Pr ~Pr A -> ~Pr ~Pr A So you can peel off pairs of ~Pr until you get down to one or two. Not very surprising, I guess, since Pr A == A in constructive logic, and you can do similar negation collapsing there.