Неразрешимость ZF

[Darts501]

Помогите решить задачу. Нужно доказать, что если ZF непротиворечива, то она не разрешима, то есть не существует алгоритма, который по любой данной ему формуле выясняет, выводим а ли эта формула. Можно использовать, что любой разрешимый предикат представим в ZF.

[AGu]

Обычно неразрешимость теории множеств (любой из ее версий) выводится из существенной неразрешимости арифметики (Россер, 1936 г.) — благодаря тому факту, что арифметика интерпретируется в теории множеств. Если упомянутые сведения «можно использовать», то дело в шляпе. Ну а если нельзя, то поди догадайся... Неразрешимость — штука нетривиальная, в лоб не доказывается.