# Can you please tell me if this is a bug in quantifiers?

Posted 5 months ago
659 Views
|
5 Replies
|
2 Total Likes
|
 Consider the following code: In[1]:= l1={3,3,3} Out[1]= {3,3,3} In[2]:= l2={1,2,3} Out[2]= {1,2,3} In[4]:= ForAll[x,MemberQ[l1,x],Exists[y,MemberQ[l2,y],x==y]] Out[4]= True In[3]:= Exists[z,MemberQ[l2,z],ForAll[u,MemberQ[l1,u],z==u]] Out[3]= False In[5]:= Exists[z,MemberQ[l2,z_],ForAll[u,MemberQ[l1,u],z==u]] Out[5]= True "WHY z HAVE TO BE SET TO PATTERN z_ TO GET RIGHT RESULT?" Attachments:
5 Replies
Sort By:
Posted 5 months ago
 MemberQ will evaluate to False before ForAll ever sees it. THe following will show this. Exists[z, MemberQ[Y, z], ForAll[u, MemberQ[X, u], z == u]] // Trace What is needed is an "algebraicization" of the membership relation. This can be done as below, by setting the product of differences x-elementj to zero. xX = {3, 3, 3}; yY = {1, 2, 3}; myElement[x_, set_] := Apply[Times, x - set] == 0 Resolve is needed for quantifier elimination. Resolve[ ForAll[x, myElement[x, xX], Exists[y, myElement[y, yY], x == y]]] (* Out[304]= True *) Resolve[ Exists[z, myElement[z, yY], ForAll[u, myElement[u, xX], z == u]]] (* Out[303]= True *) If the sets in question are consecutive integers the element check can be done instead via inequalities with a subsequent domain restriction for Resolve. myElement2[x_, set_] := Min[set] <= x <= Max[set] Resolve[Exists[z, myElement2[z, yY], ForAll[u, myElement2[u, xX], z == u]], Integers] (* Out[310]= True *) Alternatively the domain restriction can be placed directly in the element test: myElement3[x_, set_] := Min[set] <= x <= Max[set] && Element[x, Integers] Resolve[Exists[z, myElement3[z, yY], ForAll[u, myElement3[u, xX], z == u]]] (* Out[314]= True *) 
Posted 5 months ago
 Thank you very much for YOUR TIME! I've found documentation about evaluation, so... maybe I'll help myself soon. I'm trying to write elegantly DFA minimalization in Mathematica. There I need some construction to make iteration on set of states: s[i+1]:=s[i] u { p e States| E q e States | E a e Sigma | d[p][a]=q } (HOPE YOU UNDERSTAND this "PSEUDOCODE" - d is transition function) I've attached a sample how far I get yet...:) Thanks for your OPTIONAL suggestions PF Attachments:
Posted 5 months ago
 MemberQ is probably a programming construct, and it is not suitable to logic manipulation. MemberQ[{1},z] evaluates immediately to False inside Exists: Exists[z, MemberQ[{1}, z]] This is a way around the problem: X = {3, 3, 3}; Y = {1, 2, 3}; ForAll[x, Or @@ Thread[x == X], Exists[y, Or @@ Thread[y == Y], x == y]] // Reduce Exists[z, Or @@ Thread[z == Y], ForAll[u, Or @@ Thread[u == X], z == u]] // Reduce 
 In[297]:= xX = {2, 3, 3}; In[298]:= xY = {0, 0, 1}; In[299]:= xZ = {1, 2, 2}; (* E y e Y : Vz e Z :E x e X: x\[Equal]z+1 && y !e X *) Thanks! Yes, this is also good solution. I first meant replace ForAll by And @@ Thread[z == X] (it is shorter but not RIGHT) Complicated formulas can be handled this way also : In[318]:= Exists[y, Or @@ Thread[y == xY],ForAll[z, Or @@ Thread[z == xZ], Exists[x, Or @@ Thread[xX == x], (x == (z + 1)) && ! (Or @@ Thread[xX == y])]]] // Reduce Out[318]= True 
 Hello Everyone! Quantifiers are here again. Finally GOOD solution is here to share, so see notebook for full details :) Shortly: xE[x_, a_, c_] := Block[{i, ce}, For[i = 1, i <= Length[a], i++,(*main result*) ce = With[{x = a[[i]]}, c]; If[ce, Return[ce], , Print["uuups!!!"]]];(*Print["xE False"];*) Return[ce]] SetAttributes[xE, HoldAll] patrikfrnka@seznam.cz Attachments: