Virtual Substitution & Real Arithmetic

Synopsis

This chapter advances the understanding of real arithmetic by generalizing the ideas from the previous chapter to linear and quadratic inequalities. As in the previous chapter, the main workhorse will again be virtual substitutions that pretend to substitute a generalized expression into a logical formula by equivalently rephrasing each occurrence. The required virtual substitutions will, however, go beyond square root substitutions but cover infinities and infinitesimals, instead, in order to capture the fact that inequalities can also be satisfied without satisfying equality.