Wednesday, May 23, 2007

Topology and verification

Recently one of the older grad students, Kohei Kishida, explained his thesis project to me. He is writing on topological semantics for modal logic. I finally got a grasp on why topologies are good at or useful for representing verification. This came up because Kevin Kelly discusses it in his work connecting computability and the problem of induction. Neat stuff.

The definition of a topology T on a set X is: T is a collection of subsets of X, and (1) the empty set and X are in T, (2) T is closed under arbitrary unions, and (3) T is closed under finite intersection. The pair of X and T is called a topological space. It is really the third condition that makes topologies useful for representing verification. For example, suppose you have verifications (finite proofs or observations) of some formula for all natural numbers. Do you then have a proof of the universally quantified statement? Not if you plan on stringing all the proofs together, taking their conjunction. This will result in an infinitely long proof, but proofs are finite. To see the point in a different way, imagine propositions (in an appropriate topological space) as sets of worlds. Taking the conjunction of propositions is taking their union. Taking the conjunction of infinitely many propositions doesn't guarantee that the conjunction will be in the topology since topologies are not closed under infinite intersection, just finite.

What Kohei pointed out was the following. Tarski and McKenzie proved an equivalence (I'm not sure what the appropriate description is exactly… interpretation? embedding?) between topologies with an interior operation int (a boolean algebra of some sort...) and S4 modal logic. E.g. int(A)\subseteq A is []\phi->\phi, int(A)\subseteq int(int(A)) []\phi->[][]\phi, X\subseteq int(X) is TRUE->[]TRUE, int(A)\cap int(B) \subseteq int(A \cap B) is []\phi & []\psi -> [](\phi & \psi), and so on for the rule of necessitation. But, there is an embedding of intuitionistic logic, which is fairly agreed upon to be good for representing finite proofs/observations in S4, and vice versa. One can give a topological semantics for S4 which models verification. One interesting thing is the relation between the topological semantics for S4 and the Kripke tree semantics for intuitionistic logic. Since we can translate between S4 and intuitionistic logic, we can just look at the structure of the semantics. It turns out that Kripke trees for intuitionistic logic translated to S4 are a certain kind of topological space, a Hausdorff space (I think that was the name), which are closed under arbitrary intersections. (I will double check this.) This means that topological semantics is more general than Kripke semantics. What is the import of this? I've unfortunately forgotten most of what Kohei told me, but he has done a lot of work with Steve Awodey generalizing this stuff to first-order logic. The exciting thing for me was the conceptual connection between verification and topology, which Kohei's work made really clear.

No comments: