Symmetry of Phase Transitions

(sorry, I couldn't find free versions of most of the papers linked to in this post. If you find free versions, please let me know).

One hot research areas of recent times is phase transition phenomena in discrete structures. One of the first examples is that of a random graph. Fix a certain number n of vertices, initially with no edges. Now, add an edge uniformly at random (so you add one of the n(n-1)/2 possible edges , selected at random). Pay attention to a graph property that you like. Let's say the size of the maximally connected subset (that is, the largest subset of the graph such that there is a path between any two vertices). I'll call this the MCS for brevity. Something pretty cool happens when you repeat the process. That is, keep throwing random edges in, keeping track of the size of the MCS. What you will find is that a "phase transition" happens where the MCS suddenly jumps from being very small, to being almost all of the graph. That is, the number of connected components of the graph suddenly decreases. This is very similar to what happens when, say, a liquid transitions to a gas in a physical system, hence the name.

It turns out that these sort of transitions happen in the boolean satisfiability problem also. One example is by tracking the hardness of a problem relative to the clause/variable ratio. A representative publication on this topic is:

Phase Transitions and Backbones of 3-SAT and Maximum 3-SAT. Weixiong Zhang

It turns out that understanding phase transitions may very well be linked to one of my pet topics - symmetries of boolean functions. We look at a slightly different phase transition though.

Say you have a boolean function, f, of n variables. Well, not just any such fundtion. Specifically, f is monotone (so contains no negated atoms) and its automorphism group is transitive. As usual, the automorphism group acts by permuting variables. Now, pick some probability p and assign each variable of f the value 1 independantly with probability p. Let u(p,f) denote the probability that f is satisfied under this assignment. Since u is monotone in p, intervals of values of p pick out a corresponding interval of values of u.

With this in mind, fix some small real e > 0. Define the threshold interval to be the interval [p1,p2] such that u(p1,f) = e and u(p2,f) = 1 - e. In words, this is the interval of probabilities such that f goes from being almost surely unsatisfied to being almost surely satisfied. If this interval is "small", then we have ourselves a phase transition.

Remember that we have some knowledge of how the automorphism group, G, of f acts though. What we do now is to look at the action that G induces on the powerset of variables in f. It turns out that if the orbits of "large" subsets is "large", then the transition interval is small, hence we have ourselves a phase transition. This result crops up in the following paper:

Influences of Variables and Thresholds under Group Symmetries" J. Borgain and G. Kalai.

Now, let us look at what happens in graphs. It turns out that we can be quite general here. A monotone graph property P is one such that if some graph G satisfies P, then every graph on the same set of vertices containing G as a subgraph satisfies P as well. The trick now is to move to something called the Hamming Space and pick out a subset, A, of n points that is "monotone" and is left invariant under some transitive permutation group on that variable set. The threshold interval for A turns out to be very very small indeed. In fact, around O(1/log(n)). From this, one can deduce the same result for montone graph properties. That is, every monotone graph property undergoes a phase transition. That's Cool! This result is contained in:

Every Monotone Graph Property has a Sharp Threshold Ehud Friedgut, Gil Kalai

The natural question then to ask is what the transitive group looks like? In the special case of monotone boolean functions with transitive automorphism group, this amounts asking what the group must be for the function to undergo a phase transition, in the probability sense. Using the usual permutation group trickery, we can answer it for the special case of primitive groups. It turns out that in this case, the group must either be the full alternating or symmetric group on the variable set:

Asymptotic Behaviour of Finite Permutation Groups Acting on Subsets Carmit Benebnisty and Aner Shalev.

Certainly both of these groups satisfy the property that the orbits of "large" subsets are "large", since they both act transitively on the set of k-subsets for any valid k.

Unspeakable Sin

Back when I was an undergraduate and only just starting out on the mathematical path, I learned a fair amount of vector calculus, topology and manifold theory from a rather entertaining (some say peculiar) man named Mike Alder. Now, anyone who believes that reading pure maths notes cannot make you laugh is invited to peruse Mike's manifolds notes (and, yes, that is an aweful lot of stuff for a one semester undergraduate level course). Sadly, he has not made his algebraic topology notes available online.

But this is all besides the point. Mike sometimes moonlights as a writer for Philosophy Now. In one such article, he considers the case of someone he once knew who refused to accept modus ponens as a valid rule of inference. In Mike's words:

"I was pretty clear therefore that Miss B had done something heinous. Whether it merited a prison term I was not quite clear. Maybe it was something where pointing out the error of her ways and deporting her to Australia would be enough. But it was very bad. Immoral if not illegal"

At any rate, it is a rather entertaining article. Those who do not like reading opinionated stuff when the opinion is not their own are hereby warned. If you have the moxy, then go on to read:

The Compleate Logician or Miss Blakemore's Unspeakeable Sin, Mike Alder

Also, picking up on a thread from logicandlanguage.net, Mike has an article available wherein he considers the distinction between science and philosophy and why many scientists try as hard as possible to distance themselves from philosophy. Again, this article comes with a warning for those sensitive to a bit of criticism:

Newton's Flaming Laser Sword or Why Mathematicians and Scientists don't like Philosophy but do it anyway, Mike Alder

At least he 'fesses up and says "You might, just possibly, have been able to detect a touch of intellectual snobbery in this view of philosophy".

Discretely Causal

Physicists have long considered spacetime to consist of a smooth real manifold equipped with a fancy sort of metric. One condition on a spacetime that physicists such as Roger Penrose favour as being "physically reasonable" is global hyperbolicity. What this condition essentially means is that some sort of "global" time coordinate exists. In particular, it makes sense to speak about causality.

Rafael Sorkin initiated the study of causal sets. A causal set is a partially ordered set that is locally finite. That is each set of the form {x : a <= x <= b} is finite:
Spacetime and Causal Sets, Rafael Sorkin.

What is intriguing is that we now have a discrete object, namely a causal set, which in some way encodes information about spacetime. Researchers have extended this in a few different ways. In one direction, one may wonder what a causal set looks like to an observer based at one point of the set:

The internal description of a causal set: What the universe looks like from the inside. Fontini Markapoulou.

The basic thrust of the above paper is that whenever you are at some point in a causal set, you know what events have happened in the past. Then, as you shift around the causal set, the set of events that are in your past changes. Markapoulou characterises this with some simple category theory that is explained very nicely in her paper.

For those familiar with branching temporal logics, such as CTL*, there isn't much new here. Most developments of branching temporal logics assume that the past is linear and that the future is branching. That is, when you stand at a moment in time, there is only one possible history, but many possible futures. An exception is one of the logics in the following paper, which augments CTL(*) with a branching past operator:

Once and for all, Kupferman, O.; Pnueli, A (you or your institution needs an IEEE Explore account to view this paper).

Now, a natural concern is whether the notion of a causal set is intrinsically artificial. That is, given a causal set, is it possible to reconstruct a continuous spacetime? The following paper answers this in the affirmative:

A domain of spacetime intervals in general relativity. Keye Martin and Prakash Panangaden

Martin and Panangaden do something very cool in this paper. Given a spacetime M, and a point x in M, let F(x) be all the points that are in the future of x and reachable by a timelike curve starting at x. Define a partial order on m by x <= y iff y is in F(x). Then, given a countable dense subset of points of some spacetime, together with the "causality relation" (which I have defined via F), we can reconstruct the entire spacetime, topology and all!Super cool! The techniques are based on domain theory, which was introduced by Scott in order to give a semantics to the lambda calculus. What the above paper shows is that techniques developed in theoretical computer science are applicable to something seemingly unrelated: general relativity. One point to note is that they drop the local finiteness condition on the "causal sets". This is because they work with continuous posets (well, bicontinuous posets actually), where one has a sort of interpolation condition on the order, which negates the possibility of local finiteness.

So, what is the global hyperbolicity condition anyway? If we have some spacetime M, then for each p and q in M, let I(p,q) be all the events in M that are in the "causal future" p as well as the "causal past of q". The "Alexandroff topology" (or rather, one topology with that name..) is obtained by taking as a basis all of the sets I(p,q) for p,q in M. We say that M is strongly causal if its Alexandroff topology is Hausdorff, which amounts to saying that its Alexandroff topology is the same as the manifold topology. The spacetime M is globally hyperbolic if it is strongly causal and for all a,b in M, the intersection of up(a) and down(b) is compact in the manifold topology on M. Here, up(a) are all those elements "above" a in the partial order and similarly for down(b).

Along the way, they show that every globally hyperbolic spacetime can be realised as a bicontinuous poset, where the order is the one I defined above. Moreover, the interval topology on the poset is the same as the original manifold topology.

Martin and Panangaden give a very convincing argument for swapping the "local finiteness" condition for a "bicontinuity" condition in the description of a causal set, though they remain diplomatic and don't go so far as to say this. Anyway, it's a pretty cool application of some ideas originally developed for "logic in computer science", so you should check it out!

NotYASS

I have been organising a very informal gathering of assorted riff raff to discuss various things related to maths, logic, philosophy and whatnot. It is called NotYASS (Not Yet Another Seminar Series) and has a shiny new webpage over here. If you find youself in Canberra some time then why not lead a session or just come along for the ride?

Challenge!

Here is a cute problem for you to think about.

Take the fragment of the sequent calculus for propositional logic over one propositional variable that consists of only the rules of weakening and contraction on the left and the right. That is, if the variable is x, then we start from x|-x and all we can do is add an x on either side or delete an x from one side, provided there are at least 2 x's on that side.

A theorem, T, of the system is just something that is derivable using the above rules. The depth of a theorem is the number of inferences in a proof of minimal length for T. For example, x,x |- x,x has depth 2, since the shortest proof is something like:

x |- x
--------
x,x |- x
--------
x,x |- x,x

The challenge is to give precise answers to the following...

Challenge 1 (easy): How many theorems are there of depth n in the above system?
Challenge 2 (trickier): How many theorems of depth n are there when we add cut to the above system?

Note that in the presense of cut, the depth of a proof, P, is defined to be the maximal length of a branch of P and the depth of a theorem, T, is defined to be the minimum depth over all proofs of T.

Also, note that we use an "additive" cut. That is, if we cut V |- x,W and X,x |- Y, we get V,X |- W,Y. Of course, in our case, the letters V,W,X and Y stand for multisets of our propositional variable (x).

If you do not know what cut is, or are rusty on formal proofs in general, then see this post.

Proof normal forms

Normal forms for logical formulae are a simple, yet powerful tool. For instance, it is not hard to show that every propositional formula is equivalent to one which is in conjunctive normal form (CNF), that is a conjunction of disjunctions. This equivalence makes building software for satisfiability testing more streamlined, since one can consider only CNF formulae.

Similarly, one can study normal forms for proofs in sequent systems. For instance, one may assume without any loss of generality that a given proof in classical logic is cut free. This is all well and good, but it still does not give us a firm grip on how the proof behaves.

Considerations like this led Gentzen to his Sharpened Haupsatz or Midsequent Theorem. This theorem states that a proof in predicate logic may be rearranged so that all propositional inferences precede all quantifier inferences. The sequent resulting from the last propositional inference is known as the midsequent.

The midsequent theorem is a rather intuitive result. There is a more general phenomenon at play here, first expounded by Kleene:

Two Papers on the Predicate Calculus. S.C. Kleene. Memoirs of the American mathematical Society 10 (1952).

The first of the two papers concerns permutability of inferences in sequent calculi for classical and intuitionistic logic respectively. From the onset, Kleene works with a cut-free system. Hence, the whole paper may be seen as an exercise in finding out how much we can sharpen the cut elimination theorem. Kleene's first approach is to number each logical and nonlogical symbol appearing in the proof. This is sensible from an algorithmic point of view, as it allows one to trace where each symbol in the end sequent came from. By doing so, we can say slightly more. In particular, it turns out that for each logical symbol in the end sequent, there is only one possible type of inference that could have created it. That is, we can immediately point to a logical symbol in the end sequent and say whether it was introduced by the left or right introduction rule for that symbol.

Kleene's main result is a sort of generalised sharpened Haupsatz. In particular, look at the logical inferences that occur in a given proof of a sequent S. Now, partition this collection into C1, C2,...,Ck however you like, though satisfying a couple of natural conditions. Then, the proof of S can be rearranged so that on each branch no occurence of an inference in class j appears above an occurence of an inference in class i for i < j.

As a special case, we get the midsequent theorem. Quite easily in fact. Start by partitioning the inferences into two classes, the first of which contains all propositional inferences and the second of which all the quantifier inferences. Now, every predicate formula is equivalent to one in prenex normal form, that is, one which looks like Q1Q2...Qn(f) where each Qi is a quantifier and f is quantifier free (i.e. propositional). So, we may assume that the formula is prenex, from whence it is easy to verify the conditions of Kleene's theorem (Of course, by using prenex formulae, it is quite easy to prove the midsequent theorem without appealing to Kleene).