Can the type of truth values be given the structure of a group?

When attempting to prove a theorem, not discussed in this post, I tried to give a certain set the structure of a group. After failing repeatedly, my proof attempts led me to consider a miniature version of the problem: can \Omega, the object of truth values, be given the structure of a group?

This question makes sense in 1-topos theory, in \infty-topos theory and in HoTT/UF, where in the latter a truth value is a type with at most one element, also known as a proposition (and sometimes as an h-proposition or as a mere proposition).

The answer to the question, in all cases, turns out to be that \Omega can be given the structure of a group if and only if the topos is boolean.

Reasoning in the internal language, or the type theory, the argument is as follows.

If the topos is boolean, that is, excluded middle holds in the internal language, then trivially \Omega has precisely two group structures, and \Omega endowed with each of them gives rise to two isomorphic groups.

It is the converse that is interesting.

We use “Higgs’ Involution Theorem”, which says that every left-cancellable map f : \Omega \to \Omega is an involution, that is, f (f p) = p.

If a group structure (\oplus , 0) on \Omega is given, by Higgs’ involution
theorem we conclude that it is abelian with p \oplus p=0 for every p:\Omega
(where it is unspecified which element of \Omega the zero element of the
group is – it can be \text{false}, \text{true}, or any element of \Omega).

Now define f(p) = p \oplus \text{false} \oplus \text{true}.

Then we have the following chain of logical equivalences:

f(p)

\iff f(p) = \text{true}

\iff p \oplus \text{false} \oplus \text{true} = \text{true}

\iff p \oplus \text{false} = 0

\iff p = \text{false}

\iff \lnot p.

Hence f(p) = \lnot p by propositional extensionality (or univalence for propositions, in the case of HoTT/UF).

But f(p), being a group action, is an automorphism and hence an
involution by Higgs’ theorem (or already by the above consequences of
Higgs’ theorem and direct calculation), which amounts to \lnot\lnot p = p, and
therefore excluded middle holds.

This argument is also written here in Agda, with a weaker assumption, namely that \Omega is given the structure of a left-cancellative monoid, including a proof of Higgs Involution Theorem.

I wouldn’t be surprised if this fact is already available in the literature or the folklore. Is it?

About Martin Escardo

https://www.cs.bham.ac.uk/~mhe/
This entry was posted in Uncategorized. Bookmark the permalink.

1 Response to Can the type of truth values be given the structure of a group?

  1. Update: none of the topos theorists we asked, including Peter Johnstone, were aware of the fact that the object of truth values can be a group only in a boolean topos.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s