# Connection between a symbol and its subscript form?

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.

• 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. Mar 6 '19 at 7:46
• 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. Mar 6 '19 at 11:56
• 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. Mar 6 '19 at 11:57