Recursive Closure Under Intersection

This file proves that recursive languages are closed under intersection.

The proof reuses the existing computability bridge: recursive languages have computable membership predicates, Boolean conjunction composes those deciders, and a total computable Boolean decider yields a recursive language.

theorem is_Recursive_intersection {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] {L₁ L₂ : Language T} (h₁ : is_Recursive L₁) (h₂ : is_Recursive L₂) : is_Recursive (L₁ ⊓ L₂)

Recursive languages over finite, primcodable alphabets are closed under intersection.

theorem Recursive_closedUnderIntersection {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ClosedUnderIntersection is_Recursive

The class of recursive languages is closed under intersection.