I am fiddling around with FindEquationalProof, currently trying to prove some basic statements for fields. I have a set of axioms which almost constitutes the field theory axioms:
fieldTheory = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
ForAll[{a}, p[a, p0] == p[p0, a] == a],
ForAll[{a}, p[a, pinv[a]] == p[pinv[a], a] == p0],
ForAll[{a, b}, m[a, b] == m[b, a]],
ForAll[{a, b, c}, m[a, m[b, c]] == m[m[a, b], c]],
ForAll[{a}, m[a, m1] == m[m1, a] == a],
ForAll[{a}, m[a, minv[a]] == m[minv[a], a] == m1],
ForAll[{a, b, c}, m[a, p[b, c]] == p[m[a, b], m[a, c]]]}
Of course, the glaring issue is that the existence of multiplicative inverses is not correctly specified. Namely, I have used a universal qualifier for a statement which is not universally true: the additive identity does not have a multiplicative inverse. If I use the axioms as written, the proof algorithm always ends up generating a proof that $0 = 1$ in trying to show any nontrivial statement. However, I cannot figure out how to build my set of axioms in such a way that FindEquationalProof accepts them. It appears from the documentation that FindEquationalProof requires all axioms to be either equational logic identities or universal qualifiers over equational logic identities. If I try to use
Forall[{a}, a != p0, m[a, minv[a]] == m[minv[a], a] == m1]
or something similar, I get an error that says something like
FindEquationalProof::invs: Invalid specification of propositions...
Is there even a way to fit the nonexistence of the multiplicative inverse of $0$ into this framework?
