Getting off the ground with FindEquationalProof

Questions
1

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?

2

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

3

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?

4

Please read my corrected answer.

5

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]
6

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.