TrolleyChoice
TrolleyChoice supplies the two-element domain for the trolley problem in Recognition Science, distinguishing the action of pulling the lever from inaction. Modelers of ethical J/σ tradeoffs cite it to anchor cost functions that separate lives-lost minimization from agency-imbalance penalties. The declaration is a direct inductive definition with constructors pull and doNothing, automatically deriving decidable equality and inhabitedness.
claimLet $T$ be the set of trolley choices with two elements: pull (diverting the trolley, incurring one death) and doNothing (preserving the original track, incurring five deaths).
background
The module frames the classic trolley dilemma inside Recognition Science as a strict J/σ tradeoff. Utilitarian evaluation tracks J-cost via lives lost; deontological evaluation tracks σ-cost via the agency imbalance created by an active intervention. livesLost maps pull to 1 and doNothing to 5; sigmaCost maps pull to 1 and doNothing to 0; jCost simply lifts livesLost to the reals. The setting sits in the philosophical-paradoxes row of the framework and references the 14 DREAM virtues as the structural bridge that could, in principle, reconcile the two axes.
proof idea
The declaration is an inductive definition that introduces exactly two constructors, pull and doNothing. Derivation of DecidableEq and Inhabited is automatic; no lemmas or tactics are invoked.
why it matters in Recognition Science
TrolleyChoice is the root type for every downstream result in the module: jCost, livesLost, sigmaCost, pull_lowers_J, pull_raises_sigma, tradeoff_strict, and no_strictly_dominant_choice all quantify over it. It supplies the concrete instance of the J/σ tradeoff described in the module documentation, placing the trolley problem inside the Recognition Science treatment of ethical decisions. The construction touches the open question whether a virtue-aligned action can ever escape the strict dominance prohibition shown by no_strictly_dominant_choice.
scope and limits
- Does not assign overall moral preference to either choice.
- Does not embed the 14 DREAM virtues into the choice set.
- Does not model probabilistic or continuous variants of the dilemma.
- Does not claim resolution of the underlying ethical tension.
formal statement (Lean)
52inductive TrolleyChoice where
53 | pull
54 | doNothing
55 deriving DecidableEq, Inhabited
56
57namespace TrolleyChoice
58
59/-- Display name. -/