The Logic of Equation and Inequation Solving

An introductory example

Let `x_1, ..., x_n` be defined terms that contain no variables.

• e.g., `3`, `(1+sqrt(5))/2`
• not e.g., `a+1`, `3/0`

We want   `f(x) = 0 ⇔ x = x_1 vv … vv x = x_n`   to mean

`f(x)` is defined and yields 0   if and only if   `x = x_1 vv … vv x = x_n`.

• The equation comes as `7 sqrt(|x|-1) = x+9`, not as `-1 <= x <= 1 ^^ 7 sqrt(|x|-1) = x+9`.
• Try `x=5` in the intermediate step `(x < 0 ^^ 7 sqrt(-x-1) = x+9) vv (x >= 0 ^^ 7 sqrt(x-1) = x+9)`.

The undefined value of arithmetic

The undefined truth value

The reasoning operators ⇒ and ⇔

Reasoning in the logic

• This has not yet been fully studied, because
  MathCheck mostly only model checks, not proves.
• Many laws retain their traditional form.
• Thanks to regularity, `_|_` can usually be ignored
  • when both sides have the same minimal undefined subexpressions, and
  • with `rArr`.
• Otherwise adding “`|__f~| ^^`” often suffices.