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
• 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`, …)` yields U

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 `_|_`.

• `"dom"_x` := T when `x` is a constant or variable symbol
• `"dom"_frac(f)(g)` := `"dom"_f ^^ "dom"_g ^^ g != 0`
• it never yields U!

• `"dom"_(not varphi)` := `"dom"_varphi`
• `"dom"_(varphi ^^ zeta)` := `("dom"_varphi ^^ "dom"_zeta) vv ("dom"_varphi ^^ not varphi) vv ("dom"_zeta ^^ not zeta)`