### Logic as Invariant Theory Revisited

#### Posted by David Corfield

Some years ago I wrote a brief post on Friederich Mautner’s ‘An Extension of Klein’s Erlanger Program: Logic as Invariant-Theory’. Inspired by Weyl’s linkage of the representation theory of classical groups to invariant theory, this 1946 paper marked the first appearance of an idea, later taken up by Tarski and developed by many (nLab), that logic concerns what is invariant under the most general transformations, permutations of the universe of discourse.

With the coming of HoTT/Univalent Foundations, I think it’s worth revisiting this question. In my recent book I claimed, rather vaguely, that we find that “the boundary between logic and mathematics blurs” (MHTT, p. 89). This was inspired by the sight of people working out things like the 4th homotopy group of the 3-sphere in pure HoTT:

Guillaume Brunerie, *The James construction and $\pi_4(S^3)$ in homotopy type theory*, (arXiv:1710.10307).

But what if we could be more precise about the new boundary of the logical?

Steve Awodey is a proponent of the thesis that HoTT marks a great extension of the Mautner-Tarski idea. In his Univalence as a Principle of Logic he advocates what he calls the Tarski-Grothendieck Thesis:

If a statement, concept, or construction is purely logical, then it should be invariant under all equivalences of the structures involved. A statement that is not invariant must involve some non-logical specifics, pertaining not to general logical form but to some particular aspects of the objects bearing the structure. If it is the hallmark of a logical concept that it should pertain only to general, formal structure and not to any specific features of the objects bearing that structure, then this formal character may be witnessed by the fact that the concept is invariant under all equivalence transformations. (p. 10)

(I hope Mautner might be included in the name of this thesis.)

Something that’s attempted in the world of first-order logic is the classification of *all* constructions that may be counted as logical. Closer to HoTT, in Logical Constants across Varying Types Johan van Benthem has done some useful work along these lines for a simple type theory, generated by a type, $e$, of individuals and a type, $t$, of truth values, and closed under function types, $(\alpha, \beta)$. For instance, properties are elements of $(e, t)$, and quantifiers of $((e, t), t)$. Van Benthem gives us a way of saying of a type whether or not it has an invariant element under permutations of the set $e$.

What corresponds to this work for HoTT? Well, buying into the Freedom from Logic idea that propositions aren’t special, you might think to consider permutations of all types, perhaps via automorphisms of the universe type, $\mathcal{U}$. However, constructively we can’t even say that there are any such automorphisms. (There’s a blog post and linked article, for those wishing to follow this up.) In any case, $\mathcal{U}$ is playing the role of van Benthem’s $t$. (But note that Mautner mentions the possibility of allowing transformations swapping truth values $0$ and $1$ in footnote 6.)

Ulrik Buchholtz has been helping me on this question, and I learn from him that given a type $A$, we may proceed by considering constructions invariant under $Aut(A)$. This is proposed by him in his article

*Higher Structures in Homotopy Type Theory*, (arXiv:1807.02177)

Homotopy type theories are synthetic theories of $\infty$-groupoids. The approach is deeply

logical, where we think of logic asinvariant theoryas pioneered by Mautner [37] and later developed by Tarski in a 1966 lecture [50]. Both Mautner and Tarski were inspired by the approach to geometry given in Klein’sErlangen Program[30]. The idea is that the logical notions are those that are invariant under that maximal notion of symmetries of the universes of discourse. If the universe of discourse is a set, then the corresponding symmetry group is the symmetric group consisting of bijections of the set with itself, but if it is a higher homotopy type, then it is the (higher) automorphism group consisting of all self-homotopy equivalences.

The clever way to encode such invariance for a type $A$ in HoTT is via dependence on the type $BAut(A)$. This has as elements all types which are merely equivalent to $A$ (so no specific equivalence is designated). Then we might consider fixed points in, say,

$(X : BAut(A)) \to (X \to \mathcal{U}) \to \mathcal{U}.$

Similarly to van Benthem finding the quantifiers as invariants of $((e,t),t)$, here we find the constructions sending a type depending on $A$ to dependent sum and dependent product (dependent pair and function, if you prefer).

In $(X : BAut(A)) \to X \to \X \to \mathcal{U},$ we find the identity type.

In $(X : BAut(A)) \to \mathcal{U},$ we find the truncations of $A$, $List(A)$, $A^2$, and so on.

In $(X : BAut(A)) \to \mathcal{U} \to (X \to \mathcal{U})$ there is the pullback of types to constant types depending on $A$. Composing this with dependent sum/product gives the modal operators in $(X : BAut(A)) \to (X \to \mathcal{U}) \to (X \to \mathcal{U})$ corresponding to possibility and necessity. (Modal constructions are studied in the non-type theoretic world, see, e.g., here.)

How to treat multi-variable constructions? Mautner considers (p. 354) the case of several domains of individual variables, in particular the two cases where the domains are completely independent, and where there is one domain upon which all others are completely dependent. In the former case, we just consider permutations on each domain together.

So here, we might consider invariants in $(X: BAut(A)) \to (Y: BAut(B)) \to \mathcal{U}.$

Of those properly depending on both $X$ and $Y$, we would find sum, product and function types.

Ulrik then asks what of constructions that don’t depend on another type, constructions such as $\mathbf{1}$, the natural numbers, the Cauchy reals? And what of constructions in HoTT compatible with Univalence, but non-constructive?

I’m left wondering whether there’s something here worth pursuing. Could one achieve an exhaustive list of ‘logical’ constructions. Presumably at some stage contact should be made with these type constructions as adjoints, as universal.

## Re: Logic as Invariant Theory Revisited

James Dolan always used to emphasize to me that Galois theory was ultimately about the duality between logic and groupoid theory. In simple terms: you can’t define a function that picks out one of several elements with some property in a theory that has a symmetry nontrivially permuting these elements. He repeatedly urged me to look into Beth’s definability theorem as a way to make this precise in classical first-order logic.

Interestingly, the first example in the link I just gave has a strong flavor of Galois theory, since it concerns polynomials. But it doesn’t mention groups or groupoids, so one would have to tease that out.

I could be completely confused about what you’re getting at, but here’s my intuition:

If you don’t add any axioms to your theory besides ‘pure logic’ (whatever you choose to mean by that), a model of this theory may not have any nontrivial automorphisms. But in general models will have interesting automorphisms. For example, if you take the theory of an algebraically complete field of characteristic zero, any model of cardinality $2^{\aleph_0}$ should have an enormous symmetry group, namely $Gal(\mathbb{C}/\mathbb{Q})$.

In this example I’m using classical first-order logic, since that’s what I understand best. I’m also using the fact that theory of an algebraically complete field of characteristic zero is uncountably categorical, so all models of a given uncountable cardinality are isomorphic. This lets me talk about a group instead of a groupoid.

But extrapolating, I’d guess that if you can set up ‘the theory of an $n$-sphere’ in homotopy type theory, it should have a $\infty$-groupoid of models where the symmetries of any model — or at least any ‘standard’ model — are the homotopy autoequivalences of the $n$-sphere.

There’s a lot I don’t understand about this, but maybe someone can figure it out!