Formalizing Kantian Ethics: Formula of the Universal Law Logic (FULL)

1. Problem Statement

The field of Machine Ethics aims to create Artificial Moral Agents (AMAs) capable of reasoning about moral obligations. Current approaches typically rely on bottom-up or axiomatic methods where human moral intuitions are encoded as a fixed set of rules (e.g., "do not harm," "do not lie"). The author identifies three critical limitations in these existing approaches:

1. Action-Centric vs. Agent-Centric: Current axioms evaluate actions in isolation, ignoring the agent's purpose (maxim). They cannot distinguish between an action performed out of duty versus one performed for public relations (e.g., reducing pollution).
2. The Enumeration Problem: These approaches assume humans can a priori enumerate all moral intuitions to resolve future conflicts and exceptions (the value alignment problem). For instance, without specific exception rules, a surgeon cutting a patient might be flagged as "harm" and impermissible.
3. Lack of Autonomy: AMAs cannot critique the moral axioms they are given, preventing them from participating in moral discourse or adapting to new contexts.

The paper argues for a top-down approach based on Kantian Ethics, specifically the Formula of the Universal Law (FUL), which grounds morality in the consistency of rational agency rather than a list of prohibited actions.

2. Methodology: The Formula of the Universal Law Logic (FULL)

The author proposes FULL, a multi-sorted quantified modal logic designed to formalize Kant's FUL under a Practical Contradiction Interpretation (PCI). Unlike Logical Contradiction Interpretations (LCI) which struggle with natural actions (like murder) that remain conceivable in a universalized world, PCI evaluates whether an action remains an effective means to achieve a purpose in a world where everyone acts on the same maxim.

Core Components of FULL

• Syntax and Sorts: The logic uses sorts for Object, Agent, and Action. It includes terms for agents ($a$), actions ($b$), and formulas ($\phi$).
• Action and Causality:
  • Does(a, b): Agent $a$ performs action $b$.
  • Causes(Does(a, b), $\phi$): A modal operator representing causal laws. The logic assumes omissions also have causal status.
  • Rule R1: If an action causes a state, then performing the action entails that state.
• Willing (Agency):
  • Wills(a, $\phi$): Agent $a$ wills the truth of $\phi$.
  • Consistency (R2): Willing $\phi$ implies not willing $\neg\phi$.
  • Monotonicity (R3): Willing $\phi$ and knowing $\phi \to \psi$ implies willing $\psi$.
  • Necessity (R4): Willing implies necessary conditions (e.g., being alive).
• Maxims:
  • Represented as For(ϕ1, ϕ2), meaning "I will do $\phi_1$ (action) for $\phi_2$ (purpose)."
  • Rule R5: Doing an action for a purpose entails doing the action and willing the purpose.
  • Rule R6: Willing a maxim entails that the action is a cause of the purpose.
• Universal Law Transformation (UL):
  • A syntactic transformation that converts a specific maxim $M$ into a universal law $UL(M)$.
  • It universally quantifies the agent and constants in the purpose ($T_{\phi2}$) and existentially quantifies constants in the action ($T_{\phi1}$).
  • Example: "Karli lies to Jan to get money" becomes "For all agents $x$, if $x$ wants money, there exists an agent $y$ such that $x$ lies to $y$."
• Moral Norms:
  • Defined via deontic operators: Perm (Permissible), Imp (Impermissible), Obl (Obligatory).
  • The FUL Rule: A maxim $M$ is permissible if and only if the agent willing both the maxim and its universal law does not lead to a contradiction ($\bot$).
  • Negation as Failure: If a contradiction cannot be proven, the maxim is not automatically permissible (default assumption).

3. Key Contributions

1. Formalization of FUL under PCI: The paper provides the first rigorous formalization of Kant's first formulation using a Practical Contradiction Interpretation, which handles "natural actions" (violence, omission) that fail under Logical Contradiction interpretations.
2. Agent-Centric Evaluation: The logic evaluates the maxim (action + purpose) rather than just the action. This allows the system to distinguish between morally distinct scenarios involving the same physical act (e.g., murder vs. life-saving surgery).
3. Reduction of Human Intuition: The system does not require pre-encoded moral axioms (e.g., "do not kill"). Instead, it derives moral norms from formal principles of rational agency, causality, and background non-normative knowledge.
4. Distinction of Duties: The logic formally distinguishes between:
   • Contradictions in Conception (CC): The action becomes inconceivable as a universal law (e.g., false promising). This yields Perfect Duties (strict prohibitions).
   • Contradictions in the Will (CW): The action is conceivable but renders the agent's necessary ends (e.g., survival) impossible. This yields Imperfect Duties (broad obligations to help).

4. Results and Demonstrations

The author demonstrates the efficacy of FULL through formal proofs on three canonical Kantian cases:

• Case 1: False Promising (Perfect Duty)

  • Scenario: Karli promises to repay Jan to get travel money, intending to break the promise.
  • Result: In the Universal Law World (WUL), everyone breaks promises. Consequently, no one believes promises. Thus, promising becomes an ineffective means to get money.
  • Contradiction: Karli wills a world where promising is ineffective (via UL) but also wills her specific promise to be effective (via M). This contradiction proves the maxim is Impermissible.

• Case 2: Murder for a Job (Perfect Duty)

  • Scenario: Karli murders a rival to secure a job.
  • Result: In the WUL, everyone murders rivals. Karli cannot be certain she won't be murdered. If she is murdered, her act of murdering others cannot cause her to get the job.
  • Contradiction: The action ceases to be an effective means to the end in the WUL. The maxim is Impermissible.
  • Contrast: The paper notes that if the action were "surgery," the universalization would still be effective (saving lives), so the logic correctly permits it, unlike rule-based systems that might flag "cutting" as harm.

• Case 3: Never Helping Others (Imperfect Duty)

  • Scenario: Karli adopts a maxim of never helping others to save time for leisure.
  • Result: In the WUL, no one helps anyone. Since rational agents require help to survive (background fact), Karli wills a world where she is not alive.
  • Contradiction: Karli wills to be alive (a necessary condition for willing anything) but also wills a world where she is dead. This is a Contradiction in the Will.
  • Outcome: The maxim is Impermissible, generating an Imperfect Duty to help others sometimes.

5. Significance and Future Work

• Robustness for AMAs: FULL offers a path toward AMAs that are more autonomous and robust, capable of reasoning about novel situations without needing every exception hard-coded by humans.
• Formal Understanding of Kant: It bridges the gap between philosophical interpretation and computational logic, providing a machine-readable definition of Kantian ethics.
• Limitations & Future Directions:
  • Maxim Formulation: The current work assumes the input maxim is correctly formulated. The paper acknowledges that describing actions (e.g., "killing" vs. "destroying cells") requires moral judgment, which remains a challenge.
  • Model Theory: Future work aims to move from proof-theoretic definitions to model-theoretic semantics, particularly for intensional concepts.
  • Quantifiers: The logic plans to incorporate generalized quantifiers (e.g., "most," "few") to handle concepts like promising that survive occasional defeats, which standard $\forall$ and $\exists$ cannot capture.

In conclusion, the FULL logic successfully demonstrates that moral norms can be derived top-down from formal principles of rationality and causality, offering a promising alternative to the brittle, intuition-heavy rule sets currently used in machine ethics.