I don't agree that one has to define sets from which x and y are chosen as well as to define Max. To do syntactic reasoning, it is enough to know that Max is a constant in the language. What is crucial, however, is that the original post omitted two essential quantifiers. The expression S(s,Max) is not a closed formula (it has a free variable s) and is not a proposition. It is not obvious that one can conclude S(Max, Max). Indeed, it may happen that S(s,Max) is itself derived from some open assumptions, or it may be an open assumption. If any of those assumptions contains s free, then one cannot substitute Max for s without changing that assumption as well. Thus, it is not the case that S(s, Max) derives
. It is also misleading to omit the existential quantifier from the last formula.
When I see a logic formula with a free variable that has not been properly introduced, I tend to stop and ask what this variable stands for.