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

hume_guillotine_dissolved

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)

 176theorem hume_guillotine_dissolved :
 177    -- The moral ideal exists (is achievable)
 178    (∃ a : EthicalAction, MorallyIdeal a) ∧
 179    -- The moral ideal is unique
 180    (∀ a b : EthicalAction, MorallyIdeal a → MorallyIdeal b → a.after = b.after) ∧
 181    -- All non-ideal actions can be improved
 182    (∀ a : EthicalAction, a.after ≠ 1 →
 183      ∃ b : EthicalAction, MorallyBetter b a) :=

proof body

Term-mode proof.

 184  ⟨⟨⟨1, by norm_num, 1, by norm_num⟩, rfl⟩,
 185   moral_ideal_is_unique,
 186   fun a h_nonideal =>
 187     let ⟨b, hb, _⟩ := better_action_exists a h_nonideal
 188     ⟨b, hb⟩⟩
 189
 190/-! ## The Cost-Based Action Model -/
 191
 192/-- **Theorem (Moral Progress = Defect Decrease)**:
 193    A sequence of actions constitutes moral progress iff defect decreases. -/

depends on (22)

Lean names referenced from this declaration's body.