module module

`IndisputableMonolith.Philosophy.ObjectiveMoralityStructure`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LawOfExistence module_import

declarations in this module (16)

structure EthicalAction L67
def moral_cost L77
def MorallyBetter L80
def MorallyGood L83
def MorallyIdeal L86
theorem moral_ideal_is_unique L93
theorem ideal_iff_good L100
theorem moral_ordering_refl L109
theorem moral_ordering_trans L112
theorem better_action_exists L120
theorem is_implies_ought L147
theorem hume_guillotine_dissolved L176
theorem moral_progress_is_defect_decrease L194
theorem ethics_is_objective L201
theorem cost_ordering_gives_ethics L212
theorem ph004_objective_morality_certificate L230