Logical negation is not so simple.
In IEEE floating point number comparisons, NotANumbers a,b
a>b is false
a<b is false
a=b is false.
if a<b is "not known to be true" that does not mean it is "known to be
false".
There are also problems with intervals.
I think you can easily find a way of calculating with truth values 0,1 or
false/true in the first order predicate calculus. But it does not
solve anything interesting.
We could consider reading OTTER, a theorem prover, into Maxima,
and have something that was state of the art, instead of cooking
up our own. I have not looked at the details though.
RJF
Stavros Macrakis wrote:
>I agree *completely* that we ought to have a full set of mathematical
>boolean operations that operate sensibly with relational operators;
>indeed, I have been discussing this on and off the mailing list for some
>time.
>
>The way to do this is NOT to "remove the implicit 'IS' from 'NOT'". It
>is to write a full set of simplifying boolean operators for truth
>values, and adjusting the compar package accordingly. This is a
>reasonable project for someone to undertake. Of course, it would be
>nicer if we also handled quantifiers, and sets, and incorporated some
>sort of theorem prover, and.... But let's start with the easy stuff.
>
>-------------------------------------------
>
>As for handling negation of relations, it is easy enough to write your
>own function to do this:
>
> makelist(negate_relation[x[1]]: x[2], x,
> [["<",">="],["<=",">"],["=","#"],[">=","<"],[">","<="],["#","="])$
>
> negate_relation(ex):=
> if atom(ex) or not member(op(ex),["<","<=","=",">=",">","#"])
> then error("Can only negate relations, not",ex)
> else funmake(negate_relation[op(ex)],args(ex))$
>
>-------------------------------------------
>
>Some other comments on the discussion:
>
>Robert Dodier:
>
>
>
>>>I would suggest instead that we remove the implicit
>>>"IS" from "NOT".
>>>
>>>
>
>Alexander Vidybida:
>
>
>
>>I agree with this suggestion in a sence that the less
>>implicit things are in a system the less a beginner hits them
>>while learning how to use the system.
>>
>>
>
>a) I don't think it is meaningful to call the current semantics of NOT
>'implicit'. They are just its semantics.
>
>b) If you want to characterize this as 'implicit', then there is a huge
>number of 'implicit' things in any system like Maxima, and they are
>necessary for the system to work.
>
>c) Changing NOT without changing AND, OR, and maybe even IF will make
>the system *less* consistent, not more.
>
>The real problem here has nothing to do with implicitness. It has to do
>with the fact that AND/OR/NOT/IF are currently *programming*
>(evaluating) operations and not *mathematical* (simplifying) operations.
>
>----------------------------------------------
>
>I agree that is((NOT 1>3)=(1<=3)) => false is confusing, especially
>since is((NOT 1>3)=NOT NOT (1<=3)) => true. There are several confusing
>things, in fact. One is that NOT is a programming operation, while "="
>is a simplifying operation. Another is that "=" is syntactic. But the
>bottom line is that Maxima is simply not currently designed to handle
>things like this.
>
>In fact, Maxima is even 'uncomfortable' with things like this at the
>syntactic level. For example, "true = not false" gives a syntax error.
>Presumably this is intended to catch things like a=b=c where they intend
>(a=b) and (b=c).
>
>---------------------------------------------------
>
> -s
>
>_______________________________________________
>Maxima mailing list
>Maxima@www.math.utexas.edu
>http://www.math.utexas.edu/mailman/listinfo/maxima
>
>