Library Decidability


Definition of L-decidability


Definition ldec (P : termProp) :=
   u : term, proc u s, (P s u (tenc s) == true) (¬ P s u (tenc s) == false).

Complement, conj and disj of predicates


Definition complement (P : termProp) := fun t¬ P t.

Definition conj (P : termProp) (Q : termProp) := fun tP t Q t.

Definition disj (P : termProp) (Q : termProp) := fun tP t Q t.


Deciders for complement, conj and disj of ldec predicates


Definition tcompl (u : term) : term := .\"x"; !Not (!u "x").

Definition tconj u v : term := .\"x"; !Andalso (!u "x") (!v "x").

Definition tdisj u v : term := .\"x"; !Orelse (!u "x") (!v "x").


L-decidable predicates are closed under complement, conj and disj


Lemma ldec_complement P : ldec Pldec (complement P).

Lemma ldec_conj P Q : ldec Pldec Qldec (conj P Q).

Lemma ldec_disj P Q : ldec Pldec Qldec (disj P Q).