Trakhtenbrot's theorem

From Wikipedia, the free encyclopedia

In logic (usually computational) and finite model theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable).

[edit] References

• Boolos, Burgess, Jeffrey. Computability and Logic, Cambridge University Press, 2002.
• Simpson, S. "Theorems of Church and Trakhtenbrot". 2001.[1]