A group is not the union of two subgroups, constructively.

Question

Let $G$ be a group, and let $H$ and $K$ be subgroups of $G$. The following is well-known:

Proposition 1. If $H \cup K = G$, then $H = G$ or $K = G$.

See, for instance, this answer.

Question. Is proposition 1 provable in intuitionistic first-order logic?

The standard proof can be interpreted intuitionistically as a proof for a weaker claim:

Proposition 2. If there is an element of $H$ not in $K$, and an element of $K$ not in $H$, then $H \cup K \ne G$.

Note that proposition 2 is (prima facie) even weaker than the contraposition of proposition 1:

Proposition 3. If $H \ne G$ and $K \ne G$, then $H \cup K \ne G$.

On the other hand, we can derive the contraposition of proposition 2 from the contraposition of proposition 3: this is because $\lnot \lnot ((H = G) \lor (K = G))$ is logically equivalent to $\lnot ((H \ne G) \land (K \ne G))$, and the latter implies $\lnot ((\exists g : G . g \notin H) \land (\exists g : G . g \notin K))$.

Answer 1

"Provable intuitionistically" is too vague for a specific answer.

But, in at least one interpretation (intuitionistic type theory $\text{HA}^\omega$), a natural statement of the principle in question is not provable. If it was, we would also be able to prove that for every sequence $(G_n, H_n, K_n)$ of instances of the problem, there is a sequence $(m_i)$ such that for each $n$, $m_n = 0$ if $G_n = H_n$ and $m_n = 1$ if $G_n = K_n$. Moreover, the sequence $(m_i)$ would be computable relative to the sequence of instances. But it is a straightforward exercise in computable algebra to construct a uniformly computable sequence of instances for which the sequence $(m_i)$ is not computable.

This all follows e.g. from the results in my paper with Jeff Hirst, "Reverse Mathematics and uniformity in proofs without excluded middle", if we view groups in the signature $(\cdot, e, {}^{-1})$ which is natural for constructive treatments of groups. In that signature, there is a universal axiomatization of groups and a universal definition of a subgroup of a group, and so the results in the paper by Hirst and me apply.

Answer 2

Here is a different way of seeing that the principle in the question is not constructively provable. We will reason informally, constructively, and show that the principle in the question implies the lesser limited principle of omniscience (LLPO).

LLPO: For any sequence $a_0, a_1, \ldots$ of natural numbers such that each $a_i$ is either $0$ or $1$, and such that at most one $a_i$ is nonzero, the following holds: either $a_{2i} = 0$ for all $i$, or $a_{2i+1} = 0$ for all $i$,

Because LLPO is not constructively valid, this shows that the principle is not constructively valid either.

We will let $G = (Z_2)^\omega$, a countable product of $Z_2$ with itself. This group is generated by a sequence $(g_i)$ of elements, which commute with each other, such that $g_i^2 = e$ for each $i$. A typical element of $G$ is thus of the form $g_{i_1}\cdots g_{i_k}$ for some sequence $i_1 < \cdots < i_k$ of natural numbers.

Let $(a_i)$ be a sequence of naturals numbers each of which is $0$ or $1$. We proceed inductively. At stage $2i$, if $a_{2i} = 0$, we put into $H$ the element $g_i$ and also put in the product of $g_i$ with every element already in $H$. At stage $2i+1$, if $a_{2i+1} = 0$, we put into $K$ the element $g_i$ and also put in the product of $g_i$ with every element already in $K$. Note that $H$ and $K$ are decidable; to tell whether an element $g_{i_1}\cdots g_{i_k}$ is in one of them, we only need to examine the sequence $a_{i_1},\ldots, a_{i_k}$ and ask whether it contains a nonzero element.

We must verify $G = H \cup K$. Let $g = g_{i_1}\cdots g_{i_k}$ be an element of $G$. By assumption, at most one of the sequence $a_{i_1},\ldots, a_{i_k}$ is nonzero (and the set of nonzero naturals is, of course, a decidable set). If none is zero, $g \in H$. If the one that is zero has an odd index, $g \in H$. If the one that is zero has an even index, $g \in K$. It is still true constructively that every natural number is either even or odd, so this proves that $G = H \cup K$.

Thus, by the principle in the question, $G = H$ or $G=K$. But if we assert $G = H$, then we assert that $g_i \in H$ for all $i$, so we assert that $a_{2i} = 0$ for all $i$. Similarly, if we assert $G = K$ we assert $a_{2i+1} = 0$ for all $i$. That is what we needed to show for LLPO.

This construction is the sort of thing I had in mind in my other answer as the "exercise in computable algebra", but perhaps it is easier to follow when written in terms of LLPO without the detour into uniformization.