pith. machine review for the scientific record. sign in
theorem proved term proof

moral_progress_is_defect_decrease

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 194theorem moral_progress_is_defect_decrease (a b : EthicalAction) :
 195    MorallyBetter a b ↔ defect a.after ≤ defect b.after := Iff.rfl

proof body

Term-mode proof.

 196
 197/-- **Theorem (Ethics is Objective)**:
 198    The moral ordering is objective: it depends only on the cost function J,
 199    not on any subjective preferences or cultural norms. Two rational agents
 200    with the same cost function will agree on all moral comparisons. -/

depends on (14)

Lean names referenced from this declaration's body.