Does ∃x(Nx & ~Nx) contradiction itself?
Is there an error in my proof?
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
Yes, there is an error.
A valid existential elimination subproof requires its witness to be a fresh variable; meaning that it must not occur in any premise or prior assumption.
Your witness term
a in line 7 does occur in such; it occurs in the premise on line 4.
The witness must be fresh because otherwise we could prove 1 = 0, as follows:
1.| Ex (x=0) Premise 2.|_ c=1 Premise 3.| |_ c=0 Assume 4.| | 1=0 Equality Elimination 2,3 5.| 1=0 Existential Elimination 1,3-4
That aside, when using a fresh witness, your proof is valid.
1.| Ax (Mx v Nx) Premise 2.| Ex (Ox & ~Nx) Premise 3.| Ax (Mx -> ~Ox) Premise 4.|_ Ma v Na Premise 5.| |_ Ob & ~Nb Assume (fresh witness) 6.| | Mb v Nb A Elimination 1 7.| | Mb -> ~Ob A Elimination 3 8.| | |_ Mb Assumption 9.| | | ~Ob -> Elimination 7,8 10.| | | Ob & Elimination 5 11.| | ~Mb ~ Introduction 8-(9,10) 12.| | Nb v Sylogism 6,12 13.| | ~Nb & Elimination 5 14.| | Nb & ~Nb & Introduction 12,13 15.| | Ex (Nx & ~Nx) E Introduction 14 16.| Ex (Nx & ~Nx) E Elimination 2,5-16
So you have that your premises entail the existence of a contradiction.
Therefore the premises are unsatisfiable.