New Blog on the Spot

For a while I have been wanting to get into the world of blogging. But what to do? I decided that I would follow the formula from John Baez's always interesting "column" This Weeks Finds in Mathematical Physics. That is, I will sporadically speak about stuff that I find interesting. Except, instead of mathematical physics, I'll speak about logic. I will not attempt to cover lots of different areas, merely those bits and pieces that I find interesting. So, it will most likely end up being mainly computational with a twist of mathematical.

Well, let's do something whacky for this first post. I'm going to speak about propositional logic. While many people may believe this to be a completely mined out and somewhat trivial area, this is not so. And no, I am not going to speak about propostitional proof complexity. I am going to speak about something I have been pontificating about for a while - symmetry. What do I mean by symmetry? Well, given a propositional formula, a "symmetry" (henceforth called an automorphism, in keeping with standard mathematical terminology) is any permutation of variables which preserve the valuation. For example, given the formula "a & b", we can swap the symbols a and b without affecting the valuation. The most general symmetry group for a formula of n variables seems to be the group S2 wr Sn, the so-called wreath product of the symmetric group on 2 elements with the symmetric group on n elements. Now, the symmetric group on n elements, Sn, is the collection of all permutations of an n-element set; in our case, the variables. How the wreath product works is like this: the top group (Sn) permutes the variables in the manner in which you would expect. The base group (S2) acts like a "light switch", flipping a variable to be either negative or positive (that is, either negated or not). So, here is the first open problem to chew on:

(OP1) What groups can arise as automorphism groups of propositional formulae?

Certainly, any such group will be a subgroup of our wreath product. We can get Sn for any n - just take the disjunction of n distinct variables (or, in the old language, n literals in such a way that no atom appears more than once). But, what others....?

Lets start having some real fun now. Recall that a formula is said to be in conjunctive normal form (CNF) if it is a conjunction of disjunctions. Given a formula in CNF, we build a "multicoloured graph" as follows: Make a vertex for each clause and one for each literal appearing in the formula. Paint the vertices corresponding to clauses black and the ones corresponding to literals white. Connect a black vertex to a white vertex if the (white) literal appears in the (black) clause. Connect literals to their negations (recall that to connect vertices in a graph, we just draw an edge between them). Then, an automorphism of the resulting graph is defined to be a permutation of the vertices that maps black vertices to black vertices, white vertices to white vertices and edges to edges. With a bit of squinting, we then see:

(1) Finding symmetries of a formula is a subcase of the coloured graph automorphism problem.

From some standard graph theory, we then see:

(2) As n goes to infinity, the probability that a random propositional formula has a trivial automorphism group tends to 1.

Now, the graph automorphism problem (GAP) is one of those black sheep of computational complexity. In other words, we don't have a clue what its actual complexity is. Even the complexity of finding a nontrivial automorphism is not known.

I'll leave the discussion there. There is a lot more I have to say about this area, including some more open problems and some tantalising links to the biggest open problem in theoretical computer science, but I will leave those to sequels if people are interested.