Let A be a pair (i, x)


$H(A)$ <=> program i halts on input x


$P(A)$ <=> (there exists a proof for $H(A)$) $\vee$ (there exists a proof for $\neg H(A)$)


Assume $\forall A: P(A)$ then we can solve the halting problem (write an algorithm that enumerates all proofs and checks whether they proof $H(A)$ or $\neg H(A)$)
Therefore $\exists A: \neg P(A)$.


For such an A:


Assume $H(A)$: Then we have a proof for $H(A)$ (the sequence of steps that lead to the halting state). Therefore $\neg H(A)$.


But now we have a proof for $\neg H(A)$ and therefore $P(A)$ which contradicts the definition of A???


I assume I have a basic misconception about something. Please tell me what went wrong?


Thanks



Provability of termination. Whats wrong with my reasoning?
I believe that the error sneaks in with the phrase "for such an A." It is indeed true that for any $A$ such that $\neg P(A)$ we have that $\neg H(A)$; it follows that to be able to prove $\neg P(A)$ actually requires us to be able to prove $\neg H(A)$. You've substituted the *a priori* knowledge "this is such an $A$" for the proof that this $A$ has the property $\neg P(A)$, but it's the latter of these that you actually need. This avoids any paradox.


