Some time ago I promised to make a series of postings on "My Favourite Logic of The Month" every month starting from September 2005. Well, here we officially start until we run out of "nice" logics.
Why first-order logic (FO)? It is the simplest non-trivial logic that we can use to express many mathematical statements. In fact, it is believed that first-order set theory is sufficient to axiomatize mathematics. Besides, most of you have already been exposed to FO, which will make my task much simpler. If any terminologies here sound obscure, check out preliminaries.
We will take a look at three aspects of FO: (1) the problem of testing satisfiability and finite satisfiability, (2) model-checking, and (3) expressive power. I am trying to cover topics that hopefully satisfy finite model theorists, and other logicians. In this posting, I will only speak about (1), saving the other two for some time next week.
Satisfiability: given an FO formula, test whether it is satisfiable. Well, what can we say about this problem with respect to FO? It is undecidable (actually r.e.-complete) [correction: complete for co-r.e, thanks to Richard Zach.]; this is a well-known result proven by Turing, which shattered Hilbert's dream to axiomatize mathematics. If you're into this kind of problem, check out the following book
The Classical Decision Problem by Grädel et al.
Actually, many fragments of FO are decidable, but most are provably intractable. The most complicated such result that I know of is Rabin's result of the decidability of monadic second order theory of infinite binary tree. [Whatever this means, but we may want to delve into this awesome result in the near future.] Although decidable, the problem has non-elementary complexity.
Finite Satisfiability: given an FO formula, test whether it has a finite model. I believe that this problem, if decidable, has more practical applications, e.g., databases. Unfortunately, this problem is also undecidable (actually complete for co-r.e.) [correction: complete for r.e.]. This result is due to Trakhtenbrot. Combining this result and that satisfiability is complete for co-r.e., we can readily imply that completeness theorem, which says that satisfiability is r.e. [correction: satisfiability is co-r.e., thanks to Richard Zach.], fails in the finite. Trakhtenbrot's result in fact marks the beginning of finite model theory. Later on, Fagin proved a logical characterization of NP with a technique that is "isomorphic" to that used to prove Trakhtenbrot's theorem (see this page). For more on finite satisfiability of FO, see Libkin's Elements of Finite Model Theory.
2 comments:
…completeness theorem, which says that satisfiability is r.e.
That should be "co-r.e.", i.e., validity is r.e.
Richard, you are right ... corrections have been made.
Post a Comment