Return to Question

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:

$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.

The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.

The last part of this proof uses AC. I came across Kleppmann - Generating sets of free groups and the axiom of choice, which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.

I am interested in knowing how true this statement is constructively. I.e. are uses of excluded middle and choice (more rather statements weaker than choice) necessary to prove it?

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:

$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.

The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.

The last part of this proof uses AC. I came across Kleppmann - Generating sets of free groups and the axiom of choice, which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.

I am interested in knowing how true this statement is constructively. I.e. are uses of excluded middle and choice (or rather statements weaker than choice) necessary to prove it?

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:

$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.

The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.

The last part of this proof uses AC. I came across this article which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.

I am interested in knowing how true this statement is constructively. i.e. are uses of excluded middle and choice (more rather statements weaker than choice) necessary to prove it?

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:

$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.

The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.

The last part of this proof uses AC. I came across Kleppmann - Generating sets of free groups and the axiom of choice, which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.

I am interested in knowing how true this statement is constructively. I.e. are uses of excluded middle and choice (more rather statements weaker than choice) necessary to prove it?