# Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories

## TL;DR

This paper demonstrates how higher-order (meta-)logic, specifically Church's type theory, can be used to represent and automate complex ethical theories like Gewirth's Principle of Generic Consistency, incorporating modalities, indexicals, and higher-order quantification.

## Contribution

It introduces a novel approach using Church's type theory as a meta-logic to encode and reason with complex ethical theories featuring advanced logical constructs.

## Key findings

- Successful semantic embedding of complex ethical theories
- Automated reasoning with intricate logical features achieved
- Pushes boundaries in knowledge representation and ethical reasoning

## Abstract

The computer-mechanization of an ambitious explicit ethical theory, Gewirth's Principle of Generic Consistency, is used to showcase an approach for representing and reasoning with ethical theories exhibiting complex logical features like alethic and deontic modalities, indexicals, higher-order quantification, among others. Harnessing the high expressive power of Church's type theory as a meta-logic to semantically embed a combination of quantified non-classical logics, our work pushes existing boundaries in knowledge representation and reasoning. We demonstrate that intuitive encodings of complex ethical theories and their automation on the computer are no longer antipodes.