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!

• `|__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))`.