PRIME AND MAXIMAL IDEALS IN CONSTRUCTIVE RING THEORY

Abstract

The basic notions of ideal theory are examined constructively in the context of a commutative ring with an identity and an inequality relation. Constructive analogues of classical theorems relating maximality and primeness are proved, and it is shown that the results are the best possible in a constructive framework.

ACKNOWLEDGMENT

I am most grateful to Fred Richman and, especially, to Peter Schuster for kindly commenting on drafts of this paper, and thereby helping me to improve its presentation.

Notes

¹Mines et al. define a principal ideal ring differently, but for discrete rings, as defined in Section 2 of this paper, their definition is equivalent to ours; see page 115 of [13].

²The statement

is equivalent to Markov's Principle,

If (an ) is a binary sequence that such that ¬ ∀ n (an = 0), then there exists n such that an = 1.

Since this principle, a form of unbounded search, is independent of Heyting arithmetic (see pages 137–138 of [8]), neither it nor any statement equivalent to it is a part of our constructive mathematics.

³A set S is nonempty if ∃x (x ∈ S); to establish this property, it is not enough to prove that ¬(S = ).

⁴Note that although the ring Z of integers is discrete, the ring R of real numbers is not, since statement (1) with R = R entails LPO. (To see this, let (an) be a binary sequence and consider the real number whose binary expansion is 0 · a ₁ a ₂….) But we can prove that if a, b ∈ R and a < b, then for each x ∈ R either x > a or x < b.

⁵This example and the observation that a weakly fnite domain is a field were communicated to the author by Fred Richman.