Hi Uwe! I'm the developer of FindEquationalProof; hopefully I can be of some assistance.

The proofs that you show are perfectly valid, because (as Daniel pointed out) you haven't distinguished between what should be treated as a set, and what should be treated as a Boolean literal, since you have used the ForAll quantifier in both cases. Pure equational logic is an untyped theory, so unfortunately there is no straightforward way to make such a distinction here.

More fundamentally, set theory is not an algebraic theory, and hence cannot be axiomatized using purely equational logic, since standard axiomatizations such as ZF require more complex predicates than mere equality (and they also involve nasty things like axiom schemas...).

We're currently working on extending FindEquationalProof to support higher-order logics, and there is also a longer-term project to support fully type-theoretic theorem proving. Some of this functionality will be available in 12.1, and some will be released in future versions.

For instance, in 12.1, FindEquationalProof will (assuming that everything goes smoothly!) be able to support first-order/predicate logic, which will make it easy to do what you were trying to do, since now you can specify that certain axioms should only hold when certain predicates (such as IsSet or IsBoolean) apply:

As you can see, the ambiguity that you highlighted (regarding whether the objects should be treated as Boolean or as sets) no longer exists once the two concepts have been properly distinguished using first-order logic.

I hope this helps to clarify things! We're trying our best to make the theorem-proving framework as powerful and as general as possible, so if you have any feedback or suggestions, then I'd love to chat more with you about it. Feel free to get in touch!

Sorry, that the problem was not emphasized enough:

As shown above, it can be proved with axioms in FindEquationalProof, that

where x,y are Boolean variables on the left hand side and x,y are Set-variables on the right hand side of the equation and Omega is the Universial Set.

This mathematical senseless equation could be proved by FindEquationalProof, because the left hand side is logically equivalent to "x" and the right hand side equals to "x" according to Set Theory. The reason for this result is that FindEquationalProof matches Boolean Variables with Set Variables without any distinction between different types. That is the reason why "MetaMath Proof Explorer" inroduced Distinct Variables und distinct between Set Variables, Wff (Well Formed Formulas), and Class-Variables.

I hope the problem and my above questions are better clarified now. Sorry for my poor german English

Regards Uwe

Yes, the issue is lack of Distinct Variables for Sets, Wffs and Classes, as introduced and described at MetaMath Proof Explorer.

Hi Jonathan, I have been learning Proof Theory on my own and am working on a document that mathematically explores some notions of proof theory. I have also described in detail the slowest way to prove something: brute force.

Then I recently learned of the Knuth-Bendix algorithm. From what I see, I was just conceptualizing a 50 year algorithm.

What percent of the theorem proving in Mathematica could be considered to be brute force?
Neat, now that I know I can use Isset like that, how hard would it to write the axioms of set theory? If we can define predicates, it should be possible?