Let `frac(1)(x) > 0` mean that `frac(1)(x)` is defined and yields a positive value.

`EE y: xy = 1 ^^ y > 0`

Then traditional logic on real numbers yields a wrong root:

`frac(1)(x^2) <= 0` `hArr` `not(frac(1)(x^2) > 0)` `hArr` `not(EE y: x^2 y = 1 ^^ y > 0)` `hArr` `AA y: (x^2 y != 1 vv y <= 0)` `hArr` `x = 0`

The problem is that “is defined and” may be within the scope of negation.

Sound systems can be built on that basis, but they

- involve an unnatural distinction of predicates to two classes:

`_|_` yields**F**and `_|_` yields**T**, and - require care with when and where to write “is defined and”.

We find it easier to introduce an “undefined” truth value
**U** á la Kleene.

- The negation of undefined should be undefined as well!
`not` `^^` **F****U****T**`vv` **F****U****T**`rarr` **F****U****T**`harr` **F****U****T****F****T****F****F****F****F****F****F****U****T****F****T****T****T****F****T****U****F****U****U****U****F****U****U****U****U****U****T****U****U****U****T****U****U****U****U****T****F****T****F****U****T****T****T****T****T****T****F****U****T****T****F****U****T** - `varphi vv zeta` is `not(not varphi ^^ not zeta)`,

`varphi rarr zeta` is `not varphi vv zeta`, and

`varphi harr zeta` is `(varphi rarr zeta) ^^ (zeta rarr varphi)`.

Also this is regular:

- `varphi(…, `
**U**`, …)` either yields**U**or is independent of that argument. - `varphi(…, _|_, …)` either yields
**U**or is independent of that argument.

No logic function can be written such that `varphi(P)` yieldsTiff `P` isU.

No predicate can be written such that `varphi(x)` yieldsTiff `x` is `_|_`.

Example: the correctness of `varphi(1/(1//x)) rArr x ne 0 ^^ varphi(x)`
relies on `varphi` being regular and not identically **T**.

- We have `1/(1//x) ge 0 rArr x ne 0 ^^ x ge 0 hArr x > 0`,

but not `1/(1//x) ge 0 vv y^2 ge 0 rArr x ne 0 ^^ (x ge 0 vv y^2 ge 0)`

and not `"undefined"(1/(1//x)) rArr x ne 0 ^^ "undefined"(x)`. - This is why we use Kleene →, not Łukasiewicz →.

However, for each expression `f` there is a predicate `|__f~|`

that yields **F** if `f` yields `_|_` and **T** otherwise.

- `|__x~|` :=
**T**when `x` is a constant or variable symbol. - `|__frac(f)(g)~|` := `|__f~| ^^ |__g~| ^^ g != 0`
- It never yields
**U**!

- `|__f = g~|` := `|__f~| ^^ |__g~|`
- `|__not varphi~|` := `|__varphi~|`
- `|__varphi ^^ zeta~|` := `(|__varphi~| ^^ |__zeta~|) vv (|__varphi~| ^^ not varphi) vv (|__zeta~| ^^ not zeta)`

`not |__1/(1//x)~| rArr x ne 0 ^^ not |__x~|` does not arise because

- `not |__1/(1//x)~|` is `x=0`,
- so it is not of the form `varphi(1/(1//x))`.