The Undefined Truth Value

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

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

Also this is regular:

No logic function can be written such that `varphi(P)` yields T iff `P` is U.
No predicate can be written such that `varphi(x)` yields T iff `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.

However, for each expression `f` there is a predicate `|__f~|`
that yields F if `f` yields `_|_` and T otherwise.

Similarly for each predicate

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