Proof with EI Restrictions
This video presents the same text shown beside it, spoken and on screen. It adds nothing the text does not say.
Existential instantiation must introduce a name that has not appeared in the proof, which fixes the order of operations: existentials come first, universals afterwards.
Premises: there exists an x such that Fx. And for all x, Fx horseshoe Gx. Prove there exists an x such that Gx. Correct order. Line three: Fa, from line one by existential instantiation, where a is fresh — no earlier line mentions it. Line four: Fa horseshoe Ga, from line two by universal instantiation to that same name, which is permitted because universals hold of everything. Line five: Ga, from lines four and three by modus ponens. Line six: there exists an x such that Gx, from line five by existential generalisation. Now the crash. Reverse the order: instantiate the universal first to a, then instantiate the existential to a as well. That second step asserts that the very thing the universal was applied to is the thing the existential guaranteed. Nothing licensed that identification. The premise said something is F, not that a is F.
The fresh-name requirement is not bookkeeping. A reused name silently asserts an identity the premises never established, and the resulting proof can derive conclusions that are outright false while every individual line matches a rule. Existentials first, and check that the name is new before writing it.