The Logic of Equation and Inequation
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 to mean
`f(x)` is defined and yields 0 if and only if
`x = x_1 vv … vv x = x_n`.
Restricting the domain to start with does not solve the problem.
- The equation comes as ,
not as .
- 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.