Proving Russel paradox using Hilbert style deduction

Question

On Wikipedia's entry for Formal Presentation of Russel's paradox, existential instantiation ("reusing the symbol y") is one of the two steps (the other being universal instantiation) employed to get from

$\exists y\forall x\ (x\in y \iff P(x))$

to

$y \in y \iff y \not\in y$

I'm trying to see how this argument would look like in a Hilbert deduction system - in particular, what form would existential instantiation take? I've found one possible answer Carl Mummert gave here, where existential instantiation would be a metatheorem, and applied to this particular case with

$\phi(y) \equiv (\forall x\ (x\in y \iff P(x)))$

$\psi \equiv (y \in y \iff y \not\in y)$,

the theorem would state that if $\phi(c)\vdash\psi$ then $(\exists y) \phi(y)\vdash \psi$.

The theorem also states that "there is a deduction witnessing this fact that does not mention $c$". What would be the explicit form of this deduction? I.e. how would we get from

$\exists y\forall x\ (x\in y \iff P(x))$

to

$y \in y \iff y \not\in y$

using Hilbert style deduction only?

Answer 1

For an Hilbert style deduction you need to state what the axiom(schemes) and inference rules of your system first

the axiom(scheme) for Existentional elimination is most times something like

ExPx -> ((Pt -> Q) -> Q) where Q may not contain t

Hilbert style proofs are most times also hoplessly long here a proof in natural deduction:

• 1 | EyVx( x e y <-> P(x)). . . . . Premmisse
• 2 | |_t Vx( t e y <-> P(x)). . . . . New subproof
• 3 | | Vx( t e y <-> ~(x e t)). . . . 2 define P(X)
• 4 | | t e t <-> ~(t e t). . . . . . . . . 3 Universal elimination (or instantisation)
• 5 | | Ez( z e z <-> ~(z e z)) . . . 4 Existentional Introduction
• < | <------------------------------ end subproof
• 6 | Ez( z e z <-> ~(z e z)) . . . . . 1, 2-5 Existentional elimination
• 7 | Ey( y e y <-> ~(y e y)) . . . . 6 relettering

Sorry layouting it nice is a bit to complex for me

Hope this helps