What is a good definition of a mathematical structure? At the moment I am writing a textbook in Foundations of Mathematics for students and trying to give a precise definition of a mathematical structure, which is the principal notion of structuralist approach to mathematics, formed by Bourbaki. Intuitively (and on many examples) the notion of a mathematical structure is clear: this is a pair $(X,S)$ consisting of a set $X$, endowed with a structure $S$, which is a set somehow related to $X$. This relation of $S$ to $X$ is well-defined in universal algebras or first-order theories. What about the general case?
I arrived the the following definition and would like to ask some terminological questions.
The main idea is that a mathematical structure is determined by a list $\mathcal A$ of axioms. By an axiom I understand a formula $\varphi(x,s,c_1,\dots,c_n)$ in the language of Set Theory with free variables $x,s$ and parameters which are some fixed sets $c_1,\dots,c_n$.

Definition. A mathematical structure of type $\mathcal A$ is any ordered pair of sets $\langle X,S\rangle$ such that for any axiom $\varphi$ in the list $\mathcal A$, the formula $\varphi(X,S,c_1,\dots,c_n)$ is true.
The set $X$ is called the underlying set of the mathematical structure $\langle X,S\rangle$ and the set $S$ is called its structure.

In the list $\mathcal A$ of axioms we can encode all desired properties of the structure $S$, for example that it is an indexed family of some operations or some relations on $X$ that have some desirable properties.

The question is how to call the list of axioms $\mathcal A$ determining a type of a mathematical structure? Which properties of the list $\mathcal A$ guarantee that mathematical structures of type $\mathcal A$ form a category (for some natural notion of a morphism between mathematical stuctures of type $\mathcal A$)?

I have a strong feeling that such questions has been already studied (and some standard terminology has been elaborated), but cannot find (simple) answers browsing the Internet. I would appreciate any comments on these foundational questions.
 A: My main comment is this: I would do it differently.
My training tends to look at (set-based) determinations of structures as an arrangement or system of sorts which is a (often finite) tuple of sets, and then separately a language which has a tuple of symbols and rules for what characterizes a well formed sentence, and then some correspondence which allows one to interpret or apply sentences to the tuple of sorts to see if indeed the sentence is true or holds in the system of sets.  Your initial attempt tries to rewrap these two notions into one, but I see that as causing problems later when you want to apply the sorts (or variations on them) to other languages (or variations on the first language): in your scheme you may have to throw out script A and rebuild from scratch script B in order to consider these changes.
This set based version will also not apply to those systems that emphasize a notion of relation over membership.  It's taking me a long time to learn to use category theory because I am loathe to give up the habits developed with using membership, and it is hard for me to switch to manipulating objects and arrows without trying to interpret them as domains and functions. Yet a lot of new programming languages and structures in computer science benefit from adopting different perspectives on structures, especially viewing objects by their properties and not by their (membership-based) constituents.
You might try a goal-oriented approach.  First determine what you want to do, and then try to organize structures to accomplish your goal.  If a lot of your work depends on establishing a form of equality or containment, then go with set based.  If much has to do with relations or elegant expression of procedures, consider a notation that captures the fundamental of the relational or procedural work you will do.
I recommend for inspiration George Bergman's invitation to universal constructions (his 245a class text of similar title), followed by chapter 3 of Algebras, Lattices,Varieties by McKenzie McNulty and Taylor, which has two formulations of category theory. Then try some books on Haskell or other functional programming language.  Hilbert and Ackermann's classic text on higher order logics, and Hans Hermes book on computation (title escapes me) consider other systems like Fitch's minimal calculus.  If your formulation(s) does not consider all of these for mathematical structures, I think you are setting the bar too low.
Gerhard "Ask Me About System Design" Paseman, 2020.05.21.
A: I doubt that there is any generally accepted definition of "structured set" in mathematics that includes a notion of morphism and does not already use the technology of category theory.  (For a "behavioral" definition that does use category theory, see for instance here.)  As has been noted in the comments, very few mathematicians have even ever seen Bourbaki's actual definition, and it probably had some issues.
The definition you propose seems too broad.  Allowing arbitrary formulas of set theory enables axioms like "$x=\{\emptyset\}$", so you would have a type of structure such that $\{\emptyset\}$ admits that structure but $\{\{\emptyset\}\}$ does not.  This is contrary to the general understanding of structuralism that a "structure" should be transportable across any bijection.
Probably the best-known general notion of "structured set" that forms a category (and is isomorphism-invariant) would be the models of a first-order theory.  One can expand the class of models here by considering infinitary languages.  However, this doesn't include examples such as topological spaces, which are still intuitively "structured sets".
The obvious way to remedy this difficulty is to use higher-order logic.  The problem is that there is no obvious "correct" way to define non-invertible morphisms between models of a higher-order theory.  How do you make continuous maps of topological spaces fall out of a general notion of morphism, given the contravariant character of continuity on open sets?
There are at least partial solutions to this problem, although I don't think any of them is standard or well-known.  For instance, the double powerset functor is covariantly functorial in a canonical way (induced from the contravariant functoriality of the single powerset), so if we restrict our higher-order signatures to contain only relations between elements of iterated powersets $P^n(x)$ where $n$ is even, then there is a straightforward definition of morphism of structures.  One can then represent and axiomatize topological spaces with such a signature having a single predicate on $P(P(x))$ that picks out the supersets of the topology, and the induced morphisms will be continuous maps.  (We discovered this as part of our work on the higher structure identity principle.)
It's less clear that this approach can also represent morphisms between structures that should be covariant on subsets, but it seems to to be possible in at least some cases, such as suplattices.  One could also try to augment a higher-order signature with explicit "variance information" that would determine the morphisms.  Unfortunately, it's hard to make (let alone prove) a general claim that any such approach "always works" without any existing general notion of "structure" (with attendant notion of morphism) to compare it to!
Defining invertible morphisms between structures, on the other hand, is entirely straightforward.  So if all you want is a groupoid of structures, then higher-order logic should do the job.  This is one of the arguments for the "more foundational" nature of groupoids over categories: the groupoid of topological spaces (for instance) is uniquely and canonically determined by the notion of "topological space" (expressed, for instance, as a higher-order theory), but the same can't really be said for the usual category of topological spaces (from a purely abstract point of view, what privileges continuous maps over, say, open maps?).
So if your goal is just to have a definition with which to "speak about mathematical structures as the main subject of study of mathematics", I would say that higher-order logic is probably the best answer.  If you also want to use this as a lead-in to introduce category theory, then my suggestion would probably be to discuss particular examples, then general morphisms of models of first-order theories, then isomorphisms of models of higher-order theories, then mention that defining a correct general notion of noninvertible morphism in terms of a higher-order theory is tricky, and finally use that difficulty as a motivation to refocus attention not on the notion of structure (i.e. the objects of the category) but on the entire category itself as an object of study.
