Can you constructively prove a univariate polynomial algebra over a Jacobson ring is itself Jacobson?

Question

Recall the Jacobson radical of a commutative ring $\mathrm J(A)=\lbrace a\in A\mid \forall b\in A:1-ba\in A^\times\rbrace$. The Jacobson radical of a quotient by an ideal $I\vartriangleleft A$ is therefore $\mathrm J(A/I) =\lbrace a+I\in A\mid \forall b\in A:1-ba\in (A/I)^\times\rbrace$. If I am unpacking correctly, $a+I\in \mathrm J(A/I)$ means $$\forall b\in A\exists c\in A:1-c(1-ba)\in I.$$

The nilradical of the quotient is $\mathrm{nil}(A/I)=\lbrace a+I\mid \exists n\in \mathbb N:a^n\in I \rbrace$. Hence, to prove $\mathrm J(A/I)\subset \mathrm{nil}(A/I)$ it suffices to prove:

$$[\forall b\in A\exists c\in A:1-c(1-ba)\in I]\implies a\in \sqrt I.$$

Question 1. How to constructively prove this implication for $A=R[x]$ (with $R$ a Jacobson ring) and, say, a non-radical principal ideal like $\langle x^n \rangle$?

When $R=\Bbbk$ is a field then I see how to prove the contrapositive for all sorts of ideals. For instance $a\notin \sqrt{\langle x^n\rangle} $ means $a\in \Bbbk[x]$ has a nonzero free coefficient, so letting $b\in \Bbbk$ be its inverse we find $1-ba\in \langle x\rangle$...

Question 2. How to prove (hopefully without prime ideals) the contrapositive for ideals $I\vartriangleleft R[x]$ involving irreducibles, or non-principal ideals?

Answer 1

The statement that if $R$ is Jacobson (i.e., $\mathrm{J}(R/I)\subseteq\mathrm{Nil}(R/I)$ for every ideal $I$ of $R$) then so is $R[X]$ is constructively provable. The proof is in this preprint of mine.

• A constructive proof of general Nullstellensatz for Jacobson rings, arXiv:2406.06078 [math.AC]

The proof is the same as the classical one in Matthew Emerton's PDF. You can eliminate the use of prime ideals and maximal ideals by using the idea of entailment relations. See Peter Schuster and Daniel Wessel, Syntax for Semantics: Krull’s Maximal Ideal Theorem for details.