Attempt 2

Alright, Frank, I'll provide a second answer, since you didn't find my first answer persuasive so far.

You claim "some mathematicians" find the impredicativity in the definition of the infimum you provided to be objectionable as a form of circular definition and then provided an alternative form of definition as a proposed solution. In my previous answer and subsequent back and forth with you, I have counterasserted that the impredicativity is not only not objectionable, but necessary since the rigor added to the term 'infimum' is a precising definition that establishes through the addition of a metric criterion articulated on a well-ordered set of lower bounds. So...

The Example versus Your Definition

You are confusing the impredicativity in the definition with the labeling of the definition. The impredicativity inherent in your example extends not from the label or name or mention 'infimum', but from the self-reference in the definition (or better the explanation) of what an infimum is by invoking the set X on both sides of the logical biconditional. Your solution is simply to take the converse half of the biconditional and move the mention 'infimum' to the RHS from the LHS. Let's simplify to make the predicates and logical operators simpler to see:

Example as biconditional: y is the infimum of X <--> y is the greatest lower bound of X Frank's rewrite as converse: If y is the greatest lower bound of X, then y is the infimum of X.

Have you really said anything that wasn't said in the first statement? No, all of you have done is eliminated the conditional and kept the converse from the original biconditional. The example is 'P IFF Q' and you've just simplified to 'Q THEN P'. There is no substantial modification of semantics in either P or Q, is there? That's because the impredicativity in the example isn't a function of the syntax or the logical implication between predicates, but of the shared semantics of the predicates themselves. What is self-referential in the example is that the terms '(element) y' and '(set) X' occur in BOTH the first and second predicates of the proposition, so your attempt to eliminate circularity by moving 'infimum' from the LHS to the RHS doesn't remove impredicativity at all PRECISELY because the self-referential portions haven't been modified. To boot, one can write a logically equivalent statement of the example by swapping the location of everything before IFF with everything after. That is, 'P IFF Q' is logically equivalent to 'Q IFF P'. Let's do that with your rewrite:

Given a set X, if AND ONLY IF (1) there exists lower bounds of X, (2) lower bounds can be ordered and (3) y is a lower bound for X such that (4) for any lower bound z of X, z ≤ y, y is called inf(X)

See? By adding 'AND ONLY IF' in your definition and removing 'then', your definition goes back from being the converse to the biconditional form of the original itself (though you seemed to hedge your language by explicitly conducting existential quantification in (1) which is presumed in the example). Now, let's get to the heart of the impredicativity itself which has nothing to do either with explicit existential predication or the logical consequence between the predicates. The impredicativity stems from the the invocation of 'element y' and 'set X' in both the first and second predicates. That is where the self-reference occurs.

Semantic Compositionality and Synonymy

Let's review the two predicates in naturalish language and functional syntax:

P: y is the infimum of X
[infimum(y,X)]
Q: y is the greatest lower bound of X
[glb(y,X)]
Example: y is the infimum of X if and only if y is the greatest lower bound of X
[infimum(y,X) <-> glb(y,X)]

See the impredicatvity now? It's not the mention or location of 'infimum', it's the invocation of (y,X) as part of both predicates! This is the self-reference that some might object too. But, like I've said, this impredicativity is not a bug, it's a feature. It allows us to establish a psychological equivalence (or mathematical identity relation if you prefer) between mention 'infimum' and the conditions to establish the glb using the notation '≤'. And that is important in real analysis, because it adds the rigor of a metric space to an intuitive notion of greatest lower bound, which can feel uneasy because to talk about a greatest lower anything feels a bit paradoxical, doesn't it? Same exact process for supremum, and we now are clear on the abstractions infimum and supremum and can move on to monotonicity and other abstractions.

Now, as a brief extension to address one objection, we can finish up our exploration to gain an insight into why the impredicativity is a necessary part of the act of precising (as in precising definition) by noting that:

CLAIM 1 'infimum' is a synonym for 'lower bound'

does have a defense. There are two senses to synonym, one which demands an exact substitution and one that allows an approximate substitution. For instance, take a look at all the synonyms for infer (thesaurus.com). Any thesaurus entry will be the same. It will introduce semantically similar items as well as semantically identical items. In this case, you are right to object that it is not an identity. But similarity is itself used even in aritmetic as an approximative identity relation. For example consider another claim:

CLAIM 2 y₁≈y₂ and y₁=y₂ are identity relations

Is a wholly acceptable propositions as long as one accepts there are approximative and strict notions of identity. The mere fact that there are distinct symbols for each essentially confirm the acceptability of CLAIM 2. So, to claim that 'infimum' is a synonym for 'lower bound' is quite meaningful because it allows the claimant to initially indicate in natural language of the underlying semantic similarity, and then to specify additional criteria to move the approximate identity to one of strict identity using the addition of the well-orderedness and existence of a greatest member of the set of all lower bounds. In natural language:

EXAMPLE IN NATURAL LANGUAGE: An infimum is a lower bound that is the greatest of all lower bounds.

And viola! There we have what is going on in this highly technical example to begin with. We are saying that there exists this thing 'infimum' that is not only a lower bound, but also the greatest when compared with all the others.

Summary

So, does your definition serve as an adequate response to "those" who complain about circularity? No, because:

1. There is no problem from circularity in the first place (My entire real analysis textbook is filled with this type of analytical real definition (according to Robinson).
2. Your attempt to remove self-reference doesn't remove self-reference. It only weakens the logic relation (setting aside your strengthening of the definition by making explicit existential quantification).