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
`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
No logic function can be written such that `varphi(P)` yields T iff `P` is U.However, for each expression `f` there is a predicate `"dom"_f`
No predicate can be written such that `varphi(x)` yields T iff `x` is `_|_`.