Distinguishing non-isomorphic groups with a group-theoretic property

I am teaching a first-semester course in abstract algebra, and we are discussing group isomorphisms. In order to prove that two group are not isomorphic, I encourage the students to look for a group-theoretic property satisfied by one group but not by the other. I did not give a precise meaning to the phrase "group-theoretic property", but some examples of the sort of properties I have in mind are $$ \forall g,h\in G:\exists n,m\in\mathbb{Z}:(n,m)\neq (0,0)\wedge g^n=h^m,\\ \forall H\leq G:\exists g,h\in G:H=\langle g,h\rangle,\\ \forall g,h\in G:\exists i\in G: \langle g,h\rangle = \langle i\rangle $$ One of my students asked if, give two non-isomorphic groups, there is always a group-theoretic property satisfied by one group but not the other. In a sense, "being isomorphic to that group over there" is a group-theoretic property. But this is not really what I have in mind.

To pin down the class of properties I have in mind, let's say we allow expressions involving

• quantification over $G$, subgroups of $G$, and $\mathbb{Z}$,
• group multiplication, inversion, and subgroups generated by a finite list of elements
• the symbol $1_G$ (the group identity element),
• addition, subtraction, multiplication, exponentiation (provided the exponent is non-negative), and inequalities of integers ,
• the integer symbols $0$ and $1$,
• raising a group element to an integer power, and
• equality, elementhood, and logical connectives.

I do not know much about model theory or logic, but my understanding is that this is not the first-order theory of groups. In particular, this MSE question indicates that there exist a torsion and a non-torsion group which are elementarily equivalent (meaning they cannot be distinguished by a first-order statement in the language of groups), but these groups can be distinguished by a property of the above form. I have also heard that free groups of different rank are elementarily equivalent, but these can also be distinguished by a property of the above form.

My questions are:

(1) Is there a name for the theory I am considering? Or something closely (or distantly) related?

(2) Are there examples of non-isomorphic groups that cannot be distinguished by a property of the above form? Are there examples where the groups involved could be understood by an average first-semester algebra student?

First, let's start with the silly answer. Your language only has countably many different expressions, so can only divvy groups up into continuum-many classes - so there are definitely non-isomorphic groups it can't distinguish! In general this will happen as long as your language has only set-many expressions: you need a proper class sized logic like $\mathcal{L}_{\infty,\infty}$ to distinguish between all pairs of non-isomorphic structures.

That said, you're right that you're looking at something much stronger than first-order logic. Specifically, you're describing a sublogic of second-order logic, the key difference being that second-order logic lets you quantify over arbitrary subsets of the domain, and indeed functions and relations of arbitrary arity over the domain, and not just subgroups. Second-order logic doesn't have an explicit ability to refer to (say) integers built in, but it can do so via tricks of quantifying over finite configurations.

While the exact strength of the system you describe isn't clear to me, second-order logic is known to be extremely powerful. In particular, I believe there are no known natural examples of non-isomorphic second-order-elementarily-equivalent structures at all, although as per the first paragraph of this answer such structures certainly have to exist! So second-order-equivalence is a pretty strong equivalence relation, and in practice will suffice to distinguish all the groups your students run into.

Here are some simple examples where you at least need to make some decisions about what you believe about set theory to determine whether two groups are isomorphic. Assuming the axiom of choice every vector space has a basis, so $\mathbb{R}$ is isomorphic (as a group) to some direct sum of copies of $\mathbb{Q}$ (in fact necessarily to a direct sum of $|\mathbb{R}|$ copies of $\mathbb{Q}$). The existence of such a basis for $\mathbb{R}$ over $\mathbb{Q}$ allows you to construct Vitali sets, which are non-measurable, and there are models of $ZF \neg C$ in which every subset of $\mathbb{R}$ is measurable, so $\mathbb{R}$ fails to have a basis in such models.

Another example along the same lines is $\left( \prod_{\mathbb{N}} \mathbb{Q} / \bigoplus_{\mathbb{N}} \mathbb{Q} \right)^{\ast}$, taking the dual as a $\mathbb{Q}$-vector space. Assuming the axiom of choice this is a direct sum of $|\mathbb{R}|$ copies of $\mathbb{Q}$ again, but without at least enough choice to construct something like non-principal ultrafilters on $\mathbb{N}$ it's not clear how to write down a single nonzero element of this group!

Another example that's basic and probably counts as cheating: Consider $G = \mathbb{Z}^{\kappa}$ for cardinal numbers $\kappa$ starting with $\aleph_0$. I don't know enough model theory to prove it, but I can't imagine there is a group-theoretic property that distinguishes between these.