Group Abstract Group Abstract

Message Boards Message Boards

0
|
8.6K Views
|
5 Replies
|
1 Total Like
View groups...
Share
Share this post:

Getting off the ground with FindEquationalProof

Brian Tenneson
Posted 5 years ago

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?
POSTED BY: Brian Tenneson
5 Replies
Sort By:
POSTED BY: Yehuda Ben-Shimol
Brian Tenneson
Brian Tenneson
Posted 5 years 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]
POSTED BY: Brian Tenneson
POSTED BY: Yehuda Ben-Shimol
POSTED BY: Yehuda Ben-Shimol
Brian Tenneson
Brian Tenneson
Posted 5 years 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 BY: Brian Tenneson
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Tag limit exceeded
Note: Only the first five people you tag will receive an email notification; the other tagged names will appear as links to their profiles.
Reply Preview
Attachments
Remove
or Discard