Normative Conditional Reasoning as a Fragment of HOL

TL;DR

This paper presents a mechanization of preference-based conditional normative reasoning within HOL, enabling automated verification of deontic properties and ethical paradoxes, with implications for ethical argument assessment.

Contribution

It introduces a shallow semantical embedding of Aqvist's system E in Isabelle/HOL, facilitating meta-reasoning and ethical argument analysis in normative logic.

Findings

Automated verification of deontic correspondences.

Formal encoding of Parfit's repugnant conclusion.

Insights into weakening transitivity in ethical reasoning.

Abstract

We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The equivalence is automatically verified in one direction, leading from the property to the axiom. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox (or impossibility theorem) in population ethics, Parfit's repugnant conclusion. While some have proposed overcoming the impossibility theorem by abandoning the presupposed transitivity of ''better than'', our formalisation unveils a less extreme approach, suggesting among other things the option of weakening transitivity suitably rather than discarding it entirely. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.