Leibniz' Project
An ethic is the rule of conduct which tells in each given situation if an action is ethical.
Being given a situation (also named state following the usual terminology in artificial intelligence: see this Wikipedia page for example), an ethic tells if the action is right or wrong in the situation.
Throughout this page, let \(S\) be the set of states and \(A\) the set of actions.
\(\mathbf{Definition}\)
An ethic is a function from \(S ×
A\) to \(\{⊥ ,⊤\}\), where
\(⊥\) is the image for actions
being unethical and \(⊤\) the one
for ethical actions.
Require Import Bool.Bool.
From mathcomp Require Import all_ssreflect.
Context {State : Type}.
Context {Action : eqType}.
Definition Ethic : Type := State -> Action -> bool.