Message Boards Message Boards


Getting off the ground with FindEquationalProof

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


It's not working. Any advice?

5 Replies

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...


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?

Please read my corrected answer.

Posted 8 months ago

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]

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.

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract