FindEquationalProof: Dual Axioms in Set Theory and Boolean Logic

Posted 2 years ago
5062 Views
|
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: 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:http://us.metamath.org/mpeuni/mmset.htmlI 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 meThank you for any commentsRegards Uwe
7 Replies
Sort By:
Posted 1 year ago
 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?
Posted 2 years ago
 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!
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
 If I understand correctly, the issue is lack of a type system that would separate the two categories at the axiom level.