117b – Unsolvable problems – Lecture 2

We discussed briefly Church’s and Trakhtenbrot’s theorems: The set of logically valid sentences and the set of sentences valid in all finite models are undecidable. More precisely: If is a language that contains either a binary symbol or the language of arithmetic, then the set of theorems of reduces to the set of validities of , so this set is (r.e. and) undecidable. For the same , we can axiomatize the behavior of a given Turing machine on a given input (by a similar argument to the association of a semi-Thue system to each Turing machine) in such a way that this axiomatization has a finite model iff the machine converges on this input, thus the halting problem reduces to the complement of the set of finite validities, so this last set is (co-r.e. and) undecidable.

We defined Post correspondence systems and showed that the problem of determining whether such a system admits a solution is unsolvable. Two applications to the theory of formal languages follow: There is no algorithm to test whether 2 given context-free grammars have disjoint languages, and there is no algorithm to test whether a given context-free grammar is ambiguous.