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

TL;DR

This paper introduces the Formula of the Universal Law Logic (FULL), a formal logical framework for Kantian ethics that enables autonomous moral reasoning in AI without relying on predefined moral axioms.

Contribution

It formalizes Kant's first formulation of the categorical imperative using a multi-sorted modal logic, addressing limitations of previous approaches by considering agent purposes and reducing reliance on human moral intuition.

Findings

FULL can evaluate actions based on agent purposes without moral axioms.

It formalizes Kantian ethics concepts like causality and agency.

Demonstrates reasoning on three Kantian ethics cases.

Abstract

The field of machine ethics aims to build Artificial Moral Agents (AMAs) to better understand morality and make AI agents safer. To do so, many approaches encode human moral intuition as a set of axioms on actions e.g., do not harm, you must help others. However, this introduces (at least) two limitations for future AMAs. First, it does not consider the agent's purposes in performing the action. Second, it assumes that we humans can enumerate our moral intuition. This paper explores formalizing a moral procedure that alleviates these two limitations. We specifically consider Kantian ethics and present a multi-sorted quantified modal logic we call the Formula of the Universal Law Logic (FULL). The FULL formalizes Kant's first formulation of the categorical imperative, the Formula of the Universal Law (FUL), and concepts such as causality and agency. We demonstrate on three cases from Kantian ethics that the FULL can reason to evaluate agents' actions for certain purposes without built-in moral intuition, given that it has sufficient (non-normative) background knowledge. Therefore, the FULL is a contribution towards more robust and autonomous AMAs, and a more formal understanding of Kantian ethics.