Message Boards Message Boards

0
|
6147 Views
|
5 Replies
|
1 Total Likes
View groups...
Share
Share this post:

Getting off the ground with FindEquationalProof

Brian Tenneson
Posted 4 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:

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 BY: Yehuda Ben-Shimol
Brian Tenneson
Brian Tenneson
Posted 4 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

Please read my corrected answer.
POSTED BY: Yehuda Ben-Shimol
Brian Tenneson
Brian Tenneson
Posted 4 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

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.
POSTED BY: Yehuda Ben-Shimol
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

Group Abstract Group Abstract