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.
This entry was posted on Friday, March 2nd, 2007 at 2:11 pm and is filed under 117b: Computability theory. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.
A kind of library 