The strong soundness theorem for real closed fields and Hilbert's Nullstellensatz in second order arithmetic

By RCA₀, we denote a subsystem of second order arithmetic based on Δ₁⁰ comprehension and ∑₁ ⁰ induction. We show within this system that the real number system ℝ satisfies all the theorems (possibly with non-standard length) of the theory of real closed fields under an appropriate truth definition. This enables us to develop linear algebra and polynomial ring theory over real and complex numbers, so that we particularly obtain Hilbert's Nullstellensatz in RCA₀.