Message Boards Message Boards

GROUPS:

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

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:

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
Posted 5 months ago
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
Posted 5 months ago

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:
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract