Given a set Σ, often called "alphabet", the set of all strings built from members of Σ is denoted by Σ*. A formal language is a subset of Σ*. If L1 and L2 are formal languages, their productL1L2 is defined as the set of all concatenations of a string w1 from L1 with a string w2 from L2. If L is a formal language and a is a symbol from Σ, their quotientL/a is defined as the set of all strings that can be made members of L by appending an a. Various approaches are known from formal language theory to denote a formal language by a finite description, such as a formal grammar or a finite-state machine. For example, using an alphabet Σ =, the set Σ* consists of all natural numbers, with leading zeroes allowed, and the empty string, denoted as ε. The set Ldiv3 of all naturals divisible by 3 is an infinite formal language over Σ; it can be finitely described by the following regular grammar with start symbolS0: Examples for finite languages are and ; their product yields the even numbers up to 28. The quotient of the set of prime numbers up to 100 by the symbol 7, 4, and 2 yields the language,, and, respectively.
Formal statement of the theorem
Greibach's theorem is independent of a particular approach to describe a formal language. It just considers a set C of formal languages over an alphabet Σ∪ such that
given descriptions of languages L1, L2 ∈ C and of a regular language R ∈ C, a description of the products L1R and RL1, and of the unionL1∪L2 can be effectively computed, and
it is undecidable for any member language L ∈ C with L ⊆ Σ* whether L = Σ*.
Let P be any nontrivial subset of C that contains all regular sets over Σ∪ and is closed under quotient by each single symbol in Σ∪. Then the question whether L ∈ P for a given description of a language L ∈ C is undecidable.
Proof
Let M ⊆ Σ*, such that M ∈ C, but M ∉ P. For any L ∈ C with L ⊆ Σ*, define φ = ∪. From a description of L, a description of φ can be effectively computed. Then L = Σ*if and only if φ ∈ P:
If L = Σ*, then φ = Σ*#Σ* is a regular language, and hence in P.
Else, some w ∈ Σ* \ L exists, and the quotient φ/ equals M. Therefore, by repeated application of the quotient-closure property, φ ∈ P would imply M = φ/ ∈ P, contradicting the definition of M.
Hence, if membership in P would be decidable for φ from its description, so would be L’s equality to Σ* from its description, which contradicts the definition of C.
Applications
Using Greibach's theorem, it can be shown that the following problems are undecidable:
