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

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

Is there an error in my proof?

Thank you

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.

• Can I do the universal emulation under the assumption Oa & ~Na so that I can keep using 'a' in the sentence? in Ax(Mx v Nx) and Ax (Mx -> ~Ox) Commented Apr 4, 2021 at 0:00
• Yes. You just cannot use the subproof raised by that assumption for existential elimination because a is not a fresh variable. Commented Apr 4, 2021 at 2:31
• Thanks for the help! Cannot finish these two without your suggestion. Commented Apr 4, 2021 at 3:41