From no assumptions derive the conclusion

∃x t = x

(where t can be any term).


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:

enter image description here

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.