The Undefined Value of Arithmetic

We want substitution of an expression for a free variable always be allowed

• `sqrt(x)` must not imply that we are only talking about non-negative reals
• otherwise the root 3 would be lost in the following:

  `11 sqrt(|x|+1) = 25 - x ⇔`
  `(x < 0 ^^ 11` `sqrt(1-x)` `= 25 - x)``vv``(x >= 0 ^^ 11 sqrt(x+1) = 25 - x)`

Each undefined expression must yield a “value”

• we will see that one value suffices
• we denote it with `_|_`

Let `f` and `g` be expressions without free variables

• if `f` contains an undefined subexpression but `f` yields `a` for some `a in RR`,
  then `f = x` has a wrong root `x = a`

  arithmetic must be regular á la Kleene:
  undefined argument guarantees undefined result

• if `f = g` yields T although `f` or `g` is undefined,
  then each `x in RR` is its wrong root

  `frac(1)(0) = frac(1)(0)` does not yield T, so ”`=`“ is not reflexive!

We also want to solve `f(x) > 0` and so on

if `f` or `g` is undefined, then none of `f = g`, `f < g`, `f <= g`, … yields T

• so we cannot distinguish between different undefineds, so a single `_|_` suffices
  (we could build that ability to the logic but we do not want to)