I have read all about subscript forms and that they are DownValues of Subscript[]. I still do not understand the following:

These all work fine and produce True:

Reduce[ForAll[t, Exists[Subscript[s, 1], t == Subscript[s, 1]]]]
Reduce[ForAll[Subscript[s, 2], 
    Exists[Subscript[s, 1], Subscript[s, 2] == Subscript[s, 1]]]]
Reduce[Exists[{s, Subscript[s, 1]}, s == Subscript[s, 1]]]

however this:

Reduce[ForAll[s, Exists[Subscript[s, 1], s == Subscript[s, 1]]]]

produces the error:

Reduce::nsmet: This system cannot be solved with the methods
    available to Reduce.

I see similar behavior if instead of the subscript, I use: OverHat[s].

Based on b3m2a1's comment, I switch the order of s and Subscript[s, 1], and it indeed works (producing True):

Reduce[ForAll[Subscript[s, 1], Exists[s, s == Subscript[s, 1]]]]

There might be "nothing particularly deep going on," but I'd like to understand, if only to know what to avoid.

Another possible clue: the case that did not work above, after the error message, it repeated the input as:

Reduce[ForAll[s, s == Subscript[s, 1]]]

We see that the entire Exists[Subscript[s, 1], ...] part is gone, apparently Reduce[] logically discarded it. But this discards the "definition" of Subscript[s, 1] as well. It would seem that that is not okay, but discarding the definition of s would be okay. Does that make more sense? If so, please explain.

Any pointers would be most appreciated. Thanx.

  • $\begingroup$ I think you're just seeing the effect of when quantifiers are bound in Reduce... like all of the True examples allow the "Subscript-form" to effectively be replaced with a Symbol that is independent of s but the last example doesn't, although maybe it should. There's nothing particularly deep going on. $\endgroup$
    – b3m2a1
    Mar 6 '19 at 7:46
  • 1
    $\begingroup$ If you use someSymbol to represent a variable, never use a compound expression containing someSymbol to try to represent a different variable. That means that once you used s to denote something, you can't get away with also using Subscript[s,1] or OverHat[s] or s[1] because the system can't distinguish that from something like f[s] where f would represent some function. It's safe to use both Subscript[s,1] and Subscript[s,2] but it is not safe to use one of these two together with a naked s. $\endgroup$
    – Szabolcs
    Mar 6 '19 at 11:56
  • 3
    $\begingroup$ I consider this a shortcoming of the design and generally avoid using Subscript. There are situations where it's useful though, e.g. when needing to generate a abritrary number of variables, we typically do var[1], var[2], .... Subscript[var,1], ... would be just as good. But then don't use var on its own. $\endgroup$
    – Szabolcs
    Mar 6 '19 at 11:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.