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"
.
Implies
with the equivalentNand[#1, Not[#2]]&
? $\endgroup$ – Patrick Stevens Mar 17 '18 at 23:05Or[Not[#1],#2]&
, which I had already tried. $\endgroup$ – murray Mar 18 '18 at 0:27