First-Order Logical Duality

March 27, 2009

Posted by David Corfield

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

This is the title of the PhD thesis in which Henrik Forssell presents

…an extension of Stone Duality for Boolean Algebras from classical propositional logic to classical first-order logic. The leading idea is, in broad strokes, to take the traditional logical distinction between syntax and semantics and analyze it in terms of the classical mathematical distinction between algebra and geometry, with syntax corresponding to algebra and semantics to geometry.

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

Extending the duality between Boolean algebras and Stone spaces, Forssell derives a duality between Boolean coherent categories and topological groupoids. A Boolean coherent category corresponding to a first-order theory has as dual the topological groupoid of its models and isomorphisms.

So,

Analogously with the Makkai duality, we consider the groupoid of models and isomorphisms of a theory. Analogously with Stone duality, we use topological structure to equip the models and model isomorphisms of a theory with sufficient structure to recover the theory from them. The result is a first order logical duality which, in comparison to Makkai’s, is more geometrical, in that it uses topology and sheaves on spaces and topological groupoids rather than ultraproducts, and that moreover specializes to the traditional Stone duality. (p. 17)

The dualizing object (did we give up on ambimorphic?) has shifted from $2$ to $Sets$ . Next stop $Groupoids$ .

Posted at March 27, 2009 10:15 AM UTC

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

8 Comments & 2 Trackbacks

Re: First-Order Logical Duality

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

So, Jim Dolan has spent many years telling us about the duality between first-order logic and groupoids: a theory in first order logic has a groupoid of models, and any groupoid arises as the models of an essentially unique theory. Todd Trimble made this very precise and wrote up a portion here:

Most of this concerns the special case of groups, but his last sentence gives the generalization:

For more general (let us say finite) polyadic Boolean algebras $T$ , the category $T−Mod$ is a groupoid. This is in part due to the classical (Boolean) nature of these hyperdoctrines. To be related to the fact that a topos Set $C$ is a Boolean topos iff $C$ is a groupoid.

From your quote above, it sounds that Makkai has done related work.

So, it would be very nice to 1) let Henrik Forssell know about Todd’s guest posts, 2) understand what Forssell has done.

As for 1): do you know Forssell? Maybe you can send him an email about this blog entry.

As for 2):

I’m really curious what’s the intuitive meaning of a topological groupoid of models. First, a point of terminology: is this being used to mean a groupoid internal to $Top$ (where we have a topology on the space of objects and on the space of morphisms) or a groupoid enriched in $Top$ (where we only have a topology on each hom-set)? For no particular reason I bet he means the first. In the first case: what does it mean, intuitively, for two models to be close to each other? In either case: what does it mean for two maps between models to be close to each other?

Also:

How, if at all, is this stuff related to the Joyal–Tierney theorem showing that Grothendieck topoi are all categories of sheaves on localic groupoids?

A. Joyal and M. Tierney, An extension of the Galois theory of Grothendieck, Memoirs of the A.M.S. 309 (1984).

‘Localic groupoids’ are a lot like topological groupoids, since the concept of locale is just an improved version of the concept of topological space, with better properties.

A localic groupoid is a groupoid internal to the category of locales.

It’s a bit hard for me to imagine a result in heavy-duty categorical logic that would work better for topological groupoids than localic groupoids!

Posted by: John Baez on March 27, 2009 5:27 PM | Permalink | Reply to this

Re: First-Order Logical Duality

I guess we shouldn’t be too surprised at the topological part of ‘topological groupoids appearing here in view of the syntax-semantics duality in the propositional case being captured by Stone duality.

Topological groupoids as groupoids in Top are defined on p. 19.

The ‘logical’ topology on a space of models of a first-order theory is defined on p. 42.

A topology is also defined on the groupoid of sets and functions, allowing it to play the role of dualizing object.

Posted by: David Corfield on March 30, 2009 9:05 AM | Permalink | Reply to this

Re: First-Order Logical Duality

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

John asks

How, if at all, is this stuff related to the Joyal-Tierney theorem showing that Grothendieck topoi are all categories of sheaves on localic groupoids?

Forssell writes on p. 23

The idea of the current approach is thus that in the first-order logical case, topoi of sheaves can play the role that is played by frames of open sets in the propositional case. This idea springs from the view of topoi as generalized spaces and the representation theorem of Joyal and Tierney ([11]) to the effect that any topos can be represented as equivariant sheaves on a localic groupoid.

Further,

Butz and Moerdijk show that if the topos $\mathcal{E}$ has enough points, in the sense that the collection of inverse image functors for geometric morphisms $Sets \to \mathcal{E}$ are jointly faithful, then $\mathcal{E}$ has a representation in terms of a topological groupoid, i.e. there is a topological groupoid $\mathbb{G}$ such that $\mathcal{E} \simeq Sh (\mathbb{G})$ .

Posted by: David Corfield on March 30, 2009 10:57 AM | Permalink | Reply to this

Re: First-Order Logical Duality

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

Thanks! Okay, so maybe ‘topological groupoid’ is serving as a stand-in for ‘localic groupoid with enough points’.

So, do you think this is roughly correct: he’s studying a class of topoi that are equivalent to topoi of sheaves on topological groupoids?

Posted by: John Baez on March 30, 2009 8:39 PM | Permalink | Reply to this

Re: First-Order Logical Duality

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

Here’s a handy description from pp. 38-39:

Recall that we call a coherent theory decidable if for each sort there is a predicate $\neq$ satisfying axioms of inequality (see p. 28). The goal of the current section is the representation of such a theory $\mathbb{T}$ in terms of its semantical groupoid $G_{\mathbb{T}} \rightrightarrows X_{\mathbb{T}}$ of models and isomorphisms in Theorem 2.3.4.14, stating that the topos of sheaves for the coherent coverage on $\mathcal{C}_{\mathbb{T}}$ [the syntactic category associated with $\mathbb{T}$ ] is equivalent to the topos of equivariant sheaves on $G_{\mathbb{T}} \rightrightarrows X_{\mathbb{T}}$ ,

$Sh (\mathcal{C}_{\mathbb{T}}) \simeq Sh_{G_{\mathbb{T}}}(X_{\mathbb{T}})$

The overall form of the argument resembles that sketched in Section 1.2.1 for the representation of a Boolean algebra in terms of its space of models: Generalizing the Stone Representation Theorem, we embed $\mathcal{C}_{\mathbb{T}}$ in the topos of sets over the set of models, $Sets/X_{\mathbb{T}}$ , in Lemma 2.3.2.1. Proceeding to introduce a logical topology on the set $X_{\mathbb{T}}$ of models and then to introduce $\mathbb{T}$ -model isomorphisms for additional structure, we show how the embedding of $\mathcal{C}_{\mathbb{T}}$ into $Sets/X_{\mathbb{T}}$ factors through, first, the topos $Sh(X_{\mathbb{T}})$ of sheaves on the space $X_{\mathbb{T}}$ (Proposition 2.3.2.7) and, finally, the topos $Sh_{G_{\mathbb{T}}}(X_{\mathbb{T}})$ of equivariant sheaves on the topological groupoid $G_{\mathbb{T}} \rightrightarrows X_{\mathbb{T}}$ (Lemma 2.3.4.7). Showing that the image of the embedding generates $Sh_{G_{\mathbb{T}}}(X_{\mathbb{T}})$ in Lemma 2.3.4.13, we are then in a position to conclude that the embedding lifts to an equivalence $Sh (\mathcal{C}_{\mathbb{T}}) \simeq Sh_{G_{\mathbb{T}}}(X_{\mathbb{T}})$ in Theorem 2.3.4.14.

Posted by: David Corfield on March 31, 2009 10:04 AM | Permalink | Reply to this

Re: First-Order Logical Duality

This is neat. So a Boolean coherent category (associated with a first order logic) is dual to a topological groupoid of its models and isomorphisms. There is also a deep duality result for first order logic involving profinite mathematics [1].

In terms of category theory or the theory of pretopoi or topoi, how would one best describe this first order logic:

With linear order, a first order logic with a least fixed point operator?

The reason I am asking this question is because such a logic gives the complexity class P. This is an example of descriptive complexity theory which is a branch of finite model theory. Then, the famous P/NP problem becomes:

Can second order logic describe languages (of finite linearly ordered structures with nontrivial signature) that first order logic with least fixed point cannot?

Please note that there is also infinite model theory and model theory of metafinite structures [2], and so could there also be profinite model theory? In terms of category theory, a profinite or inverse limit is an example of a (co)filtered limit [3].

[1] http://www.liafa.jussieu.fr/~jep/PDF/DualityWeb.pdf

[2] http://www-mgi.informatik.rwth-aachen.de/FMT/

[3] http://en.wikipedia.org/wiki/Filtered_category

Posted by: Charlie Stromeyer on July 14, 2009 6:59 AM | Permalink | Reply to this

Re: First-Order Logical Duality

There is also a related new paper about profinite methods in automata theory [1]. Here is perhaps another way to think about this problem:

Would it be possible to construct increasingly large finite instances X of a polynomial time problem such that an infinite instance of X is solvable? The hope is then that for a similar construction of an NP-complete problem the infinite instance of the NP-complete problem would not be solvable.

I have read various papers on infinite constraint satisfaction problems (CSPs) such as [2] and [3]. Would it make sense to use profinite categories such as in [4] or even profinite domains such as in [5] to construct an infinite CSP as the limit of increasingly large finite instances of the same underlying CSP?

[1] http://drops.dagstuhl.de/opus/volltexte/2009/1856/pdf/09001.PinJean_Eric.1856.pdf

[2] http://www.lix.polytechnique.fr/~bodirsky/publications.html

[3] http://www.brics.dk/~fvalenci/papers/icsp_sac05.pdf

[4]

http://citeseer.ist.psu.edu/61318.html

http://citeseer.ist.psu.edu/258571.html

[5] http://citeseer.ist.psu.edu/59953.html

Posted by: Charlie Stromeyer on July 15, 2009 4:33 PM | Permalink | Reply to this

Read the post Coalgebraic Modal Logic
Weblog: The n-Category Café
Excerpt: Putting together ideas of modal logic and coalgebra with ways of modelling first-order theories.
Tracked: September 7, 2009 12:51 PM

Re: First-Order Logical Duality

Forssell and Awodey now have a preprint available – First-Order Logical Duality.

Posted by: David Corfield on August 20, 2010 10:38 AM | Permalink | Reply to this

Read the post Category Theoretic Modal Logic
Weblog: The n-Category Café
Excerpt: Category theoretic ideas on modal logic
Tracked: April 4, 2011 5:11 PM

The n-Category Café

Skip to the Main Content

March 27, 2009