The Logic of Equation and Inequation Solving

An introductory example

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

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`.
Restricting the domain to start with does not solve the problem.

The undefined value of arithmetic

The undefined truth value

The reasoning operators ⇒ and ⇔

Reasoning in the logic