исчисление предикатов

[BapuK]

Исчисление предикатов гильбертовского типа, как показать, что
$\forall x\Phi(x,x) \vdash \exists y \exists z \Phi(y,z)$.
Стопор на первом же шаге, т.к. не пойму как под знаком предиката получить два разных символа, все попытки приводят к $\Phi(y,y)$ и $\Phi(z,z)$ и тому подобным...

[Maslov]

Посмотрите Клини С. Математическая логика (стр. 155, теорема 26, формула 80).
Там, правда, немного другое утверждение доказывается: $\vdash \exists x A(x, x) \to \exists x \exists y A(x, y)$

[BapuK]

мм, спасибо, помогло