# Using quantifiers with free indices as declarative conditions in equation solving

This is a toy example:

Is there a way to rewrite

Reduce[{Norm@{c[1],  c[2],  c[3]} == 1,
0 <=  c[1] < c[2] < c[3]},
{c[1], c[2], c[3]}]


As something like

Reduce[{Norm@{c[1], c[2], c[3]} == 1,
0 <= c[1] &&
ForAll[{i,j}, Implies[i<j, c[i] < c[j]]]}, {c[1], c[2], c[3]}]


?
(Which of course doesn't work)

-
Can it not be reduced (in most cases) to an equivalent Table? For example, And @@ Flatten@Table[c[i] < c[j], {i, 3}, {j, i + 1, 3}]... Of course, this is not as elegant as using ForAll (if it were possible). – R. M. Oct 26 '13 at 23:25
@rm-rf That's what we always do, and sometimes it's an unwanted burden. Quantifiers let you express any logical proposition (theorem), so a general usage is probably outside the scope of Mma as it is now. But perhaps there is a trick for using them for basic expressions. – Dr. belisarius Oct 27 '13 at 2:19
@belisarius I almost certainly missing the point: Module[{v = {c[1], c[2], c[3]}}, Reduce[{Norm@v == 1, ##, c[1] >= 0}, v] & @@ Thread[Differences[v] > 0]] – ubpdqn Jul 9 '15 at 10:57
@ubpdqn The idea is to be able to use logic quantifiers (ForAll, Exists) and FREE indices (i.e. i , j vs 1 , 2) and leave to Mma the building of the necessary "tupling". Your code is off course OK, but now instead of the used above "the components of the list are positive and strictly increasing" for three elements the following "Each element is equal to at least one multiplication between other two" with the simplicity of ForAll[{k}, Exists[{i,j}, i!=j &&i!=k&&j!=k && c[[k]] = c[[i]] c[[j]]]] – Dr. belisarius Jul 9 '15 at 14:08