>>83
(∀y. P'(y)↓) ⇔ ¬(P'(P')↓) は
P'(P')↓ かつ ∃y. ¬(P'(y)↓) なら矛盾しない。
つまりこの設定だと矛盾しない。
だから P' を
∀x.((∀y.x(y)↓) ⇔ ¬(P'(x)↓))
ではなく、ちゃんと
∀x.((x(x)↓) ⇔ ¬(P'(x)↓))
と定義しないといけない。