Message Boards Message Boards

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

GROUPS:

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:
POSTED BY: patrikfrnka
Answer
13 days 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 BY: Daniel Lichtblau
Answer
12 days 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 BY: patrikfrnka
Answer
12 days 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
POSTED BY: Gianluca Gorni
Answer
12 days 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 BY: patrikfrnka
Answer
12 days 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:
POSTED BY: patrikfrnka
Answer
6 days ago

Group Abstract Group Abstract