Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL

TL;DR

This paper presents a faithful embedding of a dyadic deontic logic into classical higher-order logic, enabling automated reasoning within existing theorem provers and proof assistants.

Contribution

It introduces a sound and complete semantical embedding of dyadic deontic logic in HOL, providing a foundation for automation and implementation.

Findings

Embedding is proven sound and complete

Facilitates automation in higher-order theorem provers

Provides theoretical foundation for dyadic deontic logic in HOL

Abstract

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants.