10
$\begingroup$

Wedderburn's Theorem states that every finite division ring is commutative. Perhaps even more surprising, this implies that every finite reduced ring is commutative. The proofs that I am aware of always follow a proof by contradiction. If a finite division ring is not commutative, its center is proper, blablabla, contradiction. Formally, this just proves that finite division rings are not not commutative, and we need the law of the excluded middle to finish the proof. This naturally leads to the following question:

Question. Does the Wedderburn Theorem hold constructively, i.e. in Intuitionistic Logic?

I believe that the answer is No. Incidentally, I have recently proven "variants" of the Wedderburn Theorem constructively, and I want to know if there is literature on this topic.

Improve this question
$\endgroup$
19
  • 1
    $\begingroup$ Irrelevant comment: it is usually called "Wedderburn's little theorem" (to distinguish it from the Wedderburn-Artin theorem, I would guess). $\endgroup$
    – Sam Hopkins
    Commented Sep 23, 2023 at 20:27
  • 3
    $\begingroup$ Wedderburn's Theorem is going to boil down to a $\Pi^0_1$ statement (i.e., for all natural numbers, something computably checkable happens) by encoding finite rings as natural numbers. Heyting arithmetic is $\Pi^0_2$ conservative over Peano arithmetic, so assuming that the theory is provable in PA, it will be provable in HA. $\endgroup$
    – James E Hanson
    Commented Sep 23, 2023 at 20:27
  • 4
    $\begingroup$ Technically this is going to be sensitive to your definition of 'finite.' If by finite, you mean that the set is in bijection with an explicitly given natural number, then commutativity of the ring is going to satisfy excluded middle (in that you can just explicitly check whether the ring satisfies commutativity). $\endgroup$
    – James E Hanson
    Commented Sep 23, 2023 at 20:29
  • 4
    $\begingroup$ Actually, $\neg\neg\forall x,y\in X\,xy=yx$ implies $\forall x,y\in X\,xy=yx$ assuming only the stability of equality on $X$ (which holds for subfinite $X$ as well). $\endgroup$
    – Emil Jeřábek
    Commented Sep 23, 2023 at 20:57
  • 3
    $\begingroup$ Maybe an amusing note: Let a division ring coordinatize a projective plane. Then the plane is Desarguesian, and it is Pappian if and only if the division ring is commutative. So geometrically, Wedderburn's Theorem amounts to show that a finite Desarguesian plane is Pappian. As far as I know, there is no purely geometric proof for that. $\endgroup$
    – Peter Mueller
    Commented Sep 25, 2023 at 6:23

0

Reset to default