Context-Free Non-Closure Under Complement

This file derives failure of closure under complement from the corresponding intersection result.

Counterexample idea: if CFLs were closed under complement, then together with closure under union they would also be closed under intersection by De Morgan's law. This contradicts the explicit non-closure result for intersection.

Main declarations

• nnyCF_of_complement_CF

theorem nnyCF_of_complement_CF : ¬∀ (L : Language (Fin 3)), is_CF L → is_CF Lᶜ

The class of context-free languages isn't closed under complement.

theorem CF_notClosedUnderComplement : ¬ClosedUnderComplement is_CF

Context-free languages over Fin 3 are not closed under complement.

theorem CF_notClosedUnderComplement_of_three {α : Type} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : ¬ClosedUnderComplement is_CF

Context-free languages are not closed under complement for any type with at least 3 elements. That is, as long as α has at least 3 distinct elements, not all complements of context-free languages over α are context-free.

theorem CF_notClosedUnderComplement_of_card {α : Type} [Fintype α] (hα : 3 ≤ Fintype.card α) : ¬ClosedUnderComplement is_CF

Context-free languages are not closed under complement for any finite alphabet with at least three symbols.