A proof of $\dim(R[T])=\dim(R)+1$ without prime ideals?

Background. If $R$ is a commutative ring, it is easy to prove $\dim(R[T]) \geq \dim(R)+1$, where $\dim$ denotes the Krull dimension. If $R$ is Noetherian, we have equality. Every proof of this fact I'm aware of uses quite a bit of commutative algebra and non-trivial theorems such as Krull's intersection theorem. It is worth mentioning that Gelfand-Kirillov dimension satisfies $\mathrm{GK}\dim(R[T])=\mathrm{GK}\dim(R)+1$ for every $K$ -algebra $R$. T. Coquand and H. Lombardi have found a surprisingly elementary, first-order characterization of the Krull dimension that does not use prime ideals at all. T. Coquand, H. Lombardi, A Short Proof for the Krull Dimension of a Polynomial Ring, The American Mathematical Monthly, Vol. 112, No. 9 (Nov., 2005), pp. 826-829 (4 pages) You can read the article here. Here is a summary. For $x \in R$ let $R_{\{x\}}$ denote the localization of $R$ at the multiplicative subset $x^{\mathbb{N}} (1+xR) \subseteq R$. Then we have $$\qquad \dim(R) = \sup_{x \in R} \left(\dim(R_{\{x\}})+1\right)\!. \label{1}\tag{$\ast$}$$ It follows that for $k \in \mathbb{N}$ we have $\dim(R) \leq k$ if and only if for all $x_0,\dotsc,x_k \in R$ there are $a_0,\dotsc,a_k \in R$ and $m_0,\ldots,m_k \in \mathbb{N}$ such that $$x_0^{m_0} (\cdots ( x_k^{m_k} (1+a_k x_k)+\cdots)+a_0 x_0)=0.$$ You can use this to define the Krull dimension. This new characterization of $\dim(R) \leq k$ can be seen as a statement in first-order logic (whereas the usual definition with prime ideals uses second-order logic): Use two sorts $N,R$, the usual ring operations for $R$, but also the "mixed" operation $N \times R \to R$, $(n,x) \mapsto x^n$. Every ring becomes a model of this language. A consequence of this is a new short proof of $\dim(K[x_1,\dotsc,x_n])=n$, where $K$ is a field. Using Noether normalization and the fact that integral extensions don't change the dimension, it follows that $\dim(R\otimes_K S)=\dim(R)+\dim(S)$ if $R,S$ are finitely generated commutative $K$ -a