Recursive Closure Under Complement

This file proves that the class of recursive (decidable) languages is closed under complement.

Proof idea: given a TM0 decider (Λ, M, accept) for L that always halts, the complement is decided by (Λ, M, fun q => !accept q) — the same machine with the acceptance predicate negated.

Main results

• is_Recursive_complement — if L is recursive then Lᶜ is recursive.
• Recursive_complement_iff — L is recursive iff Lᶜ is recursive.

theorem is_Recursive_complement {T : Type} {L : Language T} (hL : is_Recursive L) : is_Recursive Lᶜ

theorem Recursive_complement_iff {T : Type} {L : Language T} : is_Recursive Lᶜ ↔ is_Recursive L

A language is recursive iff its complement is recursive.

theorem Recursive_closedUnderComplement {T : Type} : ClosedUnderComplement is_Recursive

The class of recursive languages is closed under complement.