Nice finite model theory course notes

I have recently found nice introductory course notes on finite model theory. You can find it here. Thanks to the author for making the notes publicly available.

No compactness in finite model theory

The compactness theorem for first-order logic is indisputably the most fundamental theorem in model theory. It says that

A theory has a model iff every finite subset of it has a model

I will say no more about the usefulness of this theorem in model theory. But what I will speak about now is the failure of compactness in finite model theory, as I already remarked before.

In finite model theory (FMT), we are only concerned with finite structures. Hence compactness theorem in FMT would read

A theory has a finite model iff every subset of it has a finite model


It is easy to conjure a counterexample for this statement. Consider the first-order theory `T` over the empty vocabulary containing sentences of the following form (for all `k >= 2`):

`S_k = EE x_1,...,x_k( x_1 != x_2 ^^ x_1 != x_3 ^^ cdots ^^ x_{k-1} != x_k )`

It is easy to see that every subset `T'` of `T` has a finite model; if `n` is the largest integer such that `S_n in T'`, then the structure containing `n` elements satisfies `T'`. It is also easy to see that `T` has no finite model. (QED)

Likewise, many other fundamental theorems in model theory, such as Craig Interpolation Theorem, are also casualties of finitization (more on this later); Ehrenfeucht-Fraisse games being the only general tool available for proving inexpressibility results in finite model theory.

Finite Model Theory: Preliminaries (2)

We now focus on a very important concept in finite model theory: `k`-ary queries. In fact, one goal of finite model theory is to establish a useful, if possible complete, criterion for determining expressibility (ie, definability) of a query in a logic (such as, first-order logic) on finite structures. For example, we may ask if the query connectivity for finite graphs, which asks whether a finite graph is connected, is expressible in first-order logic. The answer is 'no', though we won't prove this now. [Curious readers are referred to Libkin's Elements of Finite Model Theory or Fagin's excellent survey paper.]

We shall start by recalling the notion of homomorphisms and isomorphisms between structures. Given two `sigma`-structures `fr A` and `fr B`, a homomorphism between them is a function `h: A -> B` such that `h(c^{fr A}) = c^{fr B}` for every constant symbol `c in sigma`, and `h(bb a) := (h(a_1), ..., h(a_r)) in R^{fr B}`, for every `r`-ary relation symbol `R in sigma` and `bb a := (a_1,...,a_r) in R^{fr A}`. So, homomorphisms are tuple-preserving functions (here, think of a tuple as an `r`-ary vector prepended by an `r`-ary relation symbol, eg, `R(1,2,3)`). Now isomorphisms are basically bijective homomorphisms whose inverse are also homomorphisms. Intuitively, this means that two isomorphic structures are the same after relabeling the elements of the universe in one of these structures. We write `fr A ~= fr B` to denote that `fr A` and `fr B` be isomorphic.

Now we define what we mean by queries. Fix a vocabulary `sigma` and a class `cc M` of (not necessarily all) finite `sigma`-structures. This class `cc M` will be referred to as a ground set. Now, for `k >= 0`, a `k`-ary query `cc Q` is a function associating each `fr A in cc M` to a subset of `A^k` such that `cc Q` is closed under isomorphisms, ie, whenever `h: A -> B` is an isomorphism, we have `h( cc Q(fr A)) = cc Q(fr B)`. Now this query `cc Q` is said to be expressible (or definable) in a logic `L` over `cc M` if there exists a `L`-formula `phi` over `sigma` with `k` free variables such that for every `fr A in cc M`, `cc Q(fr A) = phi(fr A)` where

`phi(fr A) := { (a_1,...,a_k) in A^k : fr A |= phi(a_1,...,a_k) }`.

Whenever `cc M` be the set of all finite structures, we shall omit mention of `cc M`.
An important special case occurs when `k = 0`. Such queries are normally called boolean queries or just properties. In this case, the image of `cc Q` can only be either a singleton `{()}` containing the trivial tuple `()`, or the empty set `O/`. We will identify `{()}` with `true` and `O/` with `false`. So, a property `cc Q` is expressible in a logic `L` over `cc M` if there exists an `L`-sentence `phi` over `sigma` such that `cc Q(fr A) = true` iff `fr A |= phi`, for each `fr A in cc M`. Examples of boolean queries (for finite graphs) are:

• Hamiltonian: `cc Q(fr G) = true` iff the graph `fr G` is hamiltonian.
  
• Self-loop: `cc Q(fr G) = true` iff the graph `fr G` has a self-loop (ie, `fr G |= EE x( E(x,x))`).
  
• Isolated: `cc Q(fr G) = true` iff the graph `fr G` has an isolated vertex.
  
• Connected: `cc Q(fr G) = true` iff the graph `fr G` is connected.
  
• Acyclic: `cc Q(fr G) = true` iff the graph `fr G` is acyclic.
  

An example of 2-ary queries is the transitive closure query of finite graphs:

`Q: fr G |-> { (a,b) in G^2 : text{there exists a path from } a text{ to } b text{ in} fr G }`


Question: which of the above queries are expressible in first-order logic? Well, we already saw that Self-loop is expressible in first-order logic. So, it is enough to exhibit a first-order formula to show that a query be expressible in first-order logic. But how do we prove first-order inexpressibility results? In classical model theory, we have tools like compactness and Lowenheim-Skolem theorems for proving first-order inexpressibility. However, most of these tools including the two afore-mentioned theorems fail to "work" in the finite. The only one result that survives is the Ehrenfeucht-Fraisse games (a good exposition of the result can be found here). [Incidentally, does this imply that finite model theory is more difficult than classical model theory?] The games, for example, can be used to prove that the queries Hamiltonian, Connected, Acyclic, and Transitive Closure are not definable in first-order logic. These results will be discussed in subsequent postings.

Finite Model Theory: Preliminaries (1)

I realize that in the previous postings I haven't been as precise as I can possibly be. It's all about to change: we shall now fix terminologies for our subsequent discussion on finite model theory. We will however have to divide this "section" into two postings, as it is too long for one. We shall also assume that the reader knows basic facts from mathematical logic (see Enderton's A Mathematical Introduction To Logic).

We can start by discussing what finite model theory is. One common definition for finite model theory is the model theory of finite structures. Precise, but perhaps too succinct. What makes it different from classical model theory? Finite model theory is primarily concerned with finite structures, while model theory with both finite and infinite structures. Hence, one can expect that the definitions used in finite model theory are very similar to those in classical model theory. The restriction to finite structures is necessary for studying computers and computation due to their finite nature. Note also that finiteness doesn't necessarily imply triviality. For example, witness that (finite) graph theory is a deep, rich, and beautiful subject, which has captivated brilliant mathematicians from many generations including Euler and Erdos.

Unless otherwise stated, we shall make the following assumptions in subsequent postings on finite model theory:

• Every vocabulary and structure is relational, ie, has no function symbols and functions.
  
• Every vocabulary has finitely many (constant and relation) symbols.
  
• Capital Fraktur fonts are used to denote structures; their corresponding letters in Latin correspond to their universes. For example, a structure `fr A` has universe `A`.
  

I am going to adopt an extremely useful definition of expansion of structures from Libkin's Elements of Finite Model Theory, which will allow us to convert back and forth between formulas and sentences. Let `fr A` and `fr A'` be structures over, respectively, `sigma` and `sigma'` where `sigma nn sigma' = O/`. The expansion of `fr A` by `fr A'`, denoted by `(fr A,fr A')`, is the `sigma uu sigma'`-structure with all symbols from `sigma` interpreted according to `fr A`, and from `sigma'` interpreted according to `fr A'`. An important special case is when `sigma'` be the vocabulary `sigma_n` containing only constant symbols `c_1,cdots,c_n`. In this case, if `fr A' = (a_1, cdots, a_n)` (with `a_i` interpreting `c_i`), we can omit some redundant brackets and write `(fr A, fr A') = (fr A, a_1, cdots, a_n)`. We have the following lemma:

Lemma: Suppose `phi(x_1, cdots, x_n)` be a `sigma`-formula, and `fr A` be a `sigma`-structure. Let `Phi` be the formula `phi(c_1/x_1,cdots,c_n/x_n)`, ie, each occurence of `x_i` is replaced by a brand new constant symbol `c_i`. Then, we have: `fr A |= phi(a_1,cdots,a_n)` iff `(fr A,a_1,cdots,a_n) |= Phi`.

Finally, we need to define the notion of `k`-ary queries, which we will do in the next posting.

The Unusual Effectiveness of Logic in Computer Science

A couple of days ago I found a non-technical logic-in-computer-science paper in my folder of unused papers that has turned out to be a highly interesting read. The paper is:

On the Unusual Effectiveness of Logic in Computer Science by Halpern, Halper, Immerman, Kolaitis, Vardi, and Vianu

The authors of these papers are well-renowned authorities in the area of logic in computer science, each with his own enormous contribution to the area.

Here is a summary of the paper. The authors start by mentioning two attempts of explaning the unreasonable effectiveness of mathematics in natural sciences by E.P. Wigner, a Nobel Laureate for Physics, and R.W. Hamming, an ACM Turing Award (which can be construed as the Nobel Prize for Computer Science) winner. In their separate papers, Wigner and Hamming give a number of examples supporting his argument, but conclude that the question "Why is mathematics so unreasonably effective" remains open. The above paper by Halpern et al. is basically an attempt to answer the question "why logic is so effective in computer science". Like Wigner and Hamming did, Halpern et al. give a number of examples supporting their assertion:

• Example 1: Descriptive Complexity. The reader should know roughly what this is by now.
  
• Example 2: Logic as a Database Query Language. This area is devoted to the study of abstract query languages in database theory. Examples of abstract query languages are relational calculus (equivalent to first-order logic), and conjunctive queries (see here for a definition).
  
• Example 3: Type Theory in Programming Language Research. Type theory is often used for building useful type systems for strongly-typed programming languages including Haskell (the computer science reader should know that C, for example, is not strongly-typed).
  
• Example 4: Reasoning about Knowledge. You may think of this area as "the theory of agents". Reasoning about knowledge plays a key role in burgeoning computer science fields including distributed computing, game theory, and AI.
  
• Example 5: Automated Verification in Semiconductor Designs. The meaning is self-explanatory.
  

Aside: I would love to see proof complexity and bounded arithemetic discussed in this paper.

Incidentally, Halpern et al. make a very interesting remark in their paper --- that logic seems more connected to computer science than to mathematics. To a theoretical computer scientist like myself, this claim is so conspicuous. I'm curious whether philosophers and/or mathematicians and/or logicians think so too ...

MathML

Recently I said that a good logic blogger needs to learn something like MathML. Well ... I have just taken a first step in this direction: enable the MathML mode on this website.

Also, I have just recently found ASCIIMathML, thanks to a posting in Andrej Bauer's blog. This script allows you to write math formulas in a LaTeX-like notation. This takes away the burden of learning MathML.

If your browser cannot display MathML, then here is a suggestion (look at 'system requirements' section).

What the tortoise said to achilles

Howdy! Today I am pleased to learn that somebody is actually reading my blog and has left some useful and encouraging comments. Thanks to all who have participated.

One of the good comments I received was a reference to What The Tortoise Said to Achilles by Lewis Carrol, in response to my question in the previous posting whether logicians have a sense of humor. Incidentally, my hunch says I've seen this article in Douglas Hofstadter's excellent Godel, Escher, Bach: An Eternal Golden Braid.

Anyway, on with the story. Basically, Carrol's article contains a clever and well-constructed argument that reasoning is impossible without using an infinite series of modus ponens. I personally feel this argument itself already shows that logicians are humorous (well ... more precisely, logically humorous). I leave the reader to ponder whether Carrol's article shows that logicians have a sense of humor.

Oh, incidentally, I was quite surprised to learn the well-renowned 'Alice's Adventures in Wonderland' is also written by Lewis Carrol, a logician. Wow!

How to be a good blogger

Having just started my own blog, I have recently been thinking about what one needs to do to be a good math/logic blogger. After some serious meditations, I realize that this question is equivalent to 'how to make a fine piece of math/logic writing', whose answers can be found in books like Mathematical Writing by Donald Knuth et al. Nevertheless, there are some additional, but equally important, things that good bloggers need to do:

1. Be controversial.
   
2. Utilize the ability to hyperlink (preferrably to free online resources).
   
3. Learn how to use MathML. Here is a seemingly good
   tutorial (I haven't perused this meticulously enough though). If you already know LaTeX and are using a Unix-like OS, you may want to use Ttm to convert LaTeX to MathML.
   
4. Lastly, having just a bit of sense of humor doesn't hurt. I wonder though if logicians have a sense of humor?
   

I guess I have hitherto successfully and continuously violated every single one of these tips (Oops). Ah well ... I guess there is still tomorrow.

Unary-conjunctive-view Query Language (1)

Last December I completed my BSc(Honours) degree, the Australian equivalent of American BSc degree, at the University of Melbourne (Australia). So, before I am leaving for North America for graduate studies, I thought it might be a good idea to write something about the finite-model-theory related problem I worked on for my undergraduate thesis. It might also be a good topic to get this blog started.

The story is somewhat lengthy. So, I will divide it into a series of bite-size chunks.

To get under way, recall that pure first-order logic is undecidable. [When we say that a logic is (un)decidable, we mean that its satisfiability problem is (un)decidable.] Here pure first-order logic basically consists of all first-order sentences without equality and function symbols. Turing proved this by reducing the halting problem for Turing machines to deciding the satisfiability of first-order logic. We know on the other hand that pure monadic first-order logic (MFO) is decidable, actually complete for NEXPTIME. Here the term 'monadic' simply means that the relation symbols in each formula in MFO are of arity 1. This decidability result actually lies at the border of the decidable and the undecidable because permitting merely one binary relation symbol to MFO immediately results in undecidability.

So, the question boils down to how much more can we extend MFO before we get an undecidable logic? Strictly speaking, this is not really a mathematical question, and so has no single correct answer. I'll mention three known successful attempts to extend the decidability of MFO:

• MFO with equality. Lowenheim, who proved the decidability of MFO, proved this too.
  
• MFO with any number of function symbols. This is Lob-Gurevich theorem.
  
• MFO with equality and one function symbol. This is proved by Rabin in one of his groundbreaking papers.
  

All of these results are optimum. For example, adding one more function symbol to the third logic in this list results in undecidability. For more information on these logics, the reader is referred to the reference book for the classical decision problem. We will however explore a different avenue to answer this question.

Database theorists often talk about conjunctive queries: pure first-order formulas that can be written as

$F(x_1,\dots ,x_n):=(\exists y_1,\dots ,y_k)(R_1(u_1)\wedge \dots \wedge R_m(u_m))$

where the x's are the free variables, the y's are the bound variables, and the u's are tuples of variables appropriate for the (arities of the) R's. Following notations from logic programming, we will write the formula F as

$F(x_1,\dots ,x_n)\leftarrow R_1(u_1),\dots ,R_m(u_m)$

The set of all these F's forms the conjunctive query language. Now, it is easy to see that any conjunctive query is satisfiable --- so its satisfiability problem is trivial. Here is the twist. We can combine MFO and a restricted version of conjunctive query language to make a decidable logic.

Let U be the set of all conjunctive queries with exactly one free variable (a.k.a. unary conjunctive queries). We call U a view vocabulary (signature). Let UCV be the smallest set that satisfies the following conditions:

• U is a subset of UCV.
  
• UCV is closed under boolean operations and first-order quantifications.
  

The Unary-Conjunctive-View query language is the logic UCV. To get a feel for UCV, let us start speaking in it. For example, this logic can assert the following graph-theoretic sentence "any vertex has a 4-walk but no self-loop". How? Consider the following two conjunctive queries:

• ${\mathrm{CW}}_4(x_0)\leftarrow E(x_0,x_1),E(x_1,x_2),E(x_2,x_3),E(x_3,x_4)$
  
• $\mathrm{Loop}(x)\leftarrow E(x,x)$
  

Then, the desired sentence is $AA x ( text{CW_4}(x) ^^ not text{Loop}(x) )$. We can readily see that this logic is quite expressive as it permits any number of relation symbols of any arity. This also shows that UCV is strictly more expressive than MFO and the conjunctive query language, considered individually. Nonetheless, the logic is much less expressive than the first-order logic. For example, UCV cannot even assert simple query like "there exists a path (ie, walks where none of the vertices are visited twice) of length k", for any fixed k > 0. [We'll prove this later.]

In the next posting, I will sketch a proof that UCV is decidable, actually solvable in 2-NEXPTIME but is NEXPTIME-hard. Our proof taps into the fact that UCV has the bounded model property, i.e., every satisfiable query Q in UCV has a model of size at most f(|Q|) for some computable function f:N->N where |Q| denotes the size of the encoding of Q. Note that bounded model property immediately implies decidability in SPACE(f(|Q|)), assuming that f is a proper complexity function, as a Turing machine can start by computing f(|Q|), enumerate every possible structure A appropriate for Q one-by-one, and for each A test whether A satisfies Q (which can be also be done in SPACE(f(|Q|)) ).

Later on we will explore the expressive power of UCV and a general method for proving inexpressibility in UCV.

Welcome to Logicomp!

Hello all! Throughout the past two years, I have learned a lot from Lance Fortnow's successful complexity blog. Professor Fortnow has been an excellent blogger, and kept his avid readers informed on the lattest and the must-know about complexity theory. His blog was certainly one of the things that got me interested in complexity theory, and will continue inspiring me in the future.

Although Professor Fortnow's blog covers many topics in complexity theory, it is a pity that the blog rarely touches on the elegant connection between logic and complexity theory, which --- God knows why --- many finite model theorists think will be a key to proving that P does not equal NP. For example, here are some deep results in the area:

1. Fagin's theorem: the set of properties of (relational) finite structures expressible in existential second-order logic (ESO) coincides with NP.
   
2. Dual Fagin's theorem: the set of properties of finite structures expressible in universal second-order logic (ASO) coincides with co-NP.
   
3. The set of properties of finite structures expressible in second-order logic (SO) coincides with PH.
   

So, in order to prove that P does not equal NP, it suffices to prove that the set of properties of finite structures expressible in ESO is different from that expressible in ASO. In fact, to prove this it is enough to show that the property 3-colorability is not expressible in ASO on the class of finite graphs. That is, we have reduced an important problem in complexity theory to a problem in finite model theory. The area of theoretical computer science that explores the connection between finite model theory and complexity theory is called descriptive complexity.

In view of these, I thought it would be a good idea for me to start a blog that aims to explore the deep connection between logic and complexity. Nonetheless, I realize that it is a formidable task to be a good blogger even for a small subarea of logic and complexity, especially for a newbie like myself. Thus, I will try to focus on areas that I will explore during my graduate studies: (finite and infinite) model theory and descriptive complexity, proof complexity, and perhaps bounded arithmetic. [Nonetheless, I will probably have to every now and then violate this rule and speak about other things that I find interesting and fun.] So, from now on, when I speak about 'Logic and Complexity', I will be referring to these subareas. There are already excellent blogs that cover logic, like this one maintained by Professor Restall at The University of Melbourne's Department of Philosophy, and logic and computation, like this one. However, none of these cover the stuff that I plan to talk about here such as finite model theory and descriptive complexity.

Anyway, for a starter, I plan to write a concise introduction to finite model theory that other mathematical readers, who know a bit of logic, can read. I will try to post this bit-by-bit every week. Any other ideas? Feel free to comment.