Message Boards Message Boards


FindEquationalProof: Dual Axioms in Set Theory and Boolean Logic

Posted 2 years ago
7 Replies
4 Total Likes

With the new Mathematica object "FindEquationalProof" it is possible to prove, that one expression in Boolean Logic is equal to the corresponding expression in Set Theory, despite the first is dealing with Booleans, the other is dealing with Sets (refer to the following example).

In[868]:= axioms = {
   ForAll[{A, B}, 
    union[A, intersection[B, complement[B, "\[CapitalOmega]"]]] == A],
   ForAll[{a, b}, and[a, or[b, not[b]]] == a]};

hypoth = ForAll[{x, y}, 
   and[x, or[y, not[y]]] == 
    union[x, intersection[y, complement[y, "\[CapitalOmega]"]]]];

In[870]:= proof = FindEquationalProof[hypoth, axioms, TimeConstraint -> 10]

and here a hardcopy for better visualization: enter image description here

This should not be possible!

At the "MetaMath Proof Explorer Home Page" it is explained, why it is necessary to define "Distinct Variables" and to distinct variables between "wffs", "sets" and "classes", to perform proper mathematical proofs:

I wanted to implement some basic axiom systems for example Booleans and from Set Theory, but I got proofs, which are not really valid, so that I could not further use FindEquationalProof for my intention. I updated Mathematica to Release 12 particular due to my great expectations to this new functionality.

Is there any workarround, to prevent FindEquationalProof matching different symbols of different types ? Is there any hope to get FindEquationalProof improved, so that the implementation of axiom systems like shown at MetaMath will be possoble in the future? This would be a really great progress for me

Thank you for any comments

Regards Uwe

7 Replies

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!

So far as naming goes, the variables all seem to be properly scoped. I do not see an issue here. If there is one it should be stated clearly and succinctly. I do not propose to go through a web site haystack looking for a needle.

Posted 2 years ago

Sorry, that the problem was not emphasized enough:

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

enter image description here

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

If I understand correctly, the issue is lack of a type system that would separate the two categories at the axiom level.

Posted 2 years ago

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

Posted 2 years ago

Hello Jonathan,

Thank you for your comprehensive answer. Particular your hardcopy of the FindEquationalProof-12.1-example adapted to my axiom-problem makes me very hopeful, that this problem can be solved with your new predicates “IsBoolean[x]” and “IsSet[x]” as you have shown. So I hope, that everything goes smoothly with your further development.

I assume, that this both new predicates are fix implemented as Mathematica functions and that it will not be possible to introduce userdefined predicates for use in FindEquationalProof. As I mentioned above, there is an Internet Project "MetaMath", where hundreds of general mathematical theorems are described and already proved by their own Theorem Proofer. They use additionally “Distinct variables” and “Class Variables” for their definitions, additionally to {wff = “IsBoolean[x]”; setvar = “IsSet[x]”}. I do not know if such additional variable types are basically necessary (I think not), but they explain, that this types of variables make proofs much easier than the classical “wff (well formed formular) / set” – based proofs.

For my intention it would be a great advantage, if I could take a set of theorems for a specific theory e.g. "Probability Theory" from MetaMath, implement it as axioms to Mathematica/FindEquationalProof and then I could try to prove my own theorems as I need it for my own. For that, a little bit of compatibility between this both systems (Mathematica and MetaMath) would be really great, I guess not only for me.

But nevertheless, I am hopefully looking forward to your next features, coming with Mathematica 12.1 and your great FindEquationalProof-Object.

Best Regards, Uwe Moehring

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?

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract