The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be done by a simple calculation using the binomial theorem.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent (for, otherwise, the localization at $x+y$ would have a prime ideal, and this corresponds to a prime ideal in the given ring not containing $x+y$).

The general existence of prime ideals [is equivalent][1] to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra and algebraic geometry. Moreover, it can be made "constructive", well at least provable in ZF, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. [There is][2] a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. My question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example would be: How to come up with the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ using the prime ideal proof? By the latter I mean $$V(I^n+J^n)=V(I^n) \cap V(J^n) = V(I) \cap V(J)=V(A)=\emptyset.$$ A more sophisticated example can be found [here][3], where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question. [1]: Existence of prime ideals and Axiom of Choice. [2]: http://www.sciencedirect.com/science/article/pii/016800728390012X [3]: http://math.stackexchange.com/questions/919933/the-kernel-of-r-to-a-otimes-r-b-is-nil

The sum of two nilpotent elements of a commutative ring is nilpotent. This can be checked by a direct calculation using the binomial theorem. In fact, this calculation shows the stronger statement $x^n=y^m=0 \Rightarrow (x+y)^{n+m-1}=0$.

But we can also give a more sophisticated proof: If $x,y$ are nilpotent, they are contained in every prime ideal. Hence, the same is true for $x+y$. Hence, $x+y$ is nilpotent: otherwise, the localization at $x+y$ would be non-zero and therefore have a prime ideal, but this corresponds to a prime ideal in the given ring not containing $x+y$. (In short: The set of nilpotent elements is the intersection of all prime ideals, hence closed under addition.)

The general existence of prime ideals is equivalent to the Boolean Prime Ideal Theorem and therefore the proof above is not constructive. The proof shows nothing about the nilpotence exponent of the sum. On the other hand, it is quite elegant and it is really a no-brainer if you are used to commutative algebra. Moreover, it can be made "more constructive" (not really constructive, as Matt F. points out), or at least provable in $\mathsf{ZF}$, as follows:

We restrict our attention to the subring generated by $x,y$. This ring is countable. The same is true for the localization at $x+y$. There is a constructive proof that every non-trivial countable commutative ring has a maximal ideal, hence has a prime ideal. And now we may proceed as before.

So we have two constructive proofs: (a) the direct calculation using the binomial theorem, (b) the proof using prime ideals. The question is: Assume that we know the proof (b), is there a general method how to produce the proof (a) from it? Perhaps even including the stronger statement about the nilpotence exponent? This is just a toy example for the general question how to get rid of prime ideals in proofs in commutative algebra where we would expect to have, or already know, more direct proofs. I have only picked this toy example because I hope that the general method can be easily explained with it.

Another toy example: How to produce the direct proof of $I+J=A \Rightarrow I^n+J^n=A$ for ideals $I,J \subseteq A$ from the proof using prime ideals? A more sophisticated example can be found here, where I have no idea how a direct calculation looks like (perhaps I will ask this in a separate question).

I know that Thierry Coquand and Henri Lombardi have worked on related questions, but after some skimming through their work I couldn't find an answer to my question.