Frucht's theorem without choice

Stream: maths

[Trebor Huang]

Frucht's theorem says every group is the automorphism group of some (simple, undirected) graph. This statement is provable in ZF, but it very crucially depends on the regularity axiom (!!). It is also provable with choice.

The gist of the proof with choice is to pick a well-order for a generating set, and we can construct the cayley graph with each edge marked with an ordinal. Since ordinals are very rigid, it's easy to construct decorations on the edge to guarantee no automorphisms mix up the markings. The proof in ZF uses induction on the rank of the generating set, which we don't have in a structural foundation like Lean. Is it possible to prove this theorem in Lean without choice? This is very probably not possible.

[Daniel Weber]

In Lean without choice you don't even have excluded middle

[Trebor Huang]

Daniel Weber said:

In Lean without choice you don't even have excluded middle

The proof in ZF doesn't use excluded middle either, if I read it correctly. So it is also provable in IZF.

[Daniel Weber]

Do you have a minimal example of a proof in IZF you aren't sure about in Lean without choice? I'm having some trouble understanding the problem here

[Trebor Huang]

As I said, the proof of this uses induction over the rank of a set to create a choice without actually invoking choice. What we need is enough pieces of "decorations" on a graph, so that distinct decorations cannot be mixed together via an automorphism, and there must not be any extra automorphisms induced by permuting the vertices inside that decoration.

[Trebor Huang]

ZF automatically provides us with such decorations: suppose we want to assign one decoration for each element in a set X, then for the element $x \in X$, we can just consider the $\in$-graph of the hereditary elements/transitive closure (i.e. elements, and elements of elements, and so on) of $x$! For example, the graph corresponding to $\{\varnothing, \{\varnothing\}\}$ has three vertices forming a triangle.

[Daniel Weber]

Is the statement you need basically that every set injects to some (constructive, to avoid choice) well founded order, or do you need more?
Thinking about this for a bit, I doubt this is provable without choice

[Trebor Huang]

It probably needs to be both well-founded and extensional (as in the extensionality axiom of ZF), to avoid spurious automorphisms.

[Daniel Weber]

Does this theorem fail in ZFA? I feel like that might be closer to type theory

[Trebor Huang]

Yes, it's independent of ZFA (but provable in ZFA + choice)

[Bhavik Mehta]

(deleted)

[Nir Paz]

I looked at the paper, it looks like we need that every type injects into some beth cardinal, which is immediate in ZF because the beth cardinals are just |V_a|.

I doubt this is true in lean even assuming LEM as an axiom, but I'm not sure. Either way this is really interesting! A very non-obvious effect of our choice of foundation on "normal" mathematical objects.

[Violeta Hernández]

How would you prove that Type injects into a beth number without knowing that it can be well-ordered?

[Violeta Hernández]

Even with choice, my understanding is that theorems such as #Type = #Ordinal are unprovable.

[David Michael Roberts]

Not that it is the final word, but Wikipedia claims that the two independent proofs of the infinite group case needed Choice. Where's a proof that this can be done in ZF? At the very least so it can be added to the WP page.

[David Michael Roberts]

Oh, ok, it's a preprint, here:

• Brian Pinsky, Frucht's Theorem without Choice, https://arxiv.org/abs/2305.11382