Universal elimination in Fitch

Question

I've returned to tinkering with some arguments in Fitch after not having had anything to do with formal logic in a while, and I suppose I've grown rustier than I thought I had because I simply can't figure out why the following application of universal elimination is invalid.

For reference, here is the correction application of the rule:

I suppose I was expecting that all instances of the quantified variable would be replaced with the arbitrary variable. Why is this not the case? Why does Px not become Pa?

Answer 1

I simply can't figure out why the following application of universal elimination is invalid. $$\begin{array}{|l}\forall x~\forall y~((Px\land\lnot Py)\to(y<x))\\\hline\begin{array}{|l}\boxed a\\\hline\forall y~((Pa\land\lnot Py)\to(y<a))\end{array}\end{array}$$

$\bullet$ That is because it is valid.   You have instantiated all free occurrences of the predicate's bound variable ($x$) to the assumed variable ($a$).

For reference, here is the correction application of the rule:

$$\begin{array}{|l}\forall x~\forall y~((Px\land\lnot Py)\to(y<x))\\\hline\begin{array}{|l}\boxed a\\\hline\forall y~((Px\land\lnot Py)\to(y<a))\end{array}\end{array}$$

$\color{red}{\large\times}$ This correction is incorrect; it is in fact an invalid inference.   This leaves an occurrence of the bound variable free.   It should be disallowed by your proof checker.   Submit an error ticket to the developers.