よくわからん・・・

∃P. ∀x. (P(x)↓)∧((∀y. x(y)↓) ⇔ P(x))　・・・(1)
∃P'.∀x. (P(x) ⇔ ¬(P'(x)↓))　・・・(2)

(1)、(2)から

∃P'.∀x. ((∀y. x(y)↓) ⇔ ¬(P'(x)↓))　・・・(3)

(3)にx = P'を代入

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

ってことで、(∀y. P'(y)↓) ⇒ P'(P')↓だから矛盾てことでいいのかな