Decidability of real closed fields (RCF)
Osnova sekce
-
Tarski's elementary geometry can be interpreted in RCF, which Tarski showed in decidable. Key facts are that (N,+,x,0,1) is undecidable, N can be defined in (Z,+,x,0,1) so (Z,+,x,0,1) is undecidable. By J. Robinson's result (see file) Z is definable in (Q,+,x,0,1), hence (Q,+,x,0,1) is undecidable. However, by Tarski's result, the first-order axiomatization of (R,+,x,0,1) is decidable. In particular, there is no first-order definition of N, Z, Q in (R,+,x,0,1).