Library Decidability

Definition of L-decidability

Definition ldec (P : term → Prop) :=
∃ 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 : term → Prop) := fun t ⇒ ¬ P t.

Definition conj (P : term → Prop) (Q : term → Prop) := fun t ⇒ P t ∧ Q t.

Definition disj (P : term → Prop) (Q : term → Prop) := fun t ⇒ P 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 P → ldec (complement P).

Lemma ldec_conj P Q : ldec P → ldec Q → ldec (conj P Q).

Lemma ldec_disj P Q : ldec P → ldec Q → ldec (disj P Q).