Leibniz' Project
Being given a situation (also named state following the usual terminology in artificial intelligence: see this Wikipedia page for example), an ethic tells if a given action is right or wrong.
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.
Let \(E = {\{⊥ ,⊤\}}^{S × A}\) be
the set of ethics.
Context {State : Type}. Context {Action : Type}. Definition Ethic : Type := State -> Action -> bool.
variable {State : Type} variable {Action : Type} def Ethic : Type := State -> Action -> Bool
An ethic is more restrictive than an other if all the actions it allows are also allowed by the other.
\(\mathbf{Definition}\)
An ethic \(e_1 \in E\) is said
more restrictive than \(e_2 \in
E\) in a state \(s \in S\)
if \(\forall a \in A, e_1(s, a) = ⊤
\rightarrow e_2(s, a)\).
And \(e_1\) is said strictly more
restrictive than \(e_2\) in a
state \(s \in S\) if \(e_1\) is more restrictive than \(e_2\) and \(\exists a \in A, e_1(s, a) = ⊥\) and
\(e_2(s, a) = ⊤\).
Obviously, every ethic is more restrictive than itself and is not strictly more restrictive than itself.
Definition more_restrictive (e1 e2 : Ethic) (state : State) : Prop := forall (action : Action), e1 state action = true -> e2 state action = true. Definition strictly_more_restrictive (e1 e2 : Ethic) (state : State) : Prop := more_restrictive e1 e2 state /\ exists (action : Action), e1 state action = false /\ e2 state action = true. Lemma every_ethic_more_restrictive_than_itself (state : State) : forall (e : Ethic), more_restrictive e e state. Proof. unfold more_restrictive. intros. exact H. Qed. Lemma no_ethic_strictly_more_restrictive_than_itself (state : State) : forall (e : Ethic), ~ strictly_more_restrictive e e state. Proof. unfold strictly_more_restrictive. unfold not. intros. destruct H. destruct H0. destruct H0. rewrite H1 in H0. inversion H0. Qed.
def more_restrictive (e1 e2 : @Ethic State Action) (state : State) : Prop := ∀ (action : Action), e1 state action = true -> e2 state action = true def strictly_more_restrictive (e1 e2 : @Ethic State Action) (state : State) : Prop := more_restrictive e1 e2 state ∧ ∃ (action : Action), e1 state action = false ∧ e2 state action = true
A void ethic allows every action. An ethicless person has a void ethic. The void ethic is the least restrictive of all.
\(\mathbf{Definition}\)
The void ethic is \[\begin{align*}
S × A &\to \mathbb \{⊥ ,⊤\}\\
(s, a) &\mapsto ⊤
\end{align*}\]
Obviously, every ethic is more restrictive than the void ethic.
Definition ethicless : Ethic := fun (s : State) => fun (a : Action) => true. Lemma ethicless_least_restrictive (e : Ethic) (state : State) : more_restrictive e ethicless state. Proof. unfold more_restrictive. unfold ethicless. intro. reflexivity. Qed.
def ethicless : @Ethic State Action := fun state => (fun action => true)