How do you write the question of the classification of simple groups as a mathematical formula?

Question

How do we write the question "Classify all the finite simple groups." As a predicate logical existential formula?

My attempt is below but my notation is not very good:

How does one express a classification in mathematical terms? For me it seems to be finding a numbering of the groups such that each natural number can be assigned to a group and vice versa. (Assuming there are infinite number of them - as an example the first 26 natural numbers could be assigned to the sporadic groups and then we could alternate over each member of the other infinite families. Or instead of natural numbers as labels one could use tuples of natural numbers to make things a little simpler.)

So there must be a function $f(x)$ which maps a natural number onto a simple group and a function $g(x)$ which maps a simple group onto a natural number.

And so a complete classification would have $f(g(x))=x$ because it is on-one. And also $g(f(x))=x$ for all natural numbers.

So my attempt is:

"Solve for $f$ where:

$\forall\{ABEFGH\subset Grp\}| f:\{Grp\rightarrow \mathbb{N}\} \land (A\neq B \implies f(A)\neq f(B)) \land A/E\neq F \land B/ G \neq H $ "

What I've attempted to write here is that for every two groups that are simple they have different values of f(A).

This isn't very good since I haven't put in how to say when two groups are equal (or even defined what a group is!). Perhaps it should be better written as an expression concerning matrices or permutations. Also I haven't accounted for it skipping some natural numbers.

If the expression above is written as $P(f)$ then

$\exists f P(f)$

is true if a classification exists and false otherwise.

This is just my bad attempt at writing this question rigorously.

What is the shortest existential statement equivalent to "The finite simple groups can be classified."?

(My interest in this is assuming that one day the proof is computer checked. What is it exactly they are proving as a statement in logic.)

Answer 1

The statement in logic would involve the definition of a set $\Omega$ of finite simple groups and a theorem stating that any finite simple group $G$ is isomorphic to $H$ for some $H$ in $\Omega$.

Answer 2

This sort of statement ("there exists a classification") is not the kind of thing that can be stated precisely in formal logic. The problem with your approach is not the details you mentioned you left out (which are trivial if tedious to include), but that the existential quantifier on $f$ makes your statement have a totally different meaning from what mathematicians usually mean when they say "there is a classification of finite simple groups". The existence of some function to $\mathbb{N}$ which classifies finite simple groups is totally trivial; that would just amount to checking that there are only countably many finite simple groups up to isomorphism.

What "there exists a classification" means is "there exists a useful classification", where we can say exactly what all the cases are in a way that is easy to use and understand. This is not something you can state in formal logic, since "easy to use and understand" is subjective.

The actual statement of the classification of finite simple groups is not "there exists a classification" but "this particular list is a classification". In other words, it is a list of specific families of finite simple groups together with the assertion "every finite simple group is isomorphic to a group in one of these families".