Showing that $\neg[ Px\rightarrow \forall xPx]\vdash \forall xPx$ via generalization theorem

Question

Let $P$ be a unary relation, we want to show that:

If $\neg[ Px\rightarrow \forall xPx]\vdash Px$ then $\neg[ Px\rightarrow \forall xPx]\vdash \forall xPx$.

I want to do that via generalization theorem but $x$ is free in $\neg[ Px\rightarrow \forall xPx]$ so I can't use the theorem here. I've to change the free $x$ to another variable say $y$, So, now we have

$$\neg[ Px\rightarrow \forall xPx]\vdash Py$$ and we then can use generalization theorem to obtain $\neg[ Px\rightarrow \forall xPx]\vdash \forall y Py$ which is $$\neg[ Px\rightarrow \forall xPx]\vdash \forall x Px$$ and we are done. In changing $x$ into $y$, we have assumed implicitly that $Px\vdash Py$

My question is: How to show that $Px\vdash Py$? How to justify this changing of variables from $x$ into $y$?

Answer 1

You cannot ...

It is not ture that $Px \vdash Py$, simply because : $Px \nvDash Py$.

As you can see from the answer above, you cannot prove : $¬[Px→∀xPx]⊢∀xPx$ because it is not valid.

Cosnider the interpretation sugegste by Rob, with $\mathbb N$ as the domain of the interpretation and $(x=1)$ in place of $P(x)$.

in order to show that :

$x=1 \nvDash y=1$

it is enough to assign to $x$ the value $1$ and to $y$ the value $0$.

Answer 2

You haven't said exactly what logic you are working in, but the deduction you are trying to make is not correct in the usual formulations of first order logic. To see this, note that $\lnot(A \rightarrow B)$ is equivalent to $A \land \lnot B$. If you interpret $Px$ as $x = 1$ in the theory of the natural numbers, then $\lnot[Px \rightarrow \forall xPx] \vdash Px$ (i.e., $x = 1 \land \exists x (\lnot x = 1) \vdash x = 1$) is true, but $\lnot[Px \rightarrow \forall xPx] \vdash \forall xPx$ (i.e. $x = 1 \land \exists x (\lnot x = 1) \vdash \forall x(x = 1)$) is not. Are you sure you have written the quantifiers down correctly?