Order of operations for logic seems wrong: AND is not taking priority over IMPLIES

[LukeLongworth]

I started discussing this on Zulip but I've become convinced its a bug so I moved it here.

In short: I think the order of operations for logical operators is incorrect, because expressions featuring both implies and and will resolve from left to right instead of giving priority to the and.

I checked various expressions of the form p OPERATOR q OPERATOR r with STACK's logic_equiv function and noted down the equivalence classes generated. Here is what I found:

• and and or are commutative, and implies is not (as expected!)
• and always takes priority over or (we teach that this is ambiguous, but there doesn't seem to be a universal agreement on this and I don't see this as a problem)
• or takes priority over implies; e.g. p implies q or r is equivalent to p implies r or q, but it is not equivalent to r or p implies q (as expected!)
• and and implies resolve from left to right. e.g. p implies q and r is not equivalent to p implies r and q (not as expected!)

I'm pretty sure this is a bug; it feels very strange that and takes priority over or which takes priority over implies, but that and does not take priority over implies. I'm not aware of any reason why this would be the case (though I am a bit of a novice in this particular field).

I also haven't tested further with the not, xnor, nor or nand operators.

The issue that brought this to light is that STACK will only put parentheses around expressions when it is strictly necessary. This means that the expression (p implies q) and r will display as p implies q and r, which makes students think we mean p implies (q and r) due to order of operations. This has caused some confusion in our cohort and to remedy the issue I am needing to use disp_parens in the question, which feels like an unwieldy workaround in this case.

[sangwinc]

Thanks for raising this @LukeLongworth, much appreciated. This is ironic because I recently wrote a paper about order of operations! I think these orders are basically arbitrary in the sense of not having compelling mathematical reasons for choosing one over the other. However there are strong conventions, e.g. "binds more tightly than +, so that `a+bc=a+(b*c)`.

I don't know the convention for implies. It's quite possible we didn't follow it. It's also quite possible there is no convention here either!

I copied over a maxima contributed package here https://github.com/maths/moodle-qtype_stack/blob/master/stack/maxima/stack_logic.lisp#L3

It would be relatively easy to change the binding power here https://github.com/maths/moodle-qtype_stack/blob/master/stack/maxima/stack_logic.lisp#L55 but then we'd be out of step with Maxima https://sourceforge.net/p/maxima/code/ci/master/tree/share/logic/logic.lisp

Could you contact Alexey Beshenov al@beshenov.ru who wrote this package and ask him? I think this is an issue to raise on the Maxima community rather than here. If they accept your proposal then I'll copy this across to STACK.

[sangwinc]

@LukeLongworth you might also have a look and see if this is specified in

@MANUAL{ISO80000-2:2019,
  TITLE =        {ISO80000-2:2019. Quantities and units -- Part 2: Mathematics},
  organization = {International Organization for Standardization},
  edition =      {ISO80000-2},
  year =         {2019},
}

My experience of developing STACK is that a lot of issues like this turn out to be ambiguous and interesting! @aharjula and I had this experience looking at the rules for significant figures.

[LukeLongworth]

Thanks @sangwinc, I'll have a closer look at these. We had an interesting discussion within the teaching team about the history of ordering operations. The historical rabbit hole is fascinating!

At least according to Epp's Discrete Mathematics with Applications (the textbook the course is largely built from), implies should take lower priority than and and or. This textbook also teaches that and and or are of equal priority so p and q or r is ambiguous and needs parentheses. It is clear that there is no truly universal rules with these sorts of things.

I'll let you know where this goes!