Question about proving a set that is quantificationally inconsistent in PD+ (Finished the proof but want it to be checked)

Question

Does ∃x(Nx & ~Nx) contradiction itself?

Is there an error in my proof?

Thank you

Answer 1

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.