Pondering: Negative trait promises

Well, it's not quite a contradiction -- even setting aside questions of semver, classical logic, and so forth!

What A :- not B is saying is: "one way to prove that A is true is by B being false". Similarly B :- not A. This does not imply that this is the only way to prove that A is true -- it's just one way.

So, for example, given the rules above, A and B could both be true -- but you would need some further rules (perhaps added by other impls) to justify that.

Just going by those two impls, you cannot say that A is true or B is true but you also cannot say that either one is definitely false. Or, to put it another way, you would be justified in concluding that A is false, but you are equally justified in concluding that B is false!

The problem is that whichever of those conclusions you try to reach, you then wind up proving up disqualifying the other. So the problem here is not no solutions, it is rather that you have multiple, equally valid, contradictory solutions -- you could either say that (A, not B) or (not A, B). But we are trying to answer a simpler question: is A true or not? And we can't answer that without also answering something about B.

(There are other ways to evaluate logical programs. e.g., with Answer Set Programming, you actually get back multiple sets of answers... so in this case you would get something like [(A, not B), (B, not A)]. But we have now reached the limit of my knowledge about ASP, since I never dug that far into it -- it didn't seem appropriate for a setting like Rust.)

1 Like