Logic as Invariant Theory Revisited

August 11, 2021

Logic as Invariant Theory Revisited

Posted by David Corfield

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

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?

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

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 as invariant theory as 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’s Erlangen 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.

Posted at August 11, 2021 12:07 PM UTC

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

Some Related Entries

25 Comments & 0 Trackbacks

Re: Logic as Invariant Theory Revisited

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

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.

However, constructively we can’t even say that there are any such automorphisms.

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!

Posted by: John Baez on August 11, 2021 4:51 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

As regards the first point, we do still have a report on James’s ideas on a Galois correspondence between complete theories of structures on a set $X$ and concrete groups of transformations on $X$ from Todd Trimble’s posts I and II. This is very much Mautner territory.

No doubt there was much more we never heard about. Last time I noted that this included, as described by Todd:

a whole slew of interesting developments, in which we view Jim’s orbi-simplex idea as a geometric description of a general axiomatic theory, which in turn is related to the idea of viewing Tits buildings as “quantized” axiomatic theories, and also perhaps to the theory of classifying toposes and their “Galois theory”.

Posted by: David Corfield on August 11, 2021 6:49 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

As for the second part, so we’re in the game of finding constructions that treat equivalent types equivalently. Since another thread led me there, I was very much reminded of your description of James’s ideas on Holodeck games. Here’s an extract

Let’s play a game. I have a set $X$ in my pocket, and I’m not telling you what it is. Can you pick an element of $X$ in a systematic way? No, of course not: you don’t have enough information. $X$ could even be empty, in which case you’re clearly doomed! But even if it’s nonempty, if you don’t know anything about it, you can’t pick an element in a systematic way.

So, you lose.

Okay, let’s play another game. Can you pick an element of

$X^X$

in a systematic way? Here $A^B$ means the set of functions from $B$ to $A$ . So, I’m asking if you can pick a function from $X$ to itself in a systematic way.

Yes! You can pick the identity function! This sends each element of $X$ to itself:

$x \mapsto x$

Taking this up to a simple type theory with individuals $e$ and truth values $t$ , can you systematically give me an element of $e$ , of $(e, e)$ , of $(e, t)$ , of $((e, t), t)$ , $((e, t), e)$ and so on?

Again: No special individual; Yes, the identity; Yes, e.g., always true; Yes, several including the quantifiers; No special way to go from properties to elements.

By “systematic” we mean invariant under symmetries of $e$ .

I was looking to take this approach further to a more sophisticated type theory.

Posted by: David Corfield on August 11, 2021 7:11 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

So perhaps we could adapt the holodeck theory where setting $X=0$ in an expression such as

$((X^X)^{(X^X)})^{((X^X)^{(X^X)})}$

tells you if there’s a way to win (a systematic element) to van Benthem’s simple type theory, by setting $e=0$ and $t=1$ in his expressions.

Can their technique to find all the ways to win a game be adapted?

Posted by: David Corfield on August 11, 2021 7:55 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Van Benthem’s result about compound types being inhabited by invariant terms (pp. 5-6 of Logical Constants across Varying Types) then corresponds to showing that an iterated exponential of $0$ s and $1$ s will only be $0$ if the final term is $0$ and the others $1$ .

Has anyone made a connection between logic as invariant theory and logic as game?

Posted by: David Corfield on August 13, 2021 10:35 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

I’m interested in the comment “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” in the context of Galois theory, which I persist in thinking has something to do with roots of polynomials. It seems to me that one can indeed talk about “the positive square root of 2”, or “the real cube root of 2”, although somehow not about “the square root of -1 with positive imaginary part”. And yet each of those things is a root of a polynomial in which there are symmetries non-trivially, indeed transitively, permuting those roots.

Posted by: Richard Pinch on August 14, 2021 10:55 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Well there you’re not handing me just any set. There aren’t any non-trivial field automorphisms of the reals. On the other hand, there are very many field automorphisms of $\mathbb{C}$ .

Posted by: David Corfield on August 14, 2021 2:00 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Quite so. So although the two fields of degree two over the rationals generated by the roots of the polynomials $X^2+1$ and $X^2-2$ respectively both have automorphisms that transitively permute the respective sets of roots, one can be embedded in the complex numbers in such a way that the images of the two roots are distinguishable: there is no automorphism of $\mathbf C$ taking the positive real root to the negative real; whereas the other cannot: there is an automorphism of $\mathbf C$ taking the image of one root to the other. How do we reconcile this with the general proposition that “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”? What is the logical difference between the two theories?

Posted by: Richard Pinch on August 14, 2021 8:34 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

there is no automorphism of $\mathbf{C}$ taking the positive real root to the negative real

There are such automorphisms. Of course, they won’t be continuous, but “wild” (e.g., here). Such wild automorphisms fix the rationals but map the reals to a dense subset of the plane.

That real roots seem more specifiable is surely down to the order structure on the rationals and its completion to the reals.

Posted by: David Corfield on August 15, 2021 8:44 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

But you must know all this of course, now I see your background.

Perhaps Joel Hamkins’ MO answer helps

the real number field is not definable in the complex field by any assertion in the language of fields…

except for the rational numbers, every single complex number is part of a nontrivial orbit of automorphic copies, from which it cannot be distinguished in the field structure.

Posted by: David Corfield on August 15, 2021 9:00 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

You’re quite right that I was thinking of those automorphisms which preserve the real numbers, and that’s a very special case. You’re helping me to clarify my point, which by now might be better expressed as: there are two quadratic extensions of the rationals, one of which can be ordered/embedded in an ordered field/embedded in the reals and having done so it is possible to distinguish the two roots; the other one cannot. Yet in each case there is a symmetry non-trivially interchanging those two roots. So it seems to me there’s more to be said about the existence or non-existence of functions which pick out one of the two roots beyond the existence of that symmetry.

Posted by: Richard Pinch on August 15, 2021 9:39 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Incidentally, while I did initially focus on order properties of the roots of a polynomial, it’s not just about real and complex: let me give a p-adic instance of the same question. The equation $X^2 - 4X + 5$ has two roots with a symmetry permuting them in a quadratic extension of $\mathbf Q$ . If we look at them 5-adically, one of them is congruent to $0 \pmod 5$ and the other one isn’t.

Posted by: Richard Pinch on August 15, 2021 10:52 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

There are people far better qualified to talk about this, but with these shifting fields, perhaps you might consider these polynomials in terms of schemes. There’s no reason for the $S$ -points of a given $R$ -scheme to retain the symmetries of its $S'$ -points.

Posted by: David Corfield on August 15, 2021 6:35 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

… and than me, hence my raising the point! Of course I see that there’s a difference between the “internal” symmetries of the quadratic field $\mathbf{Q}(\sqrt{2})$ and those of the “external” field $\mathbf R$ or $\mathbf{Q}_5$ into which I choose to embed it. On the other hand, Class Field Theory tells me that the way a number field embeds into larger fields (abelian extensions to be precise) is reflected in its internal structure (ray classes of ideals).

Posted by: Richard Pinch on August 16, 2021 7:19 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

You said: “you might think to consider permutations of all types, perhaps via automorphisms of the universe type. However, constructively we can’t even say that there are any such automorphisms.”

At present all we know is that, constructively, there can’t be any automorphism of a universe that swaps the empty type with a non-empty type.

It is still open whether, constructively, there is (provably) a non-identity universe automorphism, as far as I know.

Posted by: Martin Escardo on August 13, 2021 9:22 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Thanks for the clarification, Martin. I didn’t phrase those lines well.

Posted by: David Corfield on August 13, 2021 10:23 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

But I am inclined to believe that there is no definable non-identity automorphism of the universe.

Posted by: Martin Escardo on August 13, 2021 11:31 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

I see Tarski closes out his article –What are Logical Notions? –arguing that whether or not mathematics is a part of logic depends on the foundational system used. Yes for Russell’s theory of types; No for set theory.

He has the idea that type theory as a monistic theory of logic and mathematics appeals more to philosophers, while mathematicians not wishing to have their subject reduced to logic prefer set theory.

Now we seem to live in an age when philosophers prefer set theory.

Posted by: David Corfield on August 17, 2021 9:47 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

What do you think he would think of Martin-Lof-style type theory? Or ETCS, for that matter?

Posted by: Mike Shulman on August 18, 2021 8:46 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Interesting question.

So the argument relies on being able to say what is the “universe of discourse” in each case. For set theories, this universe covers all sets, and there is an primitive, undefined binary relation of membership. Only identity, non-identity, and the empty and universal relations are logical, thus set membership is not.

For the type theory of Principia Mathematica the universe is constituted by a class of individuals, the subject of the transformations. These induce transformations in higher constructs - classes of individuals, relations between individuals, etc. Thus membership is preserved.

How would ETCS go? I guess that depends on the presentation. In Todd Trimble’s account it’s built up from a one-sorted theory of categories, the sort of morphisms. Am I then to consider whether the further notions are “logical” by considering any permutation of the class of morphisms? Clearly then little would be logical, such as the ternary relation of composition.

And MLTT? I’m really not sure Tarksi’s line of argument above helps here. Perhaps we fall back on the invariance idea as expressed in the main post for HoTT – any type formation operation must be invariant under equivalence of types used. Then mathematics coincides with logic.

Posted by: David Corfield on August 19, 2021 7:39 AM | Permalink | Reply to this

questions

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

What’s the name of the category containing itself as an object? And how to call an n-category which is contained as an object in one of its underlying 1-categories? How would that cyclicity break the 1..n labeling?

Thanks!

PS sorry for the OT, feel free to delete, not sure how to navigate the site and post to ask a general question to all of you. I’d love to hear from you though.

Posted by: Elio on August 21, 2021 3:34 AM | Permalink | Reply to this

Re: questions

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

I think this is a reasonable question to ask at math.stackexchange, it’s a bit more subtle that at first appears, but not something that usually comes up. If one is working in set theory with the Anti-Foundation Axiom it might be possible. But as you can see, it’s not the sort of thing that people generally worry about, as AFA doesn’t really impinge on how people do mathematics, day-to-day.

Posted by: David Roberts on August 22, 2021 2:24 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

Thank you, I think n-categories with the structure I described can model nontrivial entailment structures. Is anybody here familiar with (M,R)-systems?

How do I tackle math.stackexchange when not being a mathematician, hence my language not being formal enough? See here:

https://math.stackexchange.com/questions/4230351/on-n-categories-having-their-arrows-contained-in-their-underlying-1-categories/4230358#4230358

Please correct me if I’m wrong, a 2-category contains 1-category arrows as its objects. A 3-category contains 2-category arrows as its objects. What if the 3-category arrows are themselves objects in the underlying 1-category? Do we obtain any special structure?

Posted by: Elio on August 22, 2021 8:05 PM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

I think that it might be worth brushing up on the theory of categories a little bit first. I can’t parse what you are writing. It’s not a matter of being formal enough, but what you write having a meaning that I can process and respond to. A 2-category can have whatever objects it has, and $n$ -category can have whatever objects it has. I can’t figure out what you mean by your last couple of sentences. Similarly with your question at math.SE. Good luck with the applications, I’m afraid I can’t help you with those since I do not know what they are.

Posted by: David Roberts on August 23, 2021 1:52 AM | Permalink | Reply to this

Re: Logic as Invariant Theory Revisited

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

I should also point out that this blog is not for people to ask general questions in the process of learning category theory, sorry. If there’s something specific in a post you want to discuss, then that’s fine.

Posted by: David Roberts on August 23, 2021 1:54 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

August 11, 2021