FindEquationalProof: Dual Axioms in Set Theory and Boolean Logic

Posted 4 months ago
965 Views
|
6 Replies
|
2 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
6 Replies
Sort By:
Posted 4 months 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 4 months 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 4 months ago
 If I understand correctly, the issue is lack of a type system that would separate the two categories at the axiom level.
Posted 4 months ago
 Yes, the issue is lack of Distinct Variables for Sets, Wffs and Classes, as introduced and described at MetaMath Proof Explorer.