How can I formalize the argument that morality cannot exist, in FOL?

I am trying to formalize the following argument:

1. Every moral theory is equally valid.
2. One can always get a new moral theory from another one.
3. For something to be metaphysically real or to exist, it must be definable.
4. The definition of “morality” must be a moral theory.
5. By 1 and 2, there cannot be a moral theory that defines morality.
6. By 4 and 5, there cannot be a definition of morality.
7. By 3 and 6, morality cannot exist.

I have formalized the argument up to Premise 3 and Step 7.

Here is my work so far:

• Let L(x) mean "x is metaphysically logically valid".

• Let MT(x) mean "x is a moral theory".

• Let DM(x) mean "x defines morality".

• Let E(x) mean "x exists".

• Let D(x, y) mean "x defines the concept y".

• Let M(x) mean "x is morality".

``````  | 1. ∀x(DM(x) ⇔ ∀y[M(y) → D(x, y)])  This is an axiom based on the definitions of DM, M, and D: x defines morality if and only if for anything that is morality, x defines it.
| 2. ∀x(DM(x) → MT(x))                    Anything which defines morality must be a moral theory.
| 3. ∀xy (Lx ∧ Ly → Lxy)             If x and y are metaphysically logically valid interdependently, then they must also be so 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.

• @MauroALLEGRANZA, they told Rieke to post the question here, though why they didn't just move the question from there to here, IDK. (To be honest, anytime I've ever tried to use the move-question function on this site, it just gives me the PhilosophySE Meta as an option.) Dec 17, 2022 at 16:57
• I'd have technical objections to your formalization (but is that even on-topic on this site?), plus I'd say the thesis is anyway based on a categorical error: in short, because nothing of that has a metaphysical import, and then it's rather a matter of competing theories... May 11 at 12:00
• I would say we need to do a lot of work fine-tuning the argument before we can begin to approach the intended aim. I’m not sure why “if x defines morality then x is a theory of morality”. A theory can be something more than a definition. Maybe you could say “draws from a theory of morality”? I also don’t understand #3 - if x and y are logically valid, then so is “xy”. But what is “xy”? Some way of “putting x and y together”? How? May 11 at 17:04