Topology and First-Order Modal Logic

The normal square root function can be considered to be multi-valued.

Let’s momentarily accept the heresy of saying that the square root of a negative number is 0, so that our function will be total.

How can we represent the situation of this branching “function” topologically?

One thing we could do is just take the graph of the multivalued “function” itself in the subspace topology of \mathbb{R}^2, which is topologically just like this:

This has the downside that, at the origin (the place where all three lines meet), it doesn’t really represent the fact that the graph of the original multivalued “function” was the union of two genuine single-valued functions:  There is no neighborhood of the origin which is functional in any way.

But what about this topological space?  (The two filled-in dots represent points which are present in the space, the non-filled-in dot represents a point missing from the space.  The border is not part of the space.)

Here, the open sets are given by a basis consisting of: open sets on either of the three branches: i.e., like this

and this:

and this:

as well as open sets of this form:

and this form:

(Note that this space isn’t Hausdorff!).

This space (call it T) represents the fact that the original graph was the union of two genuine single-valued functions in the following sense:  There is a function, p, from T to the x-axis (i.e., \mathbb{R}) such that for all points y\in T, there is an open set y\in U\subset T such that p restricted to U is a homeomorphism to an open set in \mathbb{R}.  That is, every point in S has a neighborhood such that the inverse of p restricted to that neighborhood is a function.

The space T as defined above is (sort of) a sheaf over \mathbb{R}.  More precisely, it’s an étalé space:  To restate the definition above more generally, an étalé space over a topological space S is a topological space T together with a function p\colon T\to S such that, for all y\in T, there is an open set y\in U\subset S such that p(U) is open and p|_U is a homeomorphism.  In general, for any x\in S, the set p^{-1}(x)\subset T is called the stalk over x.  Note that, as a subspace of T, any stalk is discrete.

As another example along similar lines, gluing the domains of the different branches of the complex logarithm gives rise to a sheaf over \mathbb{C}: (This image is from Wikipedia and is by Jan Homann.)

In this case, T is the space pictured, S is \mathbb{C} (or \mathbb{C}^* = \mathbb{C}-\{0\}), and p is projection along the depicted vertical direction.  Note that this represents how the domains of the various branches of the complex logarithm fit together; this graph is not a depiction of the complex logarithm or any branch of the complex logarithm, which is a function from \mathbb{C} to \mathbb{C}, and thus hard to draw!

The two examples I gave were of natural functions which happen to be multivalued, but there are much more general examples of étalé spaces.  For example, for any topological spaces S and S', there is a sheaf of all continuous functions from S to S'!  The étalé space corresponding to this sheaf would have, for each x\in S, the stalk p^{-1}(x) equal to the set of germs of continuous functions from S to S' at x. (See here for more).

First-Order Modal Logic

And now we’ll switch to a seemingly totally different topic.

A modal logic is a logic that contains an operator \Box, representing necessity, and \Diamond, representing possibility.  If p is a proposition, then \Box p should be interpreted as the proposition “It is necessary that p”, or “p is necessarily true”, and \Diamond p should be interpreted as the proposition “It is possible that p is true”.

The operators \Box and \Diamond are dual to each other: \Box p is equivalent to \neg\Diamond\neg p and similarly \Diamond p is equivalent to \neg\Box\neg p (if you think about it, this actually makes real-life sense, as well as just sense in logic-land!).

There are a number of different axiomatic systems for propositional modal logic; here we’ll just consider S4, which was invented by C. I. Lewis in the early 20th century. It has the following rules:

  1. For all propositions p, \Box p\rightarrow p is a theorem.
  2. For all propositions p, \Box p\rightarrow \Box\Box p is a theorem.
  3. For all propositions p and q, \Box (p\rightarrow q)\rightarrow (\Box p \rightarrow \Box q) is a theorem.
  4. For any proposition p, if p is a theorem, then \Box p is a theorem.  (Note that this does not say that p\rightarrow \Box p is a theorem; if it did, the whole thing would be trivial!).

In the middle of the 20th century, Saul Kripke invented possible-worlds semantics for modal logics.  The idea is that there is a set W of possible worlds and at each possible world w, each atomic proposition A, B,\ldots may hold or not, independently of the other possible worlds.  Furthermore, there is a relation R between possible worlds; wRw' should be interpreted as “World w considers world w' possible”.  The whole setup is called a Kripke frame.

This gives a semantics for modal logic: For any proposition p, \Diamond p holds at a world w if there is some world w' that w considers possible such that p holds at w'.  Similarly, \Box p holds at a world w if p holds at every world w' that w considers possible.

Somebody showed (probably Kripke, but I’m not sure) that the class of Kripke frames where R is reflexive and transitive corresponds to S4, in the sense that all theorems of S4 hold in all such Kripke frames, and everything which holds in all such Kripke frames holds in S4.

Note that the accessibility relation is completely clear-cut and discrete: given a world w, you know exactly what worlds w' it considers possible.  But, interpreting R as a measure of “closeness” of two worlds, observe that topology gives us a more nuanced version of what “closeness” means: we think of the topology on \mathbb{R}, for example, as defining what “closeness” means on \mathbb{R}, even though no two fixed real numbers are actually close to one another!  (At least, they’re not close to one another in any absolute sense.)

It turns out we can incorporate this sense of “closeness” into the semantics for modal logic as well.  We’ll define a topological Kripke model this way: We again have a set W of possible worlds, but instead of defining a relation R between them, we define a topology  on W.  As above, we say, for each possible world w, which of the atomic propositions A,B,\ldots hold at that world.  Note that this is equivalent to defining arbitrary subsets [A],[B],\ldots of W.  In general, we’ll let [p] be the set of worlds at which proposition p holds.  Then we can define [\Box p] to be the interior of [p] and [\Diamond p] to be the closure of [p].  In other worlds, \Box p holds at a world w there is some open set w\in U such that p holds at every world w'\in U, and \Diamond p holds at a world w if for all open sets w\in U there is some w'\in U such that p holds at w'.

It turns out that this semantics, too corresponds to S4, in the sense that all theorems of S4 hold in all topological Kripke models and all propositions which hold in all topological Kripke models are theorems of S4.  (I’m not exactly sure who first came up with this.  I looked at the Wikipedia article and some of its links, but I couldn’t quite figure out who was the first.  It seems Tarski was involved somehow anyway.)

So far, the logics we’ve considered have all been propositional, but you can easily add first-order logic to S4 to get FOS4.  There have been a number of proposals for how to define a semantics for FOS4.  In 2008, Steve Awodey and Kohei Kishida proposed that the right generalization of topological semantics for S4 to first-order semantics for FOS4 was to use étalé spaces!

Here’s an example of how it works.  Consider the following étalé space:

The top space, T, is homeomorphic to \mathbb{R}^+ = \{y\in\mathbb{R}\mid y > 0\}.  The bottom space, S, is the circle S^1.  The projection p is given by p(y) = \langle \cos(2\pi y),\sin(2\pi y)\rangle.

We can put a first-order structure on this étalé space by considering each stalk p^{-1}(x) for x\in S to be a first-order universe, just as when defining regular semantics for first-order logic.

We can define the interpretation of relation symbols, function symbols, and constant symbols more or less arbitrarily:  The only restrictions are that the selection of the interpretation of any particular constant symbol from each stalk must be done in a continuous manner, and there is a similar continuity condition on the interpretation of function symbols.

It will turn out that the interpretation of a formula \phi with free variables v_1,\ldots,v_n will be a subset of T^n, where T^n is the nth fibered product over S of T with itself.  (This just means that, e.g., T\times T is the étalé space where the stalk of any x is p^{-1}(x)\times p^{-1}(x).).  In particular, as in the regular topological semantics, the interpretation of a sentence will be a subset of S.

The crucial step, as before, is that the interpretation of \Box \phi is the interior of the interpretation of \phi, and the interpretation of \Diamond \phi is the closure of the interpretation of \phi, although now the interiors and closures are being taken in the topology of T^n.

To see how this works, suppose that in our example we define the relation \leq on each stalk by restricting the usual ordering \leq on \mathbb{R}^+.  Then it is true in our model that \exists x\forall y\, x\leq y (since it is true in every stalk), but it is not true that \exists x\Box\forall y\, x\leq y.  The reason is that in this stalk:

the red dot is the minimum element of the stalk, but if you push it to the right just a little bit, that’s no longer true.  Intuitively, it’s the minimum element, but not necessarily so.

Awodey and Kishida prove that, as in the other cases, this sheaf semantics corresponds to FOS4 in that every theorem of FOS4 holds in all sheaf models, and everything which holds in all sheaf models is a theorem of FOS4.  (They actually prove something a bit stronger than that.)

Other Uses of Sheaves in Logic

This relationship between sheaves and logic came up relatively recently, but there is a longer and more well-known relationship which I’ll just mention briefly, namely through toposes.  Using topos theory, you can interpret the class of sheaves over a topological space S as a category similar to the category of sets.  The interpretation is actually fairly similar to the interpretation here, but instead of interpreting modal logic, higher-order (non-modal) logic is interpreted.  It turns out that the set of truth values in this interpretation is the set of open subsets of S (whereas in the modal interpretation just given, the truth values could be arbitrary subsets of S).  One of the remarkable things about this is that the set of open subsets of S can itself be interpreted as an étalé space over S, which is what allows the equivalent of power sets to be taken in this category.

For more information on this, see Sheaves in Geometry and Logic.

3 thoughts on “Topology and First-Order Modal Logic

  1. A modal logic is a logic that contains an operator \Box, representing necessity, and \Diamond, representing possibility.

    All right, but isn’t ∀ and &exists; also modal? I guess you are just saying it’s easier to explain if you use the semantics rather than the syntax.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s