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?

  • $\begingroup$ Could I ask for an example of what you would like to prove? $\endgroup$
    – ShyPerson
    Commented Dec 10, 2019 at 22:04
  • $\begingroup$ 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$. $\endgroup$
    – Michael L.
    Commented Dec 11, 2019 at 3:09

1 Answer 1


As I understand it, the field axioms cannot be axiomatized this way. But others are trying other ideas.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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