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

ph004_objective_morality_certificate

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)

 230theorem ph004_objective_morality_certificate :
 231    -- Moral ideal exists and is unique
 232    (∃ a : EthicalAction, MorallyIdeal a) ∧
 233    (∀ a b : EthicalAction, MorallyIdeal a → MorallyIdeal b → a.after = b.after) ∧
 234    -- IS-OUGHT bridge
 235    (∀ a : EthicalAction, MorallyGood a ↔ a.after = 1) ∧
 236    -- Ethics is objective
 237    (∀ a b : EthicalAction, MorallyBetter a b ∨ MorallyBetter b a) ∧
 238    -- Non-ideal states can always be improved
 239    (∀ a : EthicalAction, a.after ≠ 1 →
 240      ∃ b : EthicalAction, MorallyBetter b a) := by

proof body

Term-mode proof.

 241  refine ⟨⟨⟨1, by norm_num, 1, by norm_num⟩, rfl⟩,
 242          moral_ideal_is_unique,
 243          ?_,
 244          ethics_is_objective,
 245          fun a h => let ⟨b, hb, _⟩ := better_action_exists a h; ⟨b, hb⟩⟩
 246  intro a
 247  constructor
 248  · intro h; unfold MorallyGood moral_cost at h
 249    exact (defect_zero_iff_one a.after_pos).mp h
 250  · intro h; unfold MorallyGood moral_cost; rw [h]; exact defect_at_one
 251
 252end ObjectiveMoralityStructure
 253end Philosophy
 254end IndisputableMonolith

depends on (16)

Lean names referenced from this declaration's body.