# Getting off the ground with FindEquationalProof

Posted 8 months ago
1041 Views
|
5 Replies
|
1 Total Likes
|
 What am I doing wrong here? axiom0 = ForAll[{x, y}, ForAll[z, Implies[Equivalent[z\[Epsilon]x, z\[Epsilon]y], x == y]]] seta = {1, 2, 3}; setb = {3, 2 , 1}; FindEquationalProof[seta == setb, axiom0] I am attempting to write an extensionality axiom followed by a proof that {1,2,3} = {3,2,1}. Here, [Epsilon] denotes set membership.Thanks!It's not working. Any advice? Answer
5 Replies
Sort By:
Posted 8 months ago
 There are some problems You used \[Epsilon]. It is just a symbol, you are looking for MemberQ you used == (i.e., Equal) when you put seta == setb automatically the operation will be evaluated as False. So just make some symbolic function that will denotes the two sets are identical or equal (eg., eq[x,y]) Last one, Implies[False, True] returns True meaning that if there is some z that belongs to set y but not to set x the relation is still True... so the "axiom" is practically ForAll[{x,y}, eq[x,y]] regardless of z, so ANY two sets are defined equal by the presented logic of this expression You need another way to define the relation...best Answer
Posted 8 months ago
 Thank you...I'm not sure why, but that doesn't work when I try it. Perhaps that's because the lines are broken to begin with. Maybe I just need to restart Mathematica. Would you like to shed some light on that? Answer
Posted 8 months ago Answer
 Trying to correct code with the suggestions. I didn't see how I could use MemberQ; so I used Element. How would you tweak the code below to get a proof that {1,2,3} = {3,2,1}. axiom2 = ForAll[{x, y}, Implies[ForAll[z, Equivalent[Element[z, x], Element[z, y]]], x === y]]; seta = {1, 2, 3}; setb = {3, 2, 1}; FindEquationalProof[seta === setb, axiom2] Answer
 It seems that you will not be able to do that. Element[1,{1,2,3}] does not return either True or False for relations with sets, the expression is just returned unevaluated.Within programs MemberQ[{1, 2, 3}, 1] returns True but it is not useful for logical proofs.From what I noticed in the documentation it seems that proofs in set theory are not supported by the theorem proving tool.I hope if someone more involved in this area would be able to comment further. Answer