It is pedagogically always better to learn Fitch-style natural deduction systems such as this one. The reason that logic texts often introduce Hilbert-style systems is that they are a bit easier to reason about. But they are totally impractical for actual mathematics, and certainly bad for new students learning FOL.
In particular, take a look at the ∃intro rule in the linked system. It says that if you have deduced "E ∈ S" for some object expression "E" in the current context, and have deduced "Q(E)", then you can deduce "∃x∈S ( Q(E) )" in the same context. So it cannot be used in the way you tried in your question, because in my Fitch-style system you cannot have any undeclared variable and so the proof has to look like:
Given x∈obj:
F(x) = F(x). [1]
∀x∈obj ( F(x) = F(x) ). [2]
// Everything below this is WRONG //
F(x)∈obj. [3]
∃y∈obj ∀x∈obj ( F(x) = y ). [4]
- Unlike in most Hilbert-style systems, [1] cannot be deduced outside its subcontext, because "x" must be declared before "F(x)" is meaningful.
- [2] is deduced in the global context, but observe that "x" in the global context is not referring to anything; it was only referring inside the subcontext.
- The variable "x" in [2] is only meaningful under the ∀-quantification, and not outside it. This a "x" is sometimes called a dummy variable since it merely conveys what the quantification is. As you ought to expect, [2] is equivalent to ∀y∈obj ( F(y) = F(y) ), in which "y" is the dummy variable.
- [3] is wrong precisely because "x" is not meaningful there, nor is "F(x)".
Here is a more striking example of your logical fallacy:
Given x∈obj:
x = x.
∀x∈obj ( x = x ).
// Everything below this is WRONG //
x∈obj.
∃y∈obj ∀x∈obj ( x = y ).
So the fallacy has nothing to do with function-symbols! I will note that my deductive system for FOL permits the universe obj
to be empty, unlike the other common kind of deductive system. Both kinds of systems are equally powerful, but the kind that my system belongs to is the more intuitive kind, so once you understand the key ideas it will be obvious what the inference rules should be. These two kinds differ in that the other kind proves ∃x ( x = x ) whereas my system does not prove ∃x∈obj ( x = x ). I hope the above explanation of your fallacy lets you see how this is related.
In any case, feel free to ask further in comments!