0

enter image description here

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

Is there an error in my proof?

Thank you

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
    Apr 4 at 0:00
  • Yes. You just cannot use the subproof raised by that assumption for existential elimination because a is not a fresh variable. Apr 4 at 2:31
  • Thanks for the help! Cannot finish these two without your suggestion.
    – Stanley
    Apr 4 at 3:41

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.