How does one go about this natural deduction proof?

Question

From no assumptions derive the conclusion

∃x t = x

(where t can be any term).

Answer 1

Unless one is considering a "free logic", classical first order logic assumes all models that would be permitted to provide countermodels have a non-empty domain. So there exists a member of the domain which one may name t. Let x be a variable representing any member of the domain.

Here is a proof of the above using a Fitch-style proof checker:

The first line of the proof asserts that the domain is not empty. Equality introduction can derive the existence of t = t.

The next line uses existential introduction (∃I) on the second t of line 1 to derive the goal on line 2.

One may wonder why I was not forced by the proof checker to replace both instances of t with x when I used existential introduction. The authors of forallx explain it as follows: (Chapter 32, page 260)

But we do not need to replace both instances of a name with a variable: if Narcissus loves himself, then there is someone who loves Narcissus.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf