# Implementing the field axioms with FindEquationalProof?

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?

• Could I ask for an example of what you would like to prove? – ShyPerson Dec 10 '19 at 22:04
• Sure! A basic example might be to use FindEquationalProof to prove that every field is an integral domain, i.e. for $a, b\in F$ (a field), $ab = 0$ implies $a = 0$ or $b = 0$. – Michael L. Dec 11 '19 at 3:09