# 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[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). –  rm -rf 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. –  belisarius Oct 27 '13 at 2:19