Simplify uses Kleene's truth tables and evaluation is strict in NaN, so the annihilation and absorption rules disagree with the values they stand for #880

Split out of #876, where conditioning the order-comparison rules one at a time was clearly not the fix for this. Measured on master at 363edfa3, .NET 10, default settings.

and and or are strict in NaN

(i < 0) and False   ->  NaN
(i < 0) or  True    ->  NaN
not (i < 0)         ->  NaN
False implies (i < 0)     ->  NaN
(i < 0) implies (i < 0)   ->  NaN
(i < 0) xor (i < 0)       ->  NaN

NaN absorbs everything, including the cases a truth table settles without looking at the undefined operand. Under the three-valued logic usually meant here — Kleene's — False and u is False and True or u is True, because no value of u can change the answer.

Whichever is intended, the rule table does not match it. Patterns.Boolean.cs decides all of these:

Orf(var any1, var any2) when (any1 == True || any2 == True) ...  => True.Provided(...)
Andf(var any1, var any2) when (any1 == False || any2 == False) ... => False.Provided(...)
Impliesf(var any1, var any1a) when any1 == any1a ... => True
Xorf(var any1, var any1a) when any1 == any1a ... => False.Provided(...)

so Simplify gives the Kleene answer and evaluation gives the strict one:

"True or (True and (x < 0))".Simplify()            ->  True
"True or (True and (x < 0))" at x := i, as written ->  NaN

The absorption rules (Patterns.Boolean.cs:53-63) are in the same position: a or (a and b) reduces to a, and at a = True, b = NaN the original is NaN while a is True.

Why this is one question and not fifteen

#876 conditioned the rules that decide a pair of order comparisons, where the condition is a real statement about the operands (x in RR) and the reduction is genuinely conditional. These are different: there is no condition to attach, because the answer does not depend on the undefined operand at all. True or u is True for every u a three-valued logic admits. Attaching provided ... to each of them would be noise standing in for a semantics decision that has not been made.

So the fork is:

• Evaluation becomes Kleene — False and NaN is False, True or NaN is True, not NaN stays NaN. Annihilation, absorption and distributivity become sound as written, and no rule needs touching. It is a behaviour change in evaluation for anyone relying on NaN propagating.
• Evaluation stays strict — then the rules above are all unsound and have to withdraw their answers, which loses reductions that look basic and are relied on.

I have not measured how much of the suite pins strict propagation, so I am not proposing one over the other here.

What survives either way

Excluded middle. p or not p needs p to have a truth value, and no arrangement of the connectives supplies one, so #876's conditioning is still the right shape for those. Kleene would not make NaN or not NaN anything but NaN.

What I am not claiming

That Kleene is what AngouriMath intends -- the strictness may be deliberate and I found no comment either way. That the rule list above is exhaustive: it is what reading Patterns.Boolean.cs for this shape turned up, not the result of enumerating the table against the evaluator.