Definition complement {X} (P : X Prop) := x : X P x.
Definition reflects (b : bool) (p : Prop) := p b = true.

Definition decider {X} (f : X bool) (P : X Prop) : Prop :=
   x, reflects (f x) (P x).
Definition decidable {X} (P : X Prop) : Prop :=
   f : X bool, decider f P.

Definition enumerator {X} (f : option X) (P : X Prop) : Prop :=
   x, P x n, f n = Some x.
Definition enumerable {X} (P : X Prop) : Prop :=
   f : option X, enumerator f P.

Definition semi_decider {X} (f : X bool) (P : X Prop) : Prop :=
   x, P x n, f x n = true.
Definition semi_decidable {X} (P : X Prop) : Prop :=
   f : X bool, semi_decider f P.

Definition reduction {X Y} (f : X Y) (P : X Prop) (Q : Y Prop) :=
   x, P x Q (f x).
Definition reduces {X Y} (P : X Prop) (Q : Y Prop) :=
   f : X Y, reduction f P Q.
Notation "P ⪯ Q" := (reduces P Q) (at level 70).