9
$\begingroup$

Start, as in the Mathematica 11.3 documentation, with:

   groupTheory = {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], 
                  ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e]}

The result I want Mathematica to prove is the uniqueness of the identity e:

   uniqueIdentityThm = ForAll[f, Implies[ForAll[x, g[x, f] == x], f == e]]

If I try...

   FindEquationalProof[uniqueIdentityThm, groupTheory]

... then I get a surprising error message:

... FindEquationalProof: Invalid specification of propositions ....and axioms..

Do I have a syntax error I'm not seeing?

Or is the issue simply the presence of Implies?

Note that the general form of what I'm trying to do is OK, for example:

   inverseIsInvolution = ForAll[x, inv[inv[x]] == x
   FindEquationalProof[inverseIsInvolution, groupTheory]

This does yield a ProofObject, which can be examined, e.g., by evaluating the preceding result with argument "ProofNotebook".

Improve this question
$\endgroup$
2
  • $\begingroup$ Does it work if you replace Implies with the equivalent Nand[#1, Not[#2]]&? $\endgroup$ – Patrick Stevens Mar 17 '18 at 23:05
  • $\begingroup$ @PatrickStevens: No, and not with the equivalent Or[Not[#1],#2]&, which I had already tried. $\endgroup$ – murray Mar 18 '18 at 0:27
6
$\begingroup$

Let us consider the axioms for a group:

groupTheory={ForAll[{a,b,c},g[a,g[b,c]]==g[g[a,b],c]],
  ForAll[a,g[a,e]==a],
  ForAll[a,g[a,inv[a]]==e]};

As shown in the question, Murray's command for proving that the right identity is unique:

FindEquationalProof[Implies[ForAll[a, g[a, f]==a], e==f], groupTheory ]

fails with a message that there is an invalid specification of propositions and axioms. This suggests (I am not sure at all) that the first argument of Implies is considered as an axiom, that should be placed in the second argument of FindEquationalProof. Anyway, the unicity can be shown with Mathematica in the following way:

FindEquationalProof[e==f, Append[groupTheory, ForAll[a, g[a, f]==a] ]]

(* ProofObject[Logic: EquationalLogic   Steps: 10 ...] *)

And for sake of completeness, Mathematica can show that any right identity is also a left identity:

FindEquationalProof[ForAll[a, g[e, a]==a], groupTheory ]

(* ProofObject[Logic: EquationalLogic   Steps: 11 ...] *)
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.