I've had this circular discussion with RobbBB for a couple of hours. Maybe you will have better luck.

If a definition is not meant to be explanatory, its usefulness in understanding that which is to be defined is limited.

Exactly.

The "∀" doesn't refer to all e.g. logically constructible x, does it? Or to all computable x. For the definition to make sense, it needs to refer to all x that exist, otherwise we'd conclude that 'exists(flying unicorns)' is true. Still implicitly refers to that which is to be defined in its definition, rendering it circular.

That's one option for explaining the domain of ∀. Another is to simply say that that the domain is the universe, or that it's everything, or that it's unrestricted. All of those can be expressed without speaking in terms of existence.

If you have no idea what those ideas mean, but understand 'exists', then, sure, maybe you'll need to demand that all those ideas be unpacked in terms of existence. But what of it? If you do understand those terms but not 'exists', then interdefining them can be cognitively significant for you. Broadly speaking, the function of a definition is to relate a term that isn't understood to a term that is. If you already understand both terms, then the definition won't be useful to you; but that isn't a criticism of the definition, if other people might not understand both terms as well as you do. It's just a biographical note about your own level of linguistic/conceptual expertise.

What is EXT(=)? Some set of all existing things?

It's the extension of the identity predicate, a set of ordered pairs. Relational predicates of arity n can be treated as sets of n-tuples.

If so, would that definition do any work for us?

Do any work for who? What is it you want, exactly? If you've forgotten, the first thing I said to you was "I'm not saying it's a very useful definition". You don't need to prove it's circular in order to prove it's useless, and if you did prove it's circular ('circular' in what sense? is there any finite non-circular chain of definitions that define every term?) that very likely wouldn't help demonstrate its uselessness. So what exactly are you trying to establish, and why?

All that said, I think RobbBB is one of the best posters LW has. Like top 10. He stands out for clarity, seriousness, and charity.

It certainly has not been my impression. I found my discussion with him about instrumentalism, here and on IRC, extremely unproductive. Seems like a pattern with other philosophical types here. Maybe they don't teach philosophers to listen, I don't know. For comparison, TheOtherDave manages to carry a thoughtful, polite and insightful discussion even when he disagrees. More regulars here could learn rational discourse from him.

Or maybe I'm falling prey to the Bright Dilettante trap and the experts in the subject matter just don't have the patience to explain things in a friendly and understandable fashion. I'm not sure how to tell.

Also, I think you shouldn't do that thing where you undermine some other poster while avoiding directly addressing them or their argument.

I take back the "pseudo-" part. His answers were precise, but from a wrong domain.

How about this: Mathematicians have a conception of existence which is good enough for doing mathematics, but isn't necessary correct. When you give a mathematical definition of existence, you are implicitly assuming a certain mathematical framework without justifying it. I think you would consider this criticism to be a variant of #2.

In particular, I also think about things mathematically, but when I do so, I don't use first-order logic, but rather intuitionistic type theory. Can you give a definition for existence which would satisfy me?

Thank you, this framework helps. Definitely no to 1. Definitely yes to 2, with some corrections. Yes to some parts of 3.

Re 2. First, let me adopt bounded realism here, with physics (external reality or territory) + logic (human models of reality, or maps). Let me ignore the ultraviolet divergence of decompartmentalization (hence "bounded"), where Many Words, Tegmark IV and modal realism are considered "territory". To this end, let me put the UV cutoff on logic at the Popper's boundary: only experimentally falsifiable maps are worth considering. A map is "true" means that it is an accurate representation of the piece of territory it is intended to represent. I apologize in advance if I am inventing new terms for the standard philosophical concepts -- feel free to point me to the standard terminology.

Again, "accurate map", a.k.a. "true map" is a map that has been tested against the territory and found reliable enough to use as a guide for further travels, at least if one does not stray too far. Correspondingly, a piece of territory is said to "exist" if it is described by an accurate map.

On the other hand, your "invisible mathy things" live in the world of maps. Some of them use the same term "true", but in a different way: given a set of rules of how to form strings of symbols, true statements are well-formed finite strings. They also use the same term "exist", but also in a different way: given a set of rules, every well-formed string is said to "exist".

Now, I am not a mathematician, so this may not be entirely accurate, but the gist is that conflating "exist" as applied to the territory and "exist" as applied to maps is indeed a category error. When someone talks about existence of physical objects and you write out something containing the existential quantifier, you are talking about a different category: not reality, but a subset of maps related to mathematical logic.

I am not sure whether this answers your objection that

why I should believe in these invisible eternal number-like things that exist in their own unique number-like-thing-specific way. (And what it would mean to believe in them!)

but I hope it makes it clear why I find your replies unconvincing and generally not useful.