Indexed languages are not closed under intersection

Over Bool, the indexed languages

• abnPowM = {(a b^n)^m | n,m > 0} and
• abnAbStarPowPredN = {a b^n (a b*)^(n-1) | n > 0}

intersect in the non-indexed diagonal language abnPowN = {(a b^n)^n | n > 0}. Injective terminal relabelling transports this counterexample to every alphabet containing two distinct symbols.

theorem IndexedIntersectionNonclosure.Indexed_notClosedUnderIntersection : ¬ClosedUnderIntersection is_Indexed

Indexed languages over the binary alphabet are not closed under intersection.

theorem IndexedIntersectionNonclosure.Indexed_notClosedUnderIntersection_of_embedding {α : Type} (e : Bool ↪ α) : ¬ClosedUnderIntersection is_Indexed

An injection of the binary alphabet transports failure of indexed intersection closure to the target alphabet.

theorem IndexedIntersectionNonclosure.Indexed_notClosedUnderIntersection_of_two {α : Type} (a b : α) (hab : a ≠ b) : ¬ClosedUnderIntersection is_Indexed

Indexed languages are not closed under intersection over any alphabet containing two specified distinct symbols.

theorem IndexedIntersectionNonclosure.Indexed_notClosedUnderIntersection_of_card {α : Type} [Fintype α] (hα : 2 ≤ Fintype.card α) : ¬ClosedUnderIntersection is_Indexed

Indexed languages are not closed under intersection over any finite alphabet with at least two symbols.