Let A be the statement: "P=NP or P!=NP" (in other words, suppose P vs. NP is decidable in some chosen axiomatic system, like Zermelo-Fraenkel set theory with or without axiom of choice).
You first said:
Suppose we proved A. Then we could also prove that we proved A. This is practically a tautology, since if we proved A, of course we can prove we proved A. I'll just hand you the proof.
Next, you said:
Suppose we can prove ~A (in other words, suppose we can prove that P vs. NP is undecidable in the given axiomatic system). Contradiction!
To sum it up, you said: "Suppose A and ~A. Contradiction!"
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.
You first said:
Suppose we proved A. Then we could also prove that we proved A. This is practically a tautology, since if we proved A, of course we can prove we proved A. I'll just hand you the proof.
Next, you said:
Suppose we can prove ~A (in other words, suppose we can prove that P vs. NP is undecidable in the given axiomatic system). Contradiction!
To sum it up, you said: "Suppose A and ~A. Contradiction!"
Or am I missing something here?