Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Normative Conditional Reasoning as a Fragment of HOL

Xavier Parent, Christoph Benzmüller

TL;DR

The paper mechanizes Aqvist's system $E$ for conditional obligation using a shallow semantic embedding in Isabelle/HOL within the LogiKEy framework, enabling both meta-reasoning about correspondences and direct computer-assisted analysis of ethical arguments. It demonstrates automatic verification of correspondences between betterness properties and modal axioms (one-direction) and provides a formal encoded study of Parfit's repugnant conclusion, showing that suitably weakening the transitivity of the 'better than' relation can avoid the paradox under certain evaluation rules. Methodologically, the work combines a thorough semantic setup ($M=(W,\succeq,v)$ with $\bigcirc(\psi/\varphi)$ truth conditions) with robust automation (Sledgehammer, Nitpick) to explore both theory and case studies. The results indicate a practical utility for meta-reasoning and ethics debates, while highlighting limitations and directions for expanding the equivalence between semantic properties and axioms.

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.

Normative Conditional Reasoning as a Fragment of HOL

TL;DR

The paper mechanizes Aqvist's system for conditional obligation using a shallow semantic embedding in Isabelle/HOL within the LogiKEy framework, enabling both meta-reasoning about correspondences and direct computer-assisted analysis of ethical arguments. It demonstrates automatic verification of correspondences between betterness properties and modal axioms (one-direction) and provides a formal encoded study of Parfit's repugnant conclusion, showing that suitably weakening the transitivity of the 'better than' relation can avoid the paradox under certain evaluation rules. Methodologically, the work combines a thorough semantic setup ( with truth conditions) with robust automation (Sledgehammer, Nitpick) to explore both theory and case studies. The results indicate a practical utility for meta-reasoning and ethics debates, while highlighting limitations and directions for expanding the equivalence between semantic properties and axioms.

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.
Paper Structure (21 sections, 5 theorems, 8 equations, 35 figures, 4 tables)

This paper contains 21 sections, 5 theorems, 8 equations, 35 figures, 4 tables.

Table of Contents

  1. Introduction
  2. System E
  3. Language
  4. Semantics
  5. Systems
  6. Correspondences
  7. System E in Isabelle/HOL
  8. LogiKEy
  9. Faithful embedding of system E
  10. Properties
  11. Verifying the correspondences
  12. Max rule
  13. Opt rule
  14. Inclusion
  15. The \ref{['lewis']} truth conditions (Lewis)
  16. ...and 6 more sections

Key Result

Theorem 2.1

(i) E is sound and complete w.r.t. the class of all preference models; (ii) F is sound and complete w.r.t. the class of preference models in which $\succeq$ is limited; (iii) F+cm is sound and complete w.r.t. the class of preference models in which $\succeq$ is smooth; (iv) F+dr is (weakly) soun

Figures (35)

  • Figure 1: Weakenings of transitivity (ddl:parent24)
  • Figure 2: Systems
  • Figure 3: Basic semantical ingredients; propositional and modal connectives
  • Figure 4: Truth conditions
  • Figure 5: Axioms of E (max)
  • ...and 30 more figures

Theorems & Definitions (6)

  • Theorem 2.1: Soundness and completeness, Parent (ddl:P21ddl:parent24)
  • Theorem 2.2: Soundness and completeness, ddl:parent14
  • Theorem 3.1: Faithfulness of the embedding
  • Proposition 5.1
  • Remark 1
  • Corollary 5.2: f.m.p.