数式で書いてみたよ
最初の P が受け取る x は引数をとらないと解釈した。
↓ が「停止する」ね。
どこが矛盾？

> 任意のプログラムxに対して、無限ループするかどうかを
> 確実に検出するプログラムPが存在すると仮定する。

∃P.∀x. (x↓ ⇔ P(x)↓true)

> Pを用いて、次のようなプログラムP'を構成する：
> P'は、入力xに対してPを用いて判定し、
> (1) xが無限ループするなら停止し、
> (2) xが無限ループにならないならわざと無限ループする

∃P'.∀x. (x↓ ⇔ ¬(P'(x)↓))

> さあ、P'の入力として、P'自身を判定させてみよう！
> 上記のxにP'を代入すると、

代入すると
P'↓ ⇔ ¬(P'(P')↓)