Worrying About 2-Logic

March 6, 2008

Posted by David Corfield

$MathML-enabled post (click for more details).$

Here’s a possible problem for the idea of modal logic as 2-logic.

In ordinary first order logic a model of a theory is a set $X$ . To an $n$ -ary predicate of the theory we assign a subset of $X^n$ , to a constant an element of $X$ , and so on.

For a given $X$ , we can derive a Galois correspondence between theories modelled on $X$ and subgroups of $X !$ , the permutations of $X$ , as Todd shows.

Now, in first order modal logic (FoS4) a model of a theory is a sheaf. To show completeness we can stick with bog standard sheaves on topological spaces, as Awodey and Kishida show in their paper Topology and Modality. This combines the topological semantics of propositional modal logic with the set-valued semantics of first-order logic. Necessity relates to taking the interior of subsets of the base space.

$MathML-enabled post (click for more details).$

So here’s the problem: if groups measured the symmetries of a model of first order logic, we want 2-groups to measure the symmetries of a model of 2-logic. But what are the symmetries of a sheaf? Well a sheaf is a functor, so we’d expect the symmetries to be the group of invertible natural transformations from the functor to itself, or sheaf automorphisms. Where’s the 2-group?

[Where do sheaves of groups fit in?]

Or is this the wrong way to think of it? Is it possible that we should be ‘permuting’ the base space too, as was suggested at some point in the Klein 2-geometry programme.

But why not look more directly for the kind of theory which has a category/groupoid $C$ as a model? And which interprets an $n$ -ary predicate as a functor from $C^n$ to Set, and so on.

I’m not sure why but the question popped into my head as to whether there’s any interest in the symmetries of a topos. E.g., what’s AUT(Set) and AUT(Sh( $X$ ))?

Posted at March 6, 2008 11:28 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1623

20 Comments & 0 Trackbacks

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

I think AUT(Set) is trivial. More precisely, if we define AUT(Set) as the category whose objects are equivalences $Set \to Set$ and whose maps are natural transformations, then I think AUT(Set) is equivalent to the terminal category.

I haven’t gone through this in detail, but the idea is as follows. Any automorphism (i.e. self-equivalence) $G$ of $Set$ preserves both terminal objects and sums. Since every object of $Set$ is a sum of copies of the terminal object, $G(X) \cong X$ for all sets $X$ . Moreover, there’s a canonical choice of such an isomorphism for each $X$ . “And so on.”

I don’t think it’s going to make much difference if you consider geometric morphisms rather than functors — after all, these are equivalences.

The 2-functor Sh from locales to toposes embeds Locales as a reflective sub-2-category of Toposes. (The reflector is: take subobjects of the terminal object.) In particular, it’s a full embedding. So for locales $X$ and $Y$ , there’s an equivalence of categories $(locale maps X \to Y) \simeq (geometric morphisms Sh(X) \to Sh(Y)).$ So I reckon $AUT(Sh(X)) \simeq AUT(X)$ .

Posted by: Tom Leinster on March 6, 2008 12:01 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

Just to add a bit to Tom’s “and so on”: Tom showed that any self-equivalence on $Set$ is isomorphic to the identity functor $1_{Set}$ . But then we can just use

$1_{Set} \cong hom_{Set}(1, -)$

plus the Yoneda lemma to deduce very quickly that there’s exactly one transformation from the identity functor to itself.

Posted by: Todd Trimble on March 6, 2008 1:48 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

Thanks to both of you. I guess that’s reassuring that $Sh(X)$ and $Sh(pt.)$ , i.e., Set, behave as though though they were just the space itself.

Posted by: David Corfield on March 7, 2008 3:15 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

Ten years later, led to this post by a link of David Corfield’s at the nForum, I just wanted to remark that the analogous question for the homotopy category is Grothendieck’s “hypothèse inspiratrice”, and is unknown per se. It is quite easy to prove if one lifts the question to derivators or $(\infty, 1)$ -categories. My personal conjecture is that the question for the actual homotopy category is indepedent of ZFC. I made a few remarks about this a couple of years ago on the HoTT mailing list, here.

One can dream of proving the independence in one direction by somehow making use of the fact that one can prove it if one lifts. I have no idea, though, how to prove the other direction, i.e. find some kind of model where it does not hold.

Posted by: Richard Williamson on April 25, 2018 1:33 PM | Permalink | Reply to this

Re: Worrying about 2-logic

Can I add a more trivial class of examples that I played with not too long ago? The logic S5_n is used to model multiagent systems in artificial intelligence. (There are quite nice books about this stuff as some may know.) The basic models are sets of `possible worlds’ with $n$ equivalence relations on them. The result is therefore an n-fold groupoid. If you use S4_n, well, S4 is modelled by posets, if I remember correctly, so the corresponding models are $n$-fold posets. Does that suggest anything?

As I said these are just the basic examples but are perhaps easier to think of than the general case, and possibly suggest new directions.

Posted by: Tim Porter on March 7, 2008 8:12 AM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

Do you require that each of the $n$ equivalence relations covers the same total set of possible worlds, or can it be that they jointly cover it?

I know you were interested in groupoid atlases, which now I see from a page of yours are such that

Single domain groupoid atlases = multiple groupoids.

I’d better get studying Geometric Aspects of Multiagent Systems.

Thinking further about first order modal logic, things do tally with what John and I were trying to cook up in Minneapolis.

Take propositional logic first. Here we have one level of syntactic variable, a set of propositional variables: $P, Q, R,$ etc. In a model each is assigned a truth value.

Now (typed) first-order logic. Here we have two levels of syntax, a set of types, $A, B, C,$ etc., and a set of typed predicates, $P_A, Q_{B \times C},$ etc.

The types are interpreted as sets. The predicates are maps from the set corresponding to their type to truth values.

Often, people don’t bother with the types, and instead assign a domain of all individuals for a model. Then what was a type is seen as a predicate on this domain. E.g., rather than a type Dogs, we use a predicate $Dog(x)$ where $x$ ranges over the whole domain, and is true precisely when $x$ is a dog.

The typed version fits more satisfyingly, though, with the $n$ -category ladder story.

Third, we turn to modal logic. We have three levels of syntax. A collection of metatypes, $U, V, W$ ; a collection of types $A_U, B_{V \times W},$ ; a collection of predicates, $P_{A_U}, Q_{B_{V \times W}}$ .

[I seem to remember we had a question about whether to allow things like $R_{A_U \times B_{V \times W}}$ .]

Each metatype is assigned a groupoid (perhaps in a variant we could use categories, more generally). Each type is a map from the corresponding groupoid to Set, so a presheaf. Each predicate is a map from the corresponding presheaf to truth values.

It looks as though Awodey and Kishida have opted for an untyped single-agent first-order modal logic. So they avoid two levels of syntax by using a sheaf of all individuals over a single category of possible worlds. The $n$ of Tim’s $S5n$ corresponds to the number of metatypes. I guess one could play the same trick as described above when going from typed to untyped first-order logic, and form the universe of possible worlds as a single category.

So, I’m still unclear about what sort of thing one wants at the base of the model – groupoids, categories, sites, etc.

And I’d still like to see where the symmetry of the model comes in. Do we get a 2-group?

Posted by: David Corfield on March 7, 2008 9:39 AM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

I have not fully read David’s reply to my comment, but I think I can make one or two mini-replies.

Firstly that the better paper of the two that I wrote on this might be

Interpreted systems and Kripke models for multiagent systems from a categorical perspective, Theoretical Computer Science, 323 (2004) pp. 235-266.

As to whether the groupoid/equivalence relations cover all the set of possible worlds, that is not too much of a worry as I seem to remember checking that making all points outside the domain of the equivalence relation into singleton equivalence classes converted the general form to that much nicer form.

My definition and choices were led by the `applications’ and interpretations and I think that is a good place to start to look for the deeper structure. The multiagent context and various other similar ones from adjacent areas did make me ask certain questions about the models, e.g. communication between different systems perhaps with differing numbers of agents, could be perhaps modelled by a meta system involving the two sets of agents. This however raised the problem of building in some of the communication protocols into the basic models and that left me high and dry.

Another aspect was that of an evolving multiagent system. All these have more than a superficial link with sets of interacting particles and the physics side of this blog, so I turned to Sorkin and his causal set models and am still trying to work my way to linking across to the modal logic stuff in a richer mode.

Finally the algebraic side of $S5$ and its multimodal versions, $S5_n$ is Boolean algebras with operators and that again has strange reverberations across to the physics.

Posted by: Tim Porter on March 7, 2008 1:44 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

Alas, David, I’m too busy to carefully read this post! This is my weekend for finishing that darn Rosetta Stone paper. So, I just want to make some vatic, gnomic, cryptic, provocative pronouncements for the purposes of moral support.

2-logic won’t neatly match existing ideas on modal logic. It’ll be much better. So far, modal logic has had little impact on mathematics — basically because most approaches start by listing plausible-looking axioms and only later try to develop the semantics. In math, it’s better to start with a clear idea of what we’re talking about, and work out the formalism based on this.

The great thing about 2-logic is that it can be completely described in one sentence. A theory in 2-logic has a concrete 2-groupoid of models, and any concrete 2-groupoid is the 2-groupoid of models of an essentially unique theory in 2-logic.

This completely pins down what 2-logic is, modulo esthetic decisions about how to present it. And, it means that whenever we have a 2-groupoid, 2-logic applies. So, there’s no shortage of applications staring us in the face!

Even better, all this stuff is a straightforward generalization of ‘ordinary logic’. Ordinary logic can be summarized as follows: a theory in ordinary logic has a concrete groupoid of models…. and any concrete groupoid is the groupoid of models of an essentially unique theory in ordinary logic.

So, I wouldn’t worry too much if someone else’s models of someone else’s modal logic lack 2-groups of symmetries!

Posted by: John Baez on March 7, 2008 8:19 PM | Permalink | Reply to this

Re: Worrying about 2-logic

In essence I agree with John, BUT the mathematical world outside has a certain tendency to want a beautiful theory to interact with other areas of mathematics. The instances of modal logics that I have played with convinced me that there were several layers of extra structure lying around and that they needed examining. When in that situation it pays to be Janus-like, to look out to the abstraction but to keep an eye on the new look of the other peoples models that the extra distance gives.

I do not think that John’s one line summary of ordinary logic is fair (not that I think, it was really intended to be ). My point earlier was that I believe that the very simplest modal logics that I know of as a mathematician have models that ARE groupoids because they are equivalence relations!!!!! Thus they DO have 2-groupoids as their automorphism gadgets. This even suggests very simple examples of n+1 logics namely my friendly little $S5_n$. The motivation from applications suggests new problems that are related to the 2-logical structure of the beasties. Some of the modal logic texts do seem not to know about categories, and have the feeling of the universal algebra texts written before Lawvere’s algebraic theories, so general modal logic need not concern us that much except where it seems to fit the bill.

Grothendieck in 1975 basically suggested that the Galois-Poincaré correspondence between covering spaces and subgroups of the fundamental group extended to higher dimensions. He seems to have thought that this would have a higher dimensional Galois theory as a consequence. I suspect all of us who look at this blog regularly agree, more or less, with his view, but I do not believe there is any really striking example from algebra / number theory that shows how such a Galois theory would look. The recent discussion on another thread of this blog I think bears me out. What I mean is that the Galois 2-group of something should be definable so that the Galois group was extractable from it. What the `something’ would be is another matter. I do not really count algebraic geometric objects, as they were not evident in Galois’ original theory. I digress.

Knowing how to define something and how to construct abstract examples is good, and one hopes that it has the right `feel’ to it, but if it impacts outside the narrow circle of initiates that is even better. The stacks/ gerbes story has done that in differential geometry and mathematical physics, if not so far really in number theory. Let us hope that its logical cousin, so well described by John, will be found to do the same within some area of logic.

Posted by: Tim Porter on March 7, 2008 9:16 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

any concrete 2-groupoid is the 2-groupoid of models of an essentially unique theory in 2-logic.

I think I’m beginning to see how to fit sheaves into that slogan. But first I’d better have straight in my mind what concreteness is.

So a concrete category is a category equipped with a structure, a faithful functor to Set. Presumably a concrete groupoid is a concrete category which is a groupoid.

Am I right in thinking a concrete 2-groupoid is a 2-groupoid equipped with a faithful 2-functor to the 2-groupoid of 1-groupoids? Or do I need to worry about injectivity at different morphism levels? No doubt it’s all in here.

Which goes to prompt us to ask what a concrete 0-groupoid might be. A 0-groupoid, or set, equipped with a ??? function to the 0-groupoid of $(-1)$ -groupoids, or set of truth values?

If the ??? is no condition, then a concrete set would be a set equipped with a predicate. That seems odd.

If ??? is ‘injective’, then it would be a set with at most 2 elements. Also odd.

Posted by: David Corfield on March 8, 2008 12:26 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

David wrote:

Am I right in thinking a concrete 2-groupoid is a 2-groupoid equipped with a faithful 2-functor to the 2-groupoid of 1-groupoids?

I’m not sure this term has has a standard meaning — and indeed, my comment was more meant as an nudge in the ribs than a carefully reasoned statement. I was just trying to get you to aim higher than existing modal logic, since if ever there were a potentially interesting branch of logic that failed to develop significant ties to mainstream math, modal logic must be it!

But okay — let me try to say something clearer.

In its usual sense, a ‘concrete groupoid’ is a groupoid of sets equipped with extra structure: that is, a groupoid equipped with a functor down to $Set$ that forgets at most structure. An ‘untyped’ — or really ‘ $1$ -typed’! — theory phrased in classical logic will have a concrete groupoid of models. A simple example would be ‘the theory of monoids’, whose groupoid of models consists of:

monoids
monoid isomorphisms

More generally, an ‘ $n$ -typed’ theory phrased in classical logic will have a groupoid of models equipped with a faithful functor to $Set^n$ . A simple example with $n = 2$ would be theory of ‘ring-module pairs’.

Now we want to categorify all this! So, we turn the categorification crank…

A 1-metatyped theory in 2-logic should have a ‘concrete 2-groupoid’ of models. What’s that? It’s a 2-groupoid of categories equipped with extra stuff: that is, a 2-groupoid equipped with a 2-functor to the 2-groupoid of categories which forgets at most stuff. A simple example would be the ‘theory of monoidal categories’, whose 2-groupoid of models consists of:

monoidal categories
monoidal equivalences
monoidal natural isomorphisms

Or do I need to worry about injectivity at different morphism levels? No doubt it’s all in here.

The natural categorification of ‘forgetting at most structure’ is ‘forgetting at most stuff’ — and this is explained in the body of that paper. But, for 2-logic per se, I strongly urge that you read the appendix by Mike Shulman. He explains how the propositional calculus is 0-logic, and predicate logic is 1-logic, and he points at what should be 2-logic. But, he does this all in the intuitionistic framework, where $n$ -logic is about $n$ -topoi! In the above comments, I’m not getting into intuitionistic aspects of logic. I’m being very ‘classical’, because that’s what I understand better.

Posted by: John Baez on March 9, 2008 6:45 AM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

The thing that tends to confuse is that unless 0-logic is ‘ $n$ -typed’ (or $n$ -whatevered) for $n$ at least 2, it’s a tad boring.

So an ‘ $n$ -typed’ theory in 0-logic will have a set of models equipped with a function to $(Truth values)^n$ .

I’d guess that function had better be injective. Maps between $n$ -groupoids factorise into $(n + 2)$ layers, and for concreteness we want the top layer to be trivial. So maps between sets (0-groupoids) factorise as surjections followed by injections, and we want the surjection to be trivial.

Then we have a propositional theory with $n$ propositional variables, the models being the lines of the truth table where the axioms hold. The concreteness map forgets the property that the truth valuations satisfy the theory.

Back with 2-logic, I imagine it’s as well to keep in mind less august theories than ones like monoidal categories, just as we look at simple first order theories.

Posted by: David Corfield on March 9, 2008 12:34 PM | Permalink | Reply to this

Re: Worrying about 2-logic

Following up on that last thought, an example which might prove good to keep in mind is the 2-theory which has as a model a groupoid equipped with a presheaf. Then we could chuck in a predicate by carving out a subset from the presheaf.

Posted by: David Corfield on March 9, 2008 6:13 PM | Permalink | Reply to this

2-Undecidability; Re: Worrying about 2-logic

What do we know about Undecidability in 2-logic? My hunch is that 2-Undecidability IS equivalent to 1-Undecidability.

Posted by: Jonathan Vos Post on March 9, 2008 8:48 PM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

So is concreteness just a relative notion? A category $C$ is concrete relative to another category $D$ if it is equipped with a faithful functor to $D$ .

Posted by: David Corfield on March 10, 2008 10:43 AM | Permalink | Reply to this

Re: Worrying about 2-logic

$MathML-enabled post (click for more details).$

David wrote:

So is concreteness just a relative notion? A category $C$ is concrete relative to another category $D$ if it is equipped with a faithful functor to $D$ .

Exactly! The default $D$ is the category $Set$ , but there’s nothing sacred about that choice, except insofar as the homsets of our category are sets, which makes certain things work better with sets. (We can even get around this using enriched categories, which have more general hom-objects.)

So: one man’s ‘abstract’ is another man’s ‘concrete’…

… which reminds me of the joke that I might have seen in Concrete Mathematics: “To help the reader drowning in a sea of abstraction, the following example may serve as a concrete life preserver.”

Blub blub blub…

Posted by: John Baez on March 11, 2008 7:25 AM | Permalink | Reply to this

Re: Worrying About 2-Logic

$MathML-enabled post (click for more details).$

David wrote:

So an ‘ $n$ -typed’ theory in 0-logic will have a set of models equipped with a function to $(Truthvalues)^n$ .

That sounds right.

Back with 2-logic, I imagine it’s as well to keep in mind less august theories than ones like monoidal categories, just as we look at simple first order theories.

By “ones like monoidal categories” do you mean “ones like the 2-theory of monoidal categories”?

Unless I’m mixed up, which is quite possible, the 2-theory of monoidal categories should be about as simple and primordial as the theory of monoids. That’s why I mentioned it — I wasn’t trying to be fancy.

For the theory of monoids we need one type $M$ , one binary operation $\times$ , one constant $1$ , and axioms for the left and right unit laws and associativity.

For the theory of monoidal categories we need one metatype $M$ … what happens after that? Maybe I am mixed up. Maybe it’s easier to discuss monoidal categories with a specified set of objects? Where these objects are all the types of metatype $M$ ?

Hmm, I think I am confused.

Posted by: John Baez on March 10, 2008 4:34 AM | Permalink | Reply to this

Re: Worrying About 2-Logic

$MathML-enabled post (click for more details).$

Yes, I did mean the 2-theory of monoidal categories.

I was trying to suggest that, just as when introducing first-order logic to philosophy students you don’t instantly pull out a nice mathemathical theory like that for monoids, similarly with 2-logic.

Philosophy students get to work with things like

Anyone who is loved by someone who is tall loves everyone who is short.

Tall people love themself.

Peter is short and is not loved by Anna.

Therefore, Anna is not tall.

Typically, you see less functions (other than names).

What now about the 2-theory of monoidal categories? So the single metatype $M$ gets given a category. As there’s only one, we don’t need to metatype our types. One type $O$ is assigned the set of objects, and a predicate $I$ carves out those which act as the identity. There’s a function (or relation depending on whether you want the product) from $O \times O$ to $O$ . And so on, with axioms involving another type $A$ of arrows.

Are we encountering the issue that category theory itself doesn’t look especially natural viewed from ordinary logic, being just a complicated 2-typed theory?

Is it a little odd to have the 2-groupoid of categories and equivalences providing the concreteness of the models of a 2-theory, as that already endows them with considerable structure?

Posted by: David Corfield on March 10, 2008 10:07 AM | Permalink | Reply to this

Re: Worrying About 2-Logic

$MathML-enabled post (click for more details).$

David wrote:

Are we encountering the issue that category theory itself doesn’t look especially natural viewed from ordinary logic, being just a complicated 2-typed theory?

Right. At least, something like that is the reason I’m so confused right now.

It involves the concept of ‘model’. When we talk about a model of a theory in ordinary logic, we typically mean (by default) a model in the category of sets. So, when we talk about a model of a theory in 2-logic, I’d expect us to mean a model in the 2-category of categories (or groupoids, if we feel that way). We shouldn’t have to strain to make it work. But right now I feel we need to strain, for precisely the reason you mention.

I must be doing something dumb. I suspect if I take the time to sit down and think about it, everything will work out.

Posted by: John Baez on March 11, 2008 7:37 AM | Permalink | Reply to this

Re: Worrying About 2-Logic

$MathML-enabled post (click for more details).$

I think what I said above was abject nonsense. Let’s try again to grasp monoidal categories as a 2-theory:

The single metatype gets assigned a category $C$ .

Then we want $M$ a presheaf on $C^2$ which maps $(c, d)$ to the set of products of $c$ and $d$ .

We also want $O$ a presheaf on $C$ which maps $c$ to $\{c\}$ , and a unary predicate, $I_{O}$ , the subset consisting just of the object(s) with the property of being an identity.

Hmm, maybe we can start to see where 2-logic goes beyond modal logic. Leaving aside that we can have different metatypes of worlds, if the worlds are the objects of the category of the model, then presheaves over powers of the category give us a way to talk about how worlds are related.

In normal modal logic you might have a ‘necessarily it is possible that…’ meaning that for every world something holds in a world related to it. But now we can give conditions on sets assigned to tuples of worlds.

Posted by: David Corfield on March 11, 2008 10:02 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

March 6, 2008