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.
