Using the mathematical typography of formal logic

Question

As asked in this question, I strongly prefer to use "mathematical" typography in Mathematica over text-based ("computer science") typography. Nevertheless, it sometimes fails for no reason I can discern.

Here's a text-based proof from formal logic:

basicAxioms = {ForAll[{a, b}, And[a, b] == And[b, a]],
   ForAll[{a, b}, Or[a, b] == Or[b, a]]};

mybasicProof = FindEquationalProof[And[a, b] == And[b, a], basicAxioms]

which yields a perfectly normal proof, as can be seen by

mybasicProof["ProofGraph"]

But the (apparently) equivalent set of axioms and proof, expressed in mathematical typography, fails:

basicAxioms2 = {
   \!\(
\*SubscriptBox[\(\[ForAll]\), \(\({a, b}\)\(\ \)\)]a\) \[And] 
    b == b \[And] a,
   \!\(
\*SubscriptBox[\(\[ForAll]\), \(\({a, b}\)\(\ \)\)]a\) \[Or] 
    b == b \[Or] a};

 FindEquationalProof[a \[And] b == b \[And] a, basicAxioms2]

How can I express the axioms and proof using mathematical typography, and not ForAll[], And[], Or[], and such text-based entry?

Answer 1

As mentioned by @CarlWoll in the comments, it comes down to the precedence of operators.

Precedence[And]
(* 215 *)

Precedence[Equal]
(* 290 *)

a ∧ b == b ∧ a // Trace
(* {a && b == b && a, {b == b, True}, a && a} *)

Working upon @CarlWoll's answer, you can define some other infix equal-like operator, define it as Equal, and give it a very low precedence (like the one of Equivalent) to achieve the desired parsing.

CurrentValue[EvaluationNotebook[], {InputAliases, "eq"}] = 
  TemplateBox[{}, "Equal", DisplayFunction -> (" ⪮ " &), 
   InterpretationFunction :> (Sequence["~", "Equal", "~"] &), 
   SyntaxForm -> "⧦"];

However, the precedence of ForAll is $240$, even higher than that of And. So you will still need some brackets.

Obviously, the simplest solution is to just properly parenthesize the whole expression in the first place.