Strict Inclusion: Recursive ⊊ RE

This file proves that recursive languages form a strict subclass of recursively enumerable languages.

The proof is indirect. If every RE language over the unary alphabet were recursive, then RE would be closed under complement: move an RE language into Recursive, take the recursive complement, and use Recursive ⊆ RE. This contradicts RE non-closure under complement.

Main declarations

• haltingUnaryLanguage_not_Recursive — the unary halting language is RE but not recursive.
• Recursive_strict_subclass_RE_unit — strict inclusion over Unit.
• Recursive_strict_subclass_RE_of_nonempty — strict inclusion over any nonempty finite alphabet.
• Recursive_subclass_RE_and_exists_strict — class-level inclusion plus a strict witness alphabet.

theorem haltingUnaryLanguage_not_Recursive : ¬is_Recursive haltingUnaryLanguage

The concrete unary halting language is not recursive.

theorem Recursive_strict_subclass_RE_unit : Recursive ⊂ RE

Recursive languages over the unary alphabet form a strict subclass of RE.

theorem Recursive_strict_subclass_RE_of_nonempty {T : Type} [DecidableEq T] [Fintype T] [Nonempty T] : Recursive ⊂ RE

Recursive languages over any nonempty finite alphabet form a strict subclass of RE.

theorem Recursive_strict_subclass_RE_of_card {T : Type} [Fintype T] (hT : 1 ≤ Fintype.card T) : Recursive ⊂ RE

Recursive languages form a strict subclass of recursively enumerable languages over every finite alphabet with at least one symbol.

theorem Recursive_subclass_RE_and_exists_strict : (∀ (T : Type) [DecidableEq T] [Fintype T], Recursive ⊆ RE) ∧ ∃ (T : Type), Recursive ⊂ RE

Recursive languages are included in RE for every finite alphabet, and the inclusion is strict for at least one alphabet.