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

• 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!
     F U T     F U T     F U T not ^^ vv rarr harr T F F F F U T T T T T U F U F U U U U T U U T U U U F F U T T T T F U 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) 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.

• 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!
Similarly for each predicate
• |__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)).