### Abstract

We present a mechanisation of (preference-based) conditional normative reasoning. Our focus is on Åqvist’s system E for conditional obligation and its extensions. We present both a correspondence-theory-focused metalogical study and a use-case application to Parfit’s repugnant conclusion, focusing on the mere addition paradox. Our contribution is explained in detail in [2]. This document presents a corresponding (but sligthly modified) Isabelle/HOL dataset.

### License

BSD License

### Topics

- Logic/Philosophical aspects
- Logic/General logic

### Related publications

- Parent, X., & Benzmüller, C. (2023). Normative Conditional Reasoning as a Fragment of HOL (Version 3). arXiv. https://doi.org/10.48550/ARXIV.2308.10686

### Session CondNormReasHOL

- DDLcube
- mere_addition_opt
- mere_addition_lewis
- mere_addition_max

## Cite

×

CondNormReasHOL-AFP

    @article{CondNormReasHOL-AFP,
      author  = {Xavier Parent and Christoph Benzmüller},
      title   = {Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset)},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/CondNormReasHOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest