Processing math: 0%

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!

$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)$ 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))$ .

$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