Help with formalization of argument (ignore premises) in FOL

Question

I am trying to formalize the following argument:

1. Every Moral theory is equally valid.
2. There always can get a new moral theory from another one.
3. For something to be metaphysically real/exists it must be also definable
4. The definition of morality must be a moral theory.
5. Because 1 and 2 there cannot be a moral theory that defines morality
6. Because 4 and 5 there cannot be a definition of morality
7. Because 3 and 6 there cannot exist morality.

I have archived general success formalizing the argument until I have to formalize premise 3 and step 7. Here is my work so far:

Let L mean "is metaphysically logically valid"

Let M mean "is a moral theory"

Let N mean "defines morality"

Let E mean "Exists"

Let Dxy mean "x defines the concept y"

Let W mean "x is morality"

  | 1. ∀x(Nx ⇔ ∀y[Wy → Dxy])           Extraction from N axiom
  | 2. ∀x(Nx → Mx)                     The definition of morality must be a moral theory
  | 3. ∀xy (Lx ∧ Ly → Lxy)             If x and y are methaphisically logically valid interdependently must also hold dependently
  | 4. ∀x  (Mx → Lx)                   Hume's Law                   
  | 5. ∀x  (Mx ∧ Lx → ∃y[My ∧ ¬Lxy])   Construction of contradictory Moral theories
  | 6. ∀x(Ex → ∃y(Wy ∧ Dxy))                    Realism-Existence requires defineability
  | | 7. ∃x(Mx ∧ Lx)
  | | u 8. Mu ∧ Lu
  | | | 9. Mu ∧ Lu → ∃y(My ∧ ¬Luy)                        ∀E 5
  | | | 10. ∃y(My ∧ ¬Luy)                                  →E 8, 9
  | | | w 11. Mw ∧ ¬Luw
  | | | | 12. Mw                                          ∧E 11
  | | | | 13. Mw → Lw                                     ∀E 4
  | | | | 14. Lw                                          →E 13, 12
  | | | | 15. Lu                                          ∧E 8
  | | | | 16. Lu ∧ Lw                                     ∧I 15, 17
  | | | | 17. Lu ∧ Lw → Luw                               ∀E 3
  | | | | 18. Luw                                         →E 17, 18
  | | | | 19. ¬Luw                                        ∧E 11
  | | | | 20. ⊥                                           ¬E 16, 17
  | | | 21. ⊥                                             ∃E 10, 11-20
  | | 22. ⊥                                               ∃E 7, 8-21
  | 23. ∃!x(Mx ∧ Lx)                                     RaA 7-22 
  | | 24. ∃x(Nx)
  | | u 25. Nu
  | | | 26. Nu → Mu                                       ∀E 2
  | | | 27. Mu                                            →E 26, 25
  | | | 28. Mu → Lu                                       ∀E 4
  | | | 29. Lu                                            →E 28, 27
  | | | 30. Mu ∧ Lu                                       ∧I 27, 29
  | | | 31. ∀x(¬Mx ∨ ¬Lx)                                 Id 23
  | | | 32. ¬Mu ∨ ¬Lu                                     ∀E 31
  | | | | 33. ¬Mu
  | | | | 34. ⊥                                           ¬E 33, 27
  | | | | 35. ¬Lu
  | | | | 36. ⊥                                           ¬E 35 29
  | | | 37. ⊥                                             ∨E 32, 33-34, 35-36 
  | | 38. ⊥                                               ∃E 23, 24-25
  | 39. ∃!x(Nx)                                          RaA 23-38
  | 40. ∀x(¬Nx)                                           Id 39
  | 41. ¬Nv                                               ∀E 40
  | 42. Nv ⇔ ∀y[Wy → Dvy]                                 ∀E 1
  | 43. ¬∀y[Wy → Dvy]                                     ⇔E 42
  | 44. ∃y[Wy ∧ ¬Dvy]                                     Id 43
  | | 45. ∃x(Ex ∧ Wx)
  | | u 46. Eu ∧ Wu
  | | | 47. Eu                                            ∧E 46
  | | | 48. Eu → ∃y(Wy ∧ Duy)                             ∀E 6
  | | | 49. ∃y(Wy ∧ Duy)                                  →E 48, 47
  | | | r 50. Wr ∧ Dur
  | | | | | o 51. Wo ∧ ¬Dvo
  | | | | | 52. ¬Dvo                                      ∧I 51
  | | | | | 53.  Dur                                      ∧I 50
  | | | | | 54.  ⊥                                        ¬I 52, 53
  | | 55.  ⊥                                              ∃E 45, 46-54
  | 56. ¬∃x(Ex ∧ Wx)

As seen I only reached to conclude that there is no definition of morality in some sense, such discussion is clearly mathematical so no comments on that.

Contently I have been having problems Formalizing the premise: For x to exists metaphysically it must be definable. In such one that is can work with the conclusion ∃!x(Nx). I kind on attempt until the end, but still struggle with the derivations.

The final objective is ¬∃x(Ex ∧ Wx), but I am certainly no being able to properly reach. And I don't feel a much comfortable with ∃y[Wy ∧ ¬Dvy] existence claim.

Answer 1

"∀x(Ex → ∃y(Wy ∧ Dxy))," seems weird, doesn't it translate to, "For all x, if x exists then there is a y such that y is a moral theory and y is defined by x"? So that every term whatsoever, e.g. terms for colors, sounds, cats, dogs, gods, demons, etc. can be used to define a moral theory? But it seems as though you could define any theory about anything in such a way, though you'd end up with innumerable superfluous theories about whatever things.

The claim that "the definition of morality must be a moral theory" seems to be a case of semantic holism and so would be of a piece, to a decent extent, with an observation by Rawls (in A Theory of Justice, though I don't remember where exactly) about the usefulness of trying to define the terms of any theory before spelling the rest of a theory out. However, Rawls goes on to say that we could drop talk of, "What is right?" for, "What is in compliance with the principles of the original position?" and we'd lose little, in the end (while gaining much, perhaps).

So even if the word "morality" did not admit of a stable definition, and hence if, "What is the moral thing to do?" were a necessarily unstable question, we could still ask, "What promotes the greatest good for the greatest number?" or, "What is categorically imperative for us to do?" and so on: all those questions still exist, they have relatively sharper definitions, and so moral theory can proceed apace (just avoid using the phrase "moral theory," then, though!).

Like they were saying in the MathSE commentary, to be technical about the argument, the use of an existence predicate and the reference to higher-order terms (metaterms like "definition" and "theory") kinda pushes the whole line of reasoning beyond FOL. Not very far beyond it, perhaps, though.

Overall, I guess the problem with this reasoning is that it's kind of like a reverse ontological argument, where instead of trying to define something into existence, you're trying to define something out of it. You'll probably have to develop a stronger theory about your use of the word "existence" before the argument crystallizes more efficiently, I suppose.