FindEquationalProof: Dual Axioms in Set Theory and Boolean Logic

Posted 1 year ago
2370 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
 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 1 year ago
 Sorry, that the problem was not emphasized enough:As shown above, it can be proved with axioms in FindEquationalProof, thatwhere 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 EnglishRegards Uwe
Posted 1 year ago
 If I understand correctly, the issue is lack of a type system that would separate the two categories at the axiom level.
Posted 1 year ago
 Yes, the issue is lack of Distinct Variables for Sets, Wffs and Classes, as introduced and described at MetaMath Proof Explorer.
 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!