0

enter image description here

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

Is there an error in my proof?

Thank you

1

1 Answer 1

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.

3
  • 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)
    – Stanley
    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.
    – Stanley
    Commented Apr 4, 2021 at 3:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .