# 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?
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
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?
Posted 8 months ago