This might not be the best introduction for someone who hasn't proved "a = b iff a - c = b - c", and e.g. may not be familiar with "if and only if," or the fact that P => Q is considered true if P is false, even if Q is also false.

Tangent: ever since highschool I've wondered about the schism between (a) the elements of "showing one's work" for algebra / calculus problems and (b) formal syllogisms to justify each step.

I have to wonder if highschool math would make more sense to some students if (a) and (b) were taught together.

I think the way society conceives if grade school math is pretty rotten, and we need to shake things up if only to build a new cultural relationship with it. Common core focusing on intuition is actually good, and someday throwing in theorem provers will add back a good challenge while keeping things approachable.

I might even cut polynomials entirely to make room for the new stuff and do informal calculus earlier.

Or like, just straight up get people to practice being shape rotators lol. Do picture of something in art class, ask them to draw it from a different perspective.

Math is ultimately about bridging the gap between fuzzy warm intuition and and cold artificial rigor. Focusing on either in isolation defeats the purpose.

That may be the case. Otoh, this is being used as an intro course for first year college students, who don't have any background in logic afaik. So perhaps it could work. I don't have enough information to say either way.

On the contrary wrestling with the computer allows one to internalize those things through experience.

For anyone that struggled with pure math because memorizing seemed less "big brained" than informal proofs, computers making thing concrete let alone gamified can help immensely.

> P => Q is considered true if P is false, even if Q is also false

It's a good thing then that this framing is rather unlike the intuitionistic mathematics actually suggested.

I find that the simplest way to understand P => Q is to express it as (!P or Q).